Expr_ptr 
Expr_and_from_list(
  node_ptr  list 
)
Performs local syntactic simplification. Nil value is considered as true value

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_and_nil(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_and(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

int 
Expr_attime_get_time(
  Expr_ptr  e 
)
Retrieves the time out of an ATTIME node

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_attime_get_untimed(
  Expr_ptr  e 
)
Retrieves the untimed node out of an ATTIME node

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_attime(
  Expr_ptr  e, 
  int  time 
)
Creates a ATTIME node

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_bool_to_word1(
  Expr_ptr  a 
)
Builds the node for casting boolean to word1. Description [Works with booleans. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_divide(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_equal(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_false(
    
)
Returns the false expression value

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_function(
  const Expr_ptr  name, 
  const Expr_ptr  params 
)
Builds an uninterpreted function named "name" with "params" as parameters. "params" must be a cons list of expressions (Created with find_node)

Side Effects None

Defined in Expr.c

int 
Expr_get_time(
  SymbTable_ptr  st, 
  Expr_ptr  expr 
)
Current time is recursively calculated as follows: 1. UNTIMED_CURRENT for Nil and leaves; 2. UNTIMED_FROZEN if all vars are frozen; 3. Time specified for an ATTIME node, assuming that the inner expression is untimed. Nesting of ATTIME nodes is _not_ allowed; 4. Minimum time for left and right children assuming UNTIMED_CURRENT < UNTIMED_NEXT < t, for any t >= 0.

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_ge(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_gt(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_iff(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_implies(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

boolean 
Expr_is_false(
  const Expr_ptr  expr 
)
Checkes whether given value is the false value

Side Effects None

Defined in Expr.c

boolean 
Expr_is_timed(
  Expr_ptr  expr, 
  hash_ptr  cache 
)
Determines whether a formula has ATTIME nodes in it If cache is not null whenever we encounter a formula in the cache we simply return the previously computed value, otherwise an internal and temporary map is used. NOTE: the internal representation of cache is private so the user should provide only caches generated by this function!

Side Effects cache can be updated

Defined in Expr.c

boolean 
Expr_is_true(
  const Expr_ptr  expr 
)
Checkes whether given value is the true value

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_ite(
  const Expr_ptr  cond, 
  const Expr_ptr  t, 
  const Expr_ptr  e 
)
Performs local syntactic simplification. 'cond' is the case/ite condition, 't' is the THEN expression, 'e' is the ELSE expression

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_le(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_lt(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_minus(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_mod(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_next(
  const Expr_ptr  a 
)
Constructs a NEXT node of given expression

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_notequal(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_not(
  const Expr_ptr  expr 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_or(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_plus(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_range(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Makes a TWODOTS node, representing an integer range

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_resolve(
  SymbTable_ptr  st, 
  int  type, 
  Expr_ptr  left, 
  Expr_ptr  right 
)
Given an expression node E (handled at simplifier-level) the simplifier call this function in post order after having simplified car(E) and cdr(E). It calls it by passing node_get_type(E) as type, and simplified sub expressions for left and right. The function Expr_resolve does not traverses further the structures, it simply combine given operation encoded in type with given already simplified operands left and right. For example, suppose E is AND(exp1, exp2). The simplifier: 1. Simplifies recursively exp1 to exp1' and exp2 to exp2' (lazyness might be taken into account if exp1 is found to be a false constant). 2. Calls in postorder Expr_resolve(AND, exp1', exp2') Expr_resolve will simplify sintactically the conjunction of (exp1', exp2')

Side Effects None

See Also Expr_simplify
Defined in Expr.c

Expr_ptr 
Expr_setin(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Makes a setin node, with possible syntactic simplification.

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_signed_word_to_unsigned(
  Expr_ptr  w 
)
Builds the node for casting signed words to unsigned words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_equal(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_ge(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_gt(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_iff(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_le(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_lt(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_notequal(
  const SymbTable_ptr  st, 
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_word_bit_select(
  const SymbTable_ptr  st, 
  const Expr_ptr  w, 
  const Expr_ptr  r 
)
Builds the node for bit selection of words. Description [Works with words. Performs local semantic and syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_word_extend(
  const SymbTable_ptr  st, 
  Expr_ptr  w, 
  Expr_ptr  i 
)
Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify_word_resize(
  const SymbTable_ptr  st, 
  Expr_ptr  w, 
  Expr_ptr  i 
)
Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_simplify(
  SymbTable_ptr  st, 
  Expr_ptr  expr 
)
Top-level simplifier that evaluates constants and simplifies syntactically the given expression. Simplification is trivial, no lemma learning nor sintactic implication is carried out at the moment. WARNING: the results of simplifications are memoized in a hash stored in the symbol table provided. Be very careful not to free/modify the input expression or make sure that the input expressions are find_node-ed. Otherwise, it is very easy to introduce a bug which will be difficult to catch. The hash in the symbol table is reset when any layer is removed. NOTE FOR DEVELOPERS: if you think that memoization the simplification results may cause some bugs you always can try without global memoization. See the function body below for info.

Side Effects None

Defined in Expr.c

boolean 
Expr_time_is_current(
  int  time 
)
Returns true if the time (obtained by Expr_get_time) is current

Side Effects Expr_get_time

Defined in Expr.c

boolean 
Expr_time_is_dont_care(
  int  time 
)
Returns true if the time (obtained by Expr_get_time) is dont't care

Side Effects Expr_get_time

Defined in Expr.c

boolean 
Expr_time_is_next(
  int  time 
)
Returns true if the time (obtained by Expr_get_time) is next

Side Effects Expr_get_time

Defined in Expr.c

Expr_ptr 
Expr_times(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_true(
    
)
Returns the true expression value

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_unary_minus(
  const Expr_ptr  a 
)
Works with boolean, scalar and words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_union(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Makes a union node

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_unsigned_word_to_signed(
  Expr_ptr  w 
)
Builds the node for casting unsigned words to signed words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_untimed_explicit_time(
  SymbTable_ptr  st, 
  Expr_ptr  expr, 
  int  curr_time 
)
Returns the untimed version of an expression using the current time provided as an argument.

Side Effects Expr_get_time

Defined in Expr.c

Expr_ptr 
Expr_untimed(
  SymbTable_ptr  st, 
  Expr_ptr  expr 
)
Returns the untimed version of an expression

Side Effects Expr_get_time

Defined in Expr.c

Expr_ptr 
Expr_word1_to_bool(
  Expr_ptr  w 
)
Builds the node for casting word1 to boolean. Description [Works with words with width 1. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_bit_select(
  const Expr_ptr  w, 
  const Expr_ptr  r 
)
Builds the node for bit selection of words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_concatenate(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Builds the node for word concatenation. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_extend(
  Expr_ptr  w, 
  Expr_ptr  i 
)
Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_left_rotate(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Builds the node left rotation of words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_left_shift(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Builds the node left shifting of words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_right_rotate(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Builds the node right rotation of words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_word_right_shift(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Builds the node right shifting of words. Description [Works with words. Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_xnor(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

Expr_ptr 
Expr_xor(
  const Expr_ptr  a, 
  const Expr_ptr  b 
)
Performs local syntactic simplification

Side Effects None

Defined in Expr.c

void 
SexpFsm_apply_synchronous_product(
  SexpFsm_ptr  self, 
  SexpFsm_ptr  other 
)
The result goes into self, no changes to other.

Side Effects self will change

Defined in SexpFsm.c

VIRTUAL SexpFsm_ptr 
SexpFsm_copy(
  const SexpFsm_ptr  self 
)
Copy costructor

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create_predicate_normalised_copy(
  const SexpFsm_ptr  self, 
  PredicateNormaliser_ptr  normaliser 
)
Predicate-normalisations means that an expression is modified in such a way that at the end the subexpressions of a not-boolean expression can be only not-boolean. This is performed by changing boolean expression "exp" (which is a subexpression of a not-boolean expression) to "ITE(exp, 1, 0)", and then pushing all ITE up to the root of not-boolean expressions. Constrain: the given Sexp FSM has to be NOT boolean. Otherwise, it is meaningless to apply normalisation functions, since all the exporessions are already boolean.

Side Effects SexpFsm_copy

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create(
  const FlatHierarchy_ptr  hierarchy, 
  const Set_t  vars 
)
Given hierarchy will be copied, so the caller is responsible for its destruction. Vars set is also copied, so the caller is responsible for its destruction (best if frozen)

Defined in SexpFsm.c

VIRTUAL void 
SexpFsm_destroy(
  SexpFsm_ptr  self 
)
Destructor

Defined in SexpFsm.c

node_ptr 
SexpFsm_get_compassion(
  const SexpFsm_ptr  self 
)
Gets the list of sexp expressions defining the set of compassion constraints for this machine.

Defined in SexpFsm.c

FlatHierarchy_ptr 
SexpFsm_get_hierarchy(
  const SexpFsm_ptr  self 
)
Returned hierarchy belongs to self and cannot be freely changed without indirectly modifying self as well. Copy the returned hierarchy before modifying it if you do not want to change self. Also, notice that the SexpFsm constructor copies the passed hierarchy.

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_init(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects init states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_input(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects all input states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_invar(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects invar states for all variables handled by self

Defined in SexpFsm.c

node_ptr 
SexpFsm_get_justice(
  const SexpFsm_ptr  self 
)
Gets the list of sexp expressions defining the set of justice constraints for this machine.

Defined in SexpFsm.c

SymbTable_ptr 
SexpFsm_get_symb_table(
  const SexpFsm_ptr  self 
)
This method can be called only when a valid BddEnc was passed to the class constructor (not NULL). Returned instance do not belongs to the caller and must _not_ be destroyed

Defined in SexpFsm.c

NodeList_ptr 
SexpFsm_get_symbols_list(
  const SexpFsm_ptr  self 
)
Returned instance belongs to self. Do not change not free it.

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_trans(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects all next states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_init(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the initial state for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_input(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the input relation for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_invar(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the state constraints for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_trans(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the transition relation for the variable "v".

Defined in SexpFsm.c

NodeList_ptr 
SexpFsm_get_vars_list(
  const SexpFsm_ptr  self 
)
Returned instance belongs to self. Do not change not free it.

Defined in SexpFsm.c

Set_t 
SexpFsm_get_vars(
  const SexpFsm_ptr  self 
)
Returned instance belongs to self. Do not change not free it.

Defined in SexpFsm.c

boolean 
SexpFsm_is_boolean(
  const SexpFsm_ptr  self 
)
Since a BoolSexpFsm derives from SexpFsm, a SexpFsm is not necessarily a scalar fsm. Use this method to distinguish scalar from boolean fsm when dealing with generic SexpFsm pointers.

Defined in SexpFsm.c

boolean 
SexpFsm_is_syntactically_universal(
  SexpFsm_ptr  self 
)
Checks if the SexpFsm is syntactically universal: Checks INIT, INVAR, TRANS, INPUT, JUSTICE, COMPASSION to be empty (ie: True Expr). In this case returns true, false otherwise

Defined in SexpFsm.c

void 
SexpFsm_self_check(
  const SexpFsm_ptr  self 
)
Self-check for the instance

Defined in SexpFsm.c

static int 
expr_get_curr_time(
  SymbTable_ptr  st, 
  node_ptr  expr, 
  hash_ptr  cache 
)
Private service of Expr_get_time

Side Effects None

Defined in Expr.c

static boolean 
expr_is_timed_aux(
  Expr_ptr  expr, 
  hash_ptr  cache 
)
Private service of Expr_is_timed. To represent 'true' in cache we use the constant 2 for 'false' we use 1 to avoid representation problems wrt Nil

Side Effects cache can be updated

Defined in Expr.c

static Expr_ptr 
expr_timed_to_untimed(
  SymbTable_ptr  st, 
  Expr_ptr  expr, 
  int  curr_time, 
  boolean  in_next, 
  hash_ptr  cache 
)
Converts a timed node into an untimed node

Side Effects None

Defined in Expr.c

static assoc_retval 
sexp_fsm_callback_var_fsm_free(
  char * key, 
  char * data, 
  char * arg 
)
Private callback that destroys a single variable fsm contained into the var fsm hash

Defined in SexpFsm.c

static void 
sexp_fsm_const_var_fsm_init(
  SexpFsm_ptr  self, 
  hash_ptr  simp_hash 
)
Formulae are simplified through sexp_fsm_simplify_expr. For this reason a simplification hash is required as input

Defined in SexpFsm.c

void 
sexp_fsm_copy_aux(
  const SexpFsm_ptr  self, 
  SexpFsm_ptr  copy 
)
private service for copying self to other

Defined in SexpFsm.c

static Object_ptr 
sexp_fsm_copy(
  const Object_ptr  object 
)
This is called by the virtual copy constructor

Defined in SexpFsm.c

void 
sexp_fsm_deinit(
  SexpFsm_ptr  self 
)
Initializes the vars fsm hash

Defined in SexpFsm.c

static void 
sexp_fsm_finalize(
  Object_ptr  object, 
  void* dummy 
)
Called by the class destructor

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_destroy(
  SexpFsm_ptr  self 
)
Private method, used internally

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_init(
  SexpFsm_ptr  self, 
  hash_ptr  simp_hash 
)
Formulae are simplified through sexp_fsm_simplify_expr. For this reason a simplification hash is required as input

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_insert_var(
  SexpFsm_ptr  self, 
  node_ptr  var, 
  VarFsm_ptr  varfsm 
)
Adds a var fsm to the internal hash. Private.

Defined in SexpFsm.c

static VarFsm_ptr 
sexp_fsm_hash_var_fsm_lookup_var(
  SexpFsm_ptr  self, 
  node_ptr  var 
)
Given a variable name, returns the corresponding variable fsm, or NULL if not found

Defined in SexpFsm.c

void 
sexp_fsm_init(
  SexpFsm_ptr  self, 
  const FlatHierarchy_ptr  hierarchy, 
  const Set_t  vars_set 
)
hierarchy is copied into an independent FlatHierarchy instance. If the new sexp must be based only on a set of variables, the hierarchy must be empty

Defined in SexpFsm.c

static Expr_ptr 
sexp_fsm_simplify_expr(
  SexpFsm_ptr  self, 
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
group identifies INVAR, TRANS or INIT group.

Defined in SexpFsm.c

static void 
simplifier_hash_add_expr(
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
group is INIT, INVAR or TRANS

Side Effects The hash can change

Defined in SexpFsm.c

static hash_ptr 
simplifier_hash_create(
    
)
This is used when creating cluster list from vars list

Defined in SexpFsm.c

static void 
simplifier_hash_destroy(
  hash_ptr  hash 
)
Call after sexp_fsm_cluster_hash_create

Defined in SexpFsm.c

static boolean 
simplifier_hash_query_expr(
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
Queries for an element in the hash, returns True if found

Defined in SexpFsm.c

static VarFsm_ptr 
var_fsm_create(
  Expr_ptr  init, 
  Expr_ptr  invar, 
  Expr_ptr  next 
)
Creates a var fsm

Defined in SexpFsm.c

static void 
var_fsm_destroy(
  VarFsm_ptr  self 
)
It does not destroy the init, trans and invar nodes. It destroys only the support nodes

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_init(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_input(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_invar(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_next(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static VarFsm_ptr 
var_fsm_synchronous_product(
  VarFsm_ptr  fsm1, 
  VarFsm_ptr  fsm2 
)
Any argument can be Nil. When both are Nil the product has all arguments true.

Defined in SexpFsm.c

 
(
    
)
Use only in debugging mode, as self-checking can be expensive

Defined in SexpFsm.c

Last updated on 2011/04/06 21h:13