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

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

Go to the source code of this file.

Functions
be_ptr	Bmc_Tableau_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].
be_ptr	Bmc_Tableau_GetAllLoopsDepth1 (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k)
	Builds tableau for all possible loops in \[l, k\], in the particular case in which depth is 1. This function takes into account of fairness.
be_ptr	Bmc_Tableau_GetLtlTableau (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l)
	Builds a tableau for the LTL at length k with loopback l (single loop, no loop and all loopbacks are allowed).
be_ptr	Bmc_Tableau_GetNoLoop (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k)
	Public interface for tableau-related functionalities.
be_ptr	Bmc_Tableau_GetSingleLoop (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\], in the particular case in which depth is 1. This function takes into account of fairness.

---

Function Documentation

be_ptr Bmc_Tableau_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].

Description [Each tableau takes into account of fairnesses relative to its step. All tableau are collected together into a disjunctive form.]

SideEffects []

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Each tableau takes into account of fairnesses relative to its step. All tableau are collected together into a disjunctive form.

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

Builds tableau for all possible loops in \[l, k\], in the particular case in which depth is 1. This function takes into account of fairness.

Builds the tableau in the case depth==1 as suggested by R. Sebastiani

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

Builds a tableau for the LTL at length k with loopback l (single loop, no loop and all loopbacks are allowed).

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

Public interface for tableau-related functionalities.

Author:

Roberto Cavada

Todo:

: Missing description

AutomaticStart

Builds tableau without loop at time zero, taking into account of fairness Fairness evaluate to true if there are not fairness in the model, otherwise them evaluate to false because of no loop

be_ptr Bmc_Tableau_GetSingleLoop	(	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\], in the particular case in which depth is 1. This function takes into account of fairness.

Builds the tableau in the case depth==1 as suggested by R. Sebastiani