SexpFsm_ptr 
SexpFsm_copy(
  const SexpFsm_ptr  self 
)
Copy costructor

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create_from_members(
  Expr_ptr  init, 
  Expr_ptr  invar, 
  Expr_ptr  trans, 
  Expr_ptr  input, 
  node_ptr  justice, 
  node_ptr  compassion, 
  const enum SexpFsmType  type 
)
This method is temporary exported to be used from the LTL side, to compile the table fsm. Warning: the variable FSMs will be not constructed, so the user cannot use methods to obtain the single variable fsm information.

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create(
  VarSet_ptr  vars_list, 
  node_ptr  justice, 
  node_ptr  compassion, 
  const enum SexpFsmType  type 
)
Costructor for a scalar and boolean sexp fsm

Defined in SexpFsm.c

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

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

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

boolean 
SexpFsm_is_boolean(
  const SexpFsm_ptr  self 
)
Returns true if self if a booleanized fsm, false if it is scalar

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_scalar_to_boolean(
  const SexpFsm_ptr  self 
)
Returns a copy if self is already booleanized

Defined in SexpFsm.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_copy_shared_structures(
  const SexpFsm_ptr  self, 
  SexpFsm_ptr  copy 
)
Call this to copy data from fsm belonging to the same family. This also increments the family counter

Defined in SexpFsm.c

static void 
sexp_fsm_create_shared_structures(
  SexpFsm_ptr  self 
)
Every time a fsm is created from scratch (i.e. via its constructor), a new family is created. When a fsm D is derived from an existing base fsm B, D belongs to the family of B

Defined in SexpFsm.c

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

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, 
  VarSet_ptr  vars_list 
)
Initializes the vars fsm hash

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

static void 
sexp_fsm_init(
  SexpFsm_ptr  self, 
  VarSet_ptr  vars_list, 
  node_ptr  justice, 
  node_ptr  compassion, 
  const boolean  booleanize 
)
Initializes either the boolean or scalar sexp fsm

Defined in SexpFsm.c

static Expr_ptr 
sexp_fsm_simplify_expr(
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group, 
  const boolean  booleanize 
)
group identifies INVAR, TRANS or INIT group. If booleanize is True, the expression will be also booleanized

Defined in SexpFsm.c

static void 
sexp_fsm_try_to_destroy_shared_structures(
  SexpFsm_ptr  self 
)
All structures will be destroyed only if the family counter reaches the zero value

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

Last updated on 2004/06/09 20h:03