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