BeFsm_ptr 
BeFsm_copy(
  BeFsm_ptr  self 
)
Creates a new independent copy of the given fsm instance. You must destroy the returned class instance by invoking the class destructor when you no longer need it.

See Also BeFsm_destroy
Defined in BeFsm.c

BeFsm_ptr 
BeFsm_create_from_sexp_fsm(
  BeEnc_ptr  be_enc, 
  const SexpFsm_ptr  bfsm 
)
Creates a new instance of the BeFsm class, getting information from an instance of Fsm_Sexp type.

See Also BeFsm_create BeFsm_destroy
Defined in BeFsm.c

BeFsm_ptr 
BeFsm_create(
  BeEnc_ptr  be_enc, 
  const be_ptr  init, 
  const be_ptr  invar, 
  const be_ptr  trans, 
  const node_ptr  list_of_be_fairness 
)
It gets init, invar, transition relation and the list of fairness in Boolean Expression format.

See Also BeFsm_destroy
Defined in BeFsm.c

void 
BeFsm_destroy(
  BeFsm_ptr  self 
)
Class BeFsm destructor

Side Effects self will be invalidated

See Also BeFsm_create BeFsm_create_from_sexp_fsm
Defined in BeFsm.c

BeEnc_ptr 
BeFsm_get_be_encoding(
  const BeFsm_ptr  self 
)
Returns the be encoding associated with the given fsm instance

Defined in BeFsm.c

node_ptr 
BeFsm_get_fairness_list(
  const BeFsm_ptr  self 
)
Returns the list of fairness stored in BE format into the given fsm instance

Defined in BeFsm.c

be_ptr 
BeFsm_get_init(
  const BeFsm_ptr  self 
)
Returns the initial states stored in BE format into the given fsm instance

Defined in BeFsm.c

be_ptr 
BeFsm_get_invar(
  const BeFsm_ptr  self 
)
Returns the invariants stored in BE format into the given fsm instance

Defined in BeFsm.c

be_ptr 
BeFsm_get_trans(
  const BeFsm_ptr  self 
)
Returns the transition relation stored in BE format into the given fsm instance

Defined in BeFsm.c

static void 
be_fsm_deinit(
  BeFsm_ptr  self 
)
Private service to deinitialize the internal members

Defined in BeFsm.c

static void 
be_fsm_init(
  BeFsm_ptr  self, 
  BeEnc_ptr  be_enc, 
  const be_ptr  init, 
  const be_ptr  invar, 
  const be_ptr  trans, 
  const node_ptr  list_of_be_fairness 
)
Private service to initialize the internal members

Side Effects self will change internally

Defined in BeFsm.c

Last updated on 2007/04/06 14h:44