BeFsm Struct Reference

Public interface of the Finite State Machine class in BE format. More...

#include <BeFsm.h>

Related Functions
(Note that these are not member functions.)
void	BeFsm_apply_synchronous_product (BeFsm_ptr self, const BeFsm_ptr other)
	Apply the synchronous product between self and other modifying self.
BeFsm_ptr	BeFsm_copy (BeFsm_ptr self)
	Copy constructor for class BeFsm.
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)
	Class BeFsm constructor.
BeFsm_ptr	BeFsm_create_from_sexp_fsm (BeEnc_ptr be_enc, const BoolSexpFsm_ptr bfsm)
	Class BeFsm constructor.
void	BeFsm_destroy (BeFsm_ptr self)
	Class BeFsm destructor.
BeEnc_ptr	BeFsm_get_be_encoding (const BeFsm_ptr self)
	Returns the be encoding associated with the given fsm instance.
node_ptr	BeFsm_get_fairness_list (const BeFsm_ptr self)
	Returns the list of fairness stored in BE format into the given fsm instance.
be_ptr	BeFsm_get_init (const BeFsm_ptr self)
	Returns the initial states stored in BE format into the given fsm instance.
be_ptr	BeFsm_get_invar (const BeFsm_ptr self)
	Returns the invariants stored in BE format into the given fsm instance.
be_ptr	BeFsm_get_trans (const BeFsm_ptr self)
	Returns the transition relation stored in BE format into the given fsm instance.

---

Detailed Description

Public interface of the Finite State Machine class in BE format.

Author:

Roberto Cavada

Todo:

: Missing description

This is the BeFsm accessor type

---

Friends And Related Function Documentation

void BeFsm_apply_synchronous_product	(	BeFsm_ptr	self,
		const BeFsm_ptr	other
	)			[related]

Apply the synchronous product between self and other modifying self.

BeFsm_ptr BeFsm_copy

(

BeFsm_ptr

self

)

[related]

Copy constructor for class BeFsm.

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

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
	)			[related]

Class BeFsm constructor.

AutomaticStart

It gets init, invar, transition relation and the list of fairness in Boolean Expression format.

See also:

BeFsm_destroy

BeFsm_ptr BeFsm_create_from_sexp_fsm	(	BeEnc_ptr	be_enc,
		const BoolSexpFsm_ptr	bfsm
	)			[related]

Class BeFsm constructor.

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

void BeFsm_destroy

(

BeFsm_ptr

self

)

[related]

Class BeFsm destructor.

self will be invalidated

See also:

BeFsm_create, BeFsm_create_from_sexp_fsm

BeEnc_ptr BeFsm_get_be_encoding

(

const BeFsm_ptr

self

)

[related]

Returns the be encoding associated with the given fsm instance.

node_ptr BeFsm_get_fairness_list

(

const BeFsm_ptr

self

)

[related]

Returns the list of fairness stored in BE format into the given fsm instance.

be_ptr BeFsm_get_init

(

const BeFsm_ptr

self

)

[related]

Returns the initial states stored in BE format into the given fsm instance.

be_ptr BeFsm_get_invar

(

const BeFsm_ptr

self

)

[related]

Returns the invariants stored in BE format into the given fsm instance.

be_ptr BeFsm_get_trans

(

const BeFsm_ptr

self

)

[related]

Returns the transition relation stored in BE format into the given fsm instance.

---

The documentation for this struct was generated from the following file:

• NuSMV/code/nusmv/core/fsm/be/BeFsm.h