SexpFsm Struct Reference

Private and protected interface of class 'SexpFsm'. More...

#include <SexpFsm_private.h>

Public Member Functions
	INHERITS_FROM (Object)
Data Fields
node_ptr	const_var_fsm
int *	family_counter
hash_ptr	hash_var_fsm
FlatHierarchy_ptr	hierarchy
boolean	inlining
boolean	is_boolean
SymbTable_ptr	st
NodeList_ptr	symbols
Set_t	vars_set
Related Functions
(Note that these are not member functions.)
void	sexp_fsm_copy_aux (const SexpFsm_ptr self, SexpFsm_ptr copy)
	private service for copying self to other
void	sexp_fsm_deinit (SexpFsm_ptr self)
	DeInitializes the vars fsm hash.
void	sexp_fsm_init (SexpFsm_ptr self, const FlatHierarchy_ptr hierarchy, const Set_t vars_set)
	Initializes the sexp fsm.
void	SexpFsm_apply_synchronous_product (SexpFsm_ptr self, SexpFsm_ptr other)
	Performs the synchronous product of two FSMs.
SexpFsm_ptr	SexpFsm_copy (const SexpFsm_ptr self)
	Copy costructor.
SexpFsm_ptr	SexpFsm_create (const FlatHierarchy_ptr hierarchy, const Set_t vars_set)
	Costructor for a scalar sexp fsm.
SexpFsm_ptr	SexpFsm_create_predicate_normalised_copy (const SexpFsm_ptr self, PredicateNormaliser_ptr normaliser)
	Copy the Sexp FSM and perform predicate-normalisation on all the expressions.
void	SexpFsm_destroy (SexpFsm_ptr self)
	Destructor.
node_ptr	SexpFsm_get_compassion (const SexpFsm_ptr self)
FlatHierarchy_ptr	SexpFsm_get_hierarchy (const SexpFsm_ptr self)
	Returns the internal complete hierarchy.
Expr_ptr	SexpFsm_get_init (const SexpFsm_ptr self)
	Returns an Expr that collects init states for all variables handled by self.
Expr_ptr	SexpFsm_get_input (const SexpFsm_ptr self)
	Returns an Expr that collects all input states for all variables handled by self.
Expr_ptr	SexpFsm_get_invar (const SexpFsm_ptr self)
	Returns an Expr that collects invar states for all variables handled by self.
node_ptr	SexpFsm_get_justice (const SexpFsm_ptr self)
SymbTable_ptr	SexpFsm_get_symb_table (const SexpFsm_ptr self)
	Returns the symbol table that is connected to the BoolEnc instance connected to self.
NodeList_ptr	SexpFsm_get_symbols_list (const SexpFsm_ptr self)
	Returns the set of symbols in the FSM.
Expr_ptr	SexpFsm_get_trans (const SexpFsm_ptr self)
	Returns an Expr that collects all next states for all variables handled by self.
Expr_ptr	SexpFsm_get_var_init (const SexpFsm_ptr self, node_ptr v)
Expr_ptr	SexpFsm_get_var_input (const SexpFsm_ptr self, node_ptr v)
	Gets the sexp expression defining the input relation for the variable "v".
Expr_ptr	SexpFsm_get_var_invar (const SexpFsm_ptr self, node_ptr v)
Expr_ptr	SexpFsm_get_var_trans (const SexpFsm_ptr self, node_ptr v)
Set_t	SexpFsm_get_vars (const SexpFsm_ptr self)
	Returns the set of variables in the FSM.
NodeList_ptr	SexpFsm_get_vars_list (const SexpFsm_ptr self)
	Returns the set of variables in the FSM.
boolean	SexpFsm_is_boolean (const SexpFsm_ptr self)
	Use to check if this FSM is a scalar or boolean fsm.
boolean	SexpFsm_is_syntactically_universal (SexpFsm_ptr self)
	Checks if the SexpFsm is syntactically universal.
void	SexpFsm_self_check (const SexpFsm_ptr self)
	Self-check for the instance.

Detailed Description

Private and protected interface of class 'SexpFsm'.

The SexpFsm API.

Author:: Roberto Cavada This file can be included only by derived and friend classes

SexpFsm class definition derived from class Object

See also:: Base class Object

Author:: Roberto Cavada Class SexpFsm declaration

The SexpFsm type The SexpFsm type

Member Function Documentation

SexpFsm::INHERITS_FROM ( Object )

Friends And Related Function Documentation

void sexp_fsm_copy_aux	(	const SexpFsm_ptr	self,
		SexpFsm_ptr	copy
	)			`[related]`

private service for copying self to other

void sexp_fsm_deinit ( SexpFsm_ptr self ) [related]

DeInitializes the vars fsm hash.

void sexp_fsm_init	(	SexpFsm_ptr	self,
		const FlatHierarchy_ptr	hierarchy,
		const Set_t	vars_set
	)			`[related]`

Initializes the sexp fsm.

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

void SexpFsm_apply_synchronous_product	(	SexpFsm_ptr	self,
		SexpFsm_ptr	other
	)			`[related]`

Performs the synchronous product of two FSMs.

The result goes into self, no changes to other.

self will change

SexpFsm_ptr SexpFsm_copy ( const SexpFsm_ptr self ) [related]

Copy costructor.

SexpFsm_ptr SexpFsm_create	(	const FlatHierarchy_ptr	hierarchy,
		const Set_t	vars_set
	)			`[related]`

Costructor for a scalar sexp fsm.

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)

SexpFsm_ptr SexpFsm_create_predicate_normalised_copy	(	const SexpFsm_ptr	self,
		PredicateNormaliser_ptr	normaliser
	)			`[related]`

Copy the Sexp FSM and perform predicate-normalisation on all the expressions.

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.

SexpFsm_copy

void SexpFsm_destroy ( SexpFsm_ptr self ) [related]

Destructor.

node_ptr SexpFsm_get_compassion ( const SexpFsm_ptr self ) [related]

Gets the list of sexp expressions defining the set of compassion constraints for this machine.

FlatHierarchy_ptr SexpFsm_get_hierarchy ( const SexpFsm_ptr self ) [related]

Returns the internal complete hierarchy.

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.

Expr_ptr SexpFsm_get_init ( const SexpFsm_ptr self ) [related]

Returns an Expr that collects init states for all variables handled by self.

Expr_ptr SexpFsm_get_input ( const SexpFsm_ptr self ) [related]

Returns an Expr that collects all input states for all variables handled by self.

Expr_ptr SexpFsm_get_invar ( const SexpFsm_ptr self ) [related]

Returns an Expr that collects invar states for all variables handled by self.

node_ptr SexpFsm_get_justice ( const SexpFsm_ptr self ) [related]

Gets the list of sexp expressions defining the set of justice constraints for this machine.

SymbTable_ptr SexpFsm_get_symb_table ( const SexpFsm_ptr self ) [related]

Returns the symbol table that is connected to the BoolEnc instance connected to 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

NodeList_ptr SexpFsm_get_symbols_list ( const SexpFsm_ptr self ) [related]

Returns the set of symbols in the FSM.

Returned instance belongs to self. Do not change not free it.

Expr_ptr SexpFsm_get_trans ( const SexpFsm_ptr self ) [related]

Returns an Expr that collects all next states for all variables handled by self.

Expr_ptr SexpFsm_get_var_init	(	const SexpFsm_ptr	self,
		node_ptr	v
	)			`[related]`

Gets the sexp expression defining the initial state for the variable "v".

Expr_ptr SexpFsm_get_var_input	(	const SexpFsm_ptr	self,
		node_ptr	v
	)			`[related]`

Gets the sexp expression defining the input relation for the variable "v".

Expr_ptr SexpFsm_get_var_invar	(	const SexpFsm_ptr	self,
		node_ptr	v
	)			`[related]`

Gets the sexp expression defining the state constraints for the variable "v".

Expr_ptr SexpFsm_get_var_trans	(	const SexpFsm_ptr	self,
		node_ptr	v
	)			`[related]`

Gets the sexp expression defining the transition relation for the variable "v".

Set_t SexpFsm_get_vars ( const SexpFsm_ptr self ) [related]

Returns the set of variables in the FSM.

Returned instance belongs to self. Do not change not free it.

NodeList_ptr SexpFsm_get_vars_list ( const SexpFsm_ptr self ) [related]

Returns the set of variables in the FSM.

Returned instance belongs to self. Do not change not free it.

boolean SexpFsm_is_boolean ( const SexpFsm_ptr self ) [related]

Use to check if this FSM is a scalar or boolean fsm.

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.

boolean SexpFsm_is_syntactically_universal ( SexpFsm_ptr self ) [related]

Checks if the SexpFsm is syntactically universal.

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

void SexpFsm_self_check ( const SexpFsm_ptr self ) [related]

Self-check for the instance.