void
BeFsm_apply_synchronous_product(
BeFsm_ptr self,
const BeFsm_ptr other
)
- Apply the synchronous product between self and other
modifying self
- Defined in
BeFsm.c
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 BoolSexpFsm_ptr bfsm
)
- Creates a new instance of the BeFsm class, getting
information from an instance of a boolean 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