NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableau.h File Reference

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

Go to the source code of this file.

Functions
be_ptr	Bmc_SBMCTableau_GetAllLoops (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l)
	Builds tableau for all possible loops in \[l, k\[, taking into account of fairness using Kepa/Timo method].
be_ptr	Bmc_SBMCTableau_GetLoopCondition (const BeEnc_ptr be_enc, const int k, const int l)
	Builds a tableau that constraints state k to be equal to state l. This is the condition for a path of length (k+1) to represent a (k-l)loop (new semantics).
be_ptr	Bmc_SBMCTableau_GetNoLoop (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k)
	Public interface for SBMC tableau-related functionalities.
be_ptr	Bmc_SBMCTableau_GetSingleLoop (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l)
	Builds tableau for a single loop. This function takes into account of fairness.

---

Function Documentation

be_ptr Bmc_SBMCTableau_GetAllLoops	(	const BeFsm_ptr	be_fsm,
		const node_ptr	ltl_wff,
		const int	k,
		const int	l
	)

Builds tableau for all possible loops in \[l, k\[, taking into account of fairness using Kepa/Timo method].

Description [Fairness is taken care of by adding it to the formula.]

SideEffects []

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Fairness is taken care of by adding it to the formula.

be_ptr Bmc_SBMCTableau_GetLoopCondition	(	const BeEnc_ptr	be_enc,
		const int	k,
		const int	l
	)

Builds a tableau that constraints state k to be equal to state l. This is the condition for a path of length (k+1) to represent a (k-l)loop (new semantics).

State l and state k are forced to represent the same state by conjuncting the if-and-only-if conditions {Vil<->Vik} between Vil (variable i at time l) and Vik (variable i at time k) for each variable Vi.

See also:

Bmc_Tableau_GetAllLoopsDisjunction

be_ptr Bmc_SBMCTableau_GetNoLoop	(	const BeFsm_ptr	be_fsm,
		const node_ptr	ltl_wff,
		const int	k
	)

Public interface for SBMC tableau-related functionalities.

Author:

Timo Latvala, Marco Roveri

Todo:

: Missing description

AutomaticStart

Builds tableau without loop Fairness is ignored

be_ptr Bmc_SBMCTableau_GetSingleLoop	(	const BeFsm_ptr	be_fsm,
		const node_ptr	ltl_wff,
		const int	k,
		const int	l
	)

Builds tableau for a single loop. This function takes into account of fairness.