NuSMV/code/nusmv/core/bmc/bmcModel.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/fsm/be/BeFsm.h"

Go to the source code of this file.

Functions
be_ptr	Bmc_Model_GetFairness (const BeFsm_ptr be_fsm, const int k, const int l)
	Generates and returns an expression representing all fairnesses in a conjunctioned form.
be_ptr	Bmc_Model_GetInit0 (const BeFsm_ptr be_fsm)
	Public interface for the model-related functionalities.
be_ptr	Bmc_Model_GetInitI (const BeFsm_ptr be_fsm, const int i)
	Retrieves the init states from the given fsm, and compiles them into a BE at time i.
be_ptr	Bmc_Model_GetInvarAtTime (const BeFsm_ptr be_fsm, const int time)
	Retrieves the invars from the given fsm, and compiles them into a BE at the given time.
be_ptr	Bmc_Model_GetPathNoInit (const BeFsm_ptr be_fsm, const int k)
	Returns the path for the model from 0 to k, taking into account the invariants (and no init).
be_ptr	Bmc_Model_GetPathWithInit (const BeFsm_ptr be_fsm, const int k)
	Returns the path for the model from 0 to k, taking into account initial conditions and invariants.
be_ptr	Bmc_Model_GetTransAtTime (const BeFsm_ptr be_fsm, const int time)
	Retrieves the trans from the given fsm, and compiles it into a MSatEnc at the given time.
be_ptr	Bmc_Model_GetUnrolling (const BeFsm_ptr be_fsm, const int j, const int k)
	Unrolls the transition relation from j to k, taking into account of invars.
be_ptr	Bmc_Model_Invar_Dual_forward_unrolling (const BeFsm_ptr be_fsm, const be_ptr invarspec, int i)
	Unrolls the transition relation from j to k, taking into account of invars.

---

Function Documentation

be_ptr Bmc_Model_GetFairness	(	const BeFsm_ptr	be_fsm,
		const int	k,
		const int	l
	)

Generates and returns an expression representing all fairnesses in a conjunctioned form.

Uses bmc_model_getFairness_aux which recursively calls itself to conjuctive all fairnesses by constructing a top-level 'and' operation. Moreover bmc_model_getFairness_aux calls the recursive function bmc_model_getSingleFairness, which resolves a single fairness as a disjunctioned expression in which each ORed element is a shifting of the single fairness across \[l, k\] if a loop exists. If no loop exists, nothing can be issued, so a falsity value is returned

See also:

bmc_model_getFairness_aux, bmc_model_getSingleFairness

be_ptr Bmc_Model_GetInit0

(

const BeFsm_ptr

be_fsm

)

Public interface for the model-related functionalities.

Author:

Roberto Cavada

Todo:

: Missing description

AutomaticStart

Retrieves the init states from the given fsm, and compiles them into a BE at time 0 Use this function instead of explicitly get the init from the fsm and shift them at time 0 using the vars manager layer.

See also:

Bmc_Model_GetInvarAtTime

be_ptr Bmc_Model_GetInitI	(	const BeFsm_ptr	be_fsm,
		const int	i
	)

Retrieves the init states from the given fsm, and compiles them into a BE at time i.

Use this function instead of explicitly get the init from the fsm and shift them at time i using the vars manager layer.

See also:

Bmc_Model_GetInvarAtTime

be_ptr Bmc_Model_GetInvarAtTime	(	const BeFsm_ptr	be_fsm,
		const int	time
	)

Retrieves the invars from the given fsm, and compiles them into a BE at the given time.

Use this function instead of explicitly get the invar from the fsm and shift them at the requested time using the vars manager layer.

See also:

Bmc_Model_GetInit0

be_ptr Bmc_Model_GetPathNoInit	(	const BeFsm_ptr	be_fsm,
		const int	k
	)

Returns the path for the model from 0 to k, taking into account the invariants (and no init).

See also:

Bmc_Model_GetPathWithInit

be_ptr Bmc_Model_GetPathWithInit	(	const BeFsm_ptr	be_fsm,
		const int	k
	)

Returns the path for the model from 0 to k, taking into account initial conditions and invariants.

See also:

Bmc_Model_GetPathNoInit

be_ptr Bmc_Model_GetTransAtTime	(	const BeFsm_ptr	be_fsm,
		const int	time
	)

Retrieves the trans from the given fsm, and compiles it into a MSatEnc at the given time.

Use this function instead of explicitly get the trans from the fsm and shift it at the requested time using the vars manager layer

None

be_ptr Bmc_Model_GetUnrolling	(	const BeFsm_ptr	be_fsm,
		const int	j,
		const int	k
	)

Unrolls the transition relation from j to k, taking into account of invars.

Using of invars over next variables instead of the previuos variables is a specific implementation aspect

See also:

Bmc_Model_GetPathWithInit, Bmc_Model_GetPathNoInit

be_ptr Bmc_Model_Invar_Dual_forward_unrolling	(	const BeFsm_ptr	be_fsm,
		const be_ptr	invarspec,
		int	i
	)

Unrolls the transition relation from j to k, taking into account of invars.

Using of invars over previous variables instead of the next variables is a specific implementation aspect