FsmBuilder Struct Reference

Public interface for a high level object that can contruct FSMs. More...

#include <FsmBuilder.h>

Related Functions
(Note that these are not member functions.)
ClusterList_ptr	FsmBuilder_clusterize_expr (FsmBuilder_ptr self, BddEnc_ptr enc, Expr_ptr expr)
	Given an expression, returns a bdd ClusterList with each conjuction occurring into expr contained in each cluster of the list.
FsmBuilder_ptr	FsmBuilder_create (NuSMVEnv_ptr env)
	The constructor creates a BddEnc and self handles it.
BddFsm_ptr	FsmBuilder_create_bdd_fsm (const FsmBuilder_ptr self, BddEnc_ptr enc, const SexpFsm_ptr sexp_fsm, const TransType trans_type)
	Creates a BddFsm instance from a given SexpFsm.
BddFsm_ptr	FsmBuilder_create_bdd_fsm_of_vars (const FsmBuilder_ptr self, const SexpFsm_ptr sexp_fsm, const TransType trans_type, BddEnc_ptr enc, BddVarSet_ptr state_vars_cube, BddVarSet_ptr input_vars_cube, BddVarSet_ptr next_state_vars_cube)
	Creates a BddFsm instance from a given SexpFsm.
BoolSexpFsm_ptr	FsmBuilder_create_boolean_sexp_fsm (const FsmBuilder_ptr self, FlatHierarchy_ptr flat_hierarchy, const Set_t vars, BddEnc_ptr bdd_enc, SymbLayer_ptr det_layer)
	Creates a new boolean sexp fsm, taking into account of the current variables ordering, or the trans ordering file when specified by the user. When used, the latter overrides the former.
SexpFsm_ptr	FsmBuilder_create_scalar_sexp_fsm (const FsmBuilder_ptr self, FlatHierarchy_ptr flat_hierarchy, const Set_t vars_list)
	Creates a new scalar sexp fsm.
void	FsmBuilder_destroy (FsmBuilder_ptr self)
	Class FsmBuilder destructor.

---

Detailed Description

Public interface for a high level object that can contruct FSMs.

Author:

Roberto Cavada Declares the interface of an high-level object that lives at top-level, that is used to help contruction of FSMs. It can control information that are not shared between lower levels, so it can handle with objects that have not the full knowledge of the whole system

FSM builder class constructor

---

Friends And Related Function Documentation

ClusterList_ptr FsmBuilder_clusterize_expr	(	FsmBuilder_ptr	self,
		BddEnc_ptr	enc,
		Expr_ptr	expr
	)			[related]

Given an expression, returns a bdd ClusterList with each conjuction occurring into expr contained in each cluster of the list.

Each cluster into the list represents a piece of transition relation. If the given expression contains duplicates, they will not occur into the returned cluster list. Returned list should be destroyed by the caller.

FsmBuilder_ptr FsmBuilder_create

(

NuSMVEnv_ptr

env

)

[related]

The constructor creates a BddEnc and self handles it.

Environment requisites: None, but for later uses will need some basic structures (NodeMgr, ErrorMgr, DDMgr, OptsHandler, StreamMgr)

BddFsm_ptr FsmBuilder_create_bdd_fsm	(	const FsmBuilder_ptr	self,
		BddEnc_ptr	enc,
		const SexpFsm_ptr	sexp_fsm,
		const TransType	trans_type
	)			[related]

Creates a BddFsm instance from a given SexpFsm.

Note: all variables from provided encoding will go to the BDD FSM. Use FsmBuilder_create_bdd_fsm_of_vars if only SOME variables should be taken into account.

BddFsm_ptr FsmBuilder_create_bdd_fsm_of_vars	(	const FsmBuilder_ptr	self,
		const SexpFsm_ptr	sexp_fsm,
		const TransType	trans_type,
		BddEnc_ptr	enc,
		BddVarSet_ptr	state_vars_cube,
		BddVarSet_ptr	input_vars_cube,
		BddVarSet_ptr	next_state_vars_cube
	)			[related]

Creates a BddFsm instance from a given SexpFsm.

It is the same as FsmBuilder_create_bdd_fsm except that the cubes of state, input and next-state variables are given explicitly.

Note: The functions will take a copy of provided cubes.

BoolSexpFsm_ptr FsmBuilder_create_boolean_sexp_fsm	(	const FsmBuilder_ptr	self,
		FlatHierarchy_ptr	flat_hierarchy,
		const Set_t	vars,
		BddEnc_ptr	bdd_enc,
		SymbLayer_ptr	det_layer
	)			[related]

Creates a new boolean sexp fsm, taking into account of the current variables ordering, or the trans ordering file when specified by the user. When used, the latter overrides the former.

The caller becomes the owner of the returned object. An exception may occur if the trans cluster ordering is specified and an error occurs while parsing it.

SexpFsm_ptr FsmBuilder_create_scalar_sexp_fsm	(	const FsmBuilder_ptr	self,
		FlatHierarchy_ptr	flat_hierarchy,
		const Set_t	vars_list
	)			[related]

Creates a new scalar sexp fsm.

The caller becomes the owner of the returned object

void FsmBuilder_destroy

(

FsmBuilder_ptr

self

)

[related]

Class FsmBuilder destructor.

---

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

• NuSMV/code/nusmv/core/fsm/FsmBuilder.h