NuSMV/code/nusmv/core/mc/mc.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/fsm/bdd/BddFsm.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/opt/opt.h"

Go to the source code of this file.

Data Structures
struct	McCheckInvarOpts
	Fair CTL model checking algorithms. External header file. More...
Defines
#define	MC_CHECK_INVAR_OPTS_INVALID   -1
Functions
BddStates	abu (BddFsm_ptr, BddStates, BddStates, int, int)
	Set of states satisfying A\[f U^{inf..sup} g\].
BddStates	au (BddFsm_ptr, BddStates, BddStates)
	Set of states satisfying A\[f U g\].
BddStates	ebf (BddFsm_ptr, BddStates, int, int)
	Set of states satisfying EF^{inf..sup}(g).
BddStates	ebg (BddFsm_ptr, BddStates, int, int)
	Set of states satisfying EG^{inf..sup}(g).
BddStates	ebu (BddFsm_ptr, BddStates, BddStates, int, int)
	Set of states satisfying E\[f U^{inf..sup} g\].
BddStates	ef (BddFsm_ptr, BddStates)
	Set of states satisfying EF(g).
BddStates	eg (BddFsm_ptr, BddStates)
	Set of states satisfying EF(g).
BddStates	eu (BddFsm_ptr, BddStates, BddStates)
	Set of states satisfying E\[ f U g \].
int	eval_compute (BddFsm_ptr, BddEnc_ptr enc, node_ptr, node_ptr)
	Computes shortest and longest length of the path between two set of states.
bdd_ptr	eval_ctl_spec (BddFsm_ptr, BddEnc_ptr enc, node_ptr, node_ptr)
	Compile a CTL formula into BDD and performs Model Checking.
node_ptr	eval_formula_list (BddFsm_ptr, BddEnc_ptr enc, node_ptr, node_ptr)
	This function takes a list of formulas, and returns the list of their BDDs.
BddStates	ex (BddFsm_ptr, BddStates)
	Set of states satisfying EX(g).
node_ptr	explain (BddFsm_ptr, BddEnc_ptr, node_ptr, node_ptr, node_ptr)
	Counterexamples and witnesses generator.
void	free_formula_list (DDMgr_ptr, node_ptr)
	Frees a list of BDD as generated by eval_formula_list.
node_ptr	make_AG_counterexample (BddFsm_ptr, BddStates)
	This function constructs a counterexample starting from state target_state.
int	maxu (BddFsm_ptr, bdd_ptr, bdd_ptr)
	This function computes the maximum length of the shortest path from f to g.
int	Mc_check_invar (NuSMVEnv_ptr env, Prop_ptr prop, McCheckInvarOpts *options)
	Performs model checking of invariants.
int	Mc_check_psl_property (NuSMVEnv_ptr env, Prop_ptr prop)
	Top-level function for mc of PSL properties.
int	Mc_check_psl_spec (const NuSMVEnv_ptr env, const int prop_no)
void	Mc_CheckAGOnlySpec (NuSMVEnv_ptr env, Prop_ptr prop)
	This function checks for SPEC of the form AG alpha in "context".
void	Mc_CheckCompute (NuSMVEnv_ptr env, Prop_ptr prop)
	Compute quantitative characteristics on the model.
void	Mc_CheckCTLSpec (NuSMVEnv_ptr env, Prop_ptr prop)
	Verifies that M,s0 |= alpha.
void	Mc_CheckInvar (NuSMVEnv_ptr env, Prop_ptr prop)
	Verifies that M,s0 |= AG alpha.
void	Mc_CheckInvar_With_Strategy (NuSMVEnv_ptr env, Prop_ptr prop, Check_Strategy strategy, Trace_ptr *trace, boolean silent)
	Verifies that M,s0 |= AG alpha with the specified strategy.
void	Mc_CheckInvar_With_Strategy_And_Symbols (NuSMVEnv_ptr env, Prop_ptr prop, Check_Strategy strategy, Trace_ptr *trace, boolean silent, NodeList_ptr symbols)
	Verifies that M,s0 |= AG alpha with the specified strategy.
void	Mc_CheckInvarSilently (NuSMVEnv_ptr env, Prop_ptr prop, Trace_ptr *trace)
	Verifies that M,s0 |= AG alpha WITHOUT print results or counterexamples.
void	Mc_CheckLanguageEmptiness (NuSMVEnv_ptr env, const BddFsm_ptr fsm, boolean allinit, boolean verbose)
	Checks whether the language is empty.
Trace_ptr	Mc_create_trace_from_bdd_state_input_list (const BddEnc_ptr bdd_enc, const NodeList_ptr symbols, const char *desc, const TraceType type, node_ptr path)
	Creates a trace out of a < S (i, S)* > bdd list.
Trace_ptr	Mc_fill_trace_from_bdd_state_input_list (const BddEnc_ptr bdd_enc, Trace_ptr trace, node_ptr path)
	Fills the given trace out of a < S (i, S)* > bdd list.
void	Mc_trace_step_put_input_from_bdd (Trace_ptr trace, TraceIter step, BddEnc_ptr bdd_enc, bdd_ptr bdd)
	Populates a trace step with input assignments.
void	Mc_trace_step_put_state_from_bdd (Trace_ptr trace, TraceIter step, BddEnc_ptr bdd_enc, bdd_ptr bdd)
	Populates a trace step with state assignments.
void	McCheckInvarOpts_init (McCheckInvarOpts *options, NuSMVEnv_ptr env)
void	McCheckInvarOpts_init_invalid (McCheckInvarOpts *options)
boolean	McCheckInvarOpts_is_valid (McCheckInvarOpts *options)
int	minu (BddFsm_ptr, bdd_ptr, bdd_ptr)
	Computes the minimum length of the shortest path from f to g.
void	print_compute (OStream_ptr file, Prop_ptr, Prop_PrintFmt fmt)
	Prints out a COMPUTE specification.
void	print_invar (OStream_ptr file, Prop_ptr n, Prop_PrintFmt fmt)
	Print an invariant specification.
void	print_spec (OStream_ptr file, Prop_ptr prop, Prop_PrintFmt fmt)
	Prints out a CTL specification.

---

Define Documentation

#define MC_CHECK_INVAR_OPTS_INVALID   -1

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

BddStates abu	(	BddFsm_ptr	,
		BddStates	,
		BddStates	,
		int	,
		int
	)

Set of states satisfying A\[f U^{inf..sup} g\].

Computes the set of states satisfying A\[f U^{inf..sup} g\].

See also:

au

BddStates au	(	BddFsm_ptr	,
		BddStates	,
		BddStates
	)

Set of states satisfying A\[f U g\].

Computes the set of states satisfying A\[f U g\].

See also:

ax af ex ef

BddStates ebf	(	BddFsm_ptr	,
		BddStates	,
		int	,
		int
	)

Set of states satisfying EF^{inf..sup}(g).

Computes the set of states satisfying EF^{inf..sup}(g).

See also:

ef

BddStates ebg	(	BddFsm_ptr	,
		BddStates	,
		int	,
		int
	)

Set of states satisfying EG^{inf..sup}(g).

Computes the set of states satisfying EG^{inf..sup}(g).

See also:

eg

BddStates ebu	(	BddFsm_ptr	,
		BddStates	,
		BddStates	,
		int	,
		int
	)

Set of states satisfying E\[f U^{inf..sup} g\].

Computes the set of states satisfying E\[f U^{inf..sup} g\].

See also:

eu

BddStates ef	(	BddFsm_ptr	,
		BddStates
	)

Set of states satisfying EF(g).

Computes the set of states satisfying EF(g).

See also:

eu ex

BddStates eg	(	BddFsm_ptr	,
		BddStates
	)

Set of states satisfying EF(g).

Computes the set of states satisfying EG(g).

See also:

eu ex

BddStates eu	(	BddFsm_ptr	,
		BddStates	,
		BddStates
	)

Set of states satisfying E\[ f U g \].

Computes the set of states satisfying E\[ f U g \].

See also:

ebu

int eval_compute	(	BddFsm_ptr	,
		BddEnc_ptr	enc,
		node_ptr	,
		node_ptr
	)

Computes shortest and longest length of the path between two set of states.

This function performs the invocation of the routines to compute the length of the shortest and longest execution path between two set of states s_1 and s_2.

See also:

eval_ctl_spec

bdd_ptr eval_ctl_spec	(	BddFsm_ptr	,
		BddEnc_ptr	enc,
		node_ptr	,
		node_ptr
	)

Compile a CTL formula into BDD and performs Model Checking.

Compile a CTL formula into BDD and performs Model Checking.

See also:

eval_compute

node_ptr eval_formula_list	(	BddFsm_ptr	,
		BddEnc_ptr	enc,
		node_ptr	,
		node_ptr
	)

This function takes a list of formulas, and returns the list of their BDDs.

This function takes as input a list of formulae, and return as output the list of the corresponding BDDs, obtained by evaluating each formula in the given context.

BddStates ex	(	BddFsm_ptr	,
		BddStates
	)

Set of states satisfying EX(g).

Computes the set of states satisfying EX(g).

See also:

eu ef eg

node_ptr explain	(	BddFsm_ptr	,
		BddEnc_ptr	,
		node_ptr	,
		node_ptr	,
		node_ptr
	)

Counterexamples and witnesses generator.

This function takes as input a CTL formula and returns a witness showing how the given formula does not hold. The result consists of a list of states (i.e. an execution trace) that leads to a state in which the given formula does not hold.

See also:

explain_recur ex_explain eu_explain eg_explain ebg_explain ebu_explain

void free_formula_list	(	DDMgr_ptr	,
		node_ptr
	)

Frees a list of BDD as generated by eval_formula_list.

Frees a list of BDD as generated by eval_formula_list

See also:

eval_formula_list

node_ptr make_AG_counterexample	(	BddFsm_ptr	,
		BddStates
	)

This function constructs a counterexample starting from state target_state.

Compute a counterexample starting from a given state. Returned counterexample is a sequence of "state (input, state)*"

int maxu	(	BddFsm_ptr	,
		bdd_ptr	,
		bdd_ptr
	)

This function computes the maximum length of the shortest path from f to g.

This function computes the maximum length of the shortest path from f to g. It starts from !g and proceeds backward until no states in f can be found. In other words, it looks for the maximum length of f->AG!g. Notice that this function works correctly only if -f option is used.

Returns -1 if infinity, -2 if undefined

See also:

minu

int Mc_check_invar	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		McCheckInvarOpts *	options
	)

Performs model checking of invariants.

int Mc_check_psl_property	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

Top-level function for mc of PSL properties.

The parameters are:

• prop is the PSL property to be checked

None

int Mc_check_psl_spec	(	const NuSMVEnv_ptr	env,
		const int	prop_no
	)

Performs fair bdd-based PSL model checking.

void Mc_CheckAGOnlySpec	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

This function checks for SPEC of the form AG alpha in "context".

The implicit assumption is that "spec" must be an AG formula (i.e. it must contain only conjunctions and AG's). No attempt is done to normalize the formula (e.g. push negations). The AG mode relies on the previous computation and storage of the reachable state space (reachable_states_layers), they are used in counterexample computation.

See also:

check_ctlspec

void Mc_CheckCompute	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

Compute quantitative characteristics on the model.

Compute the given quantitative characteristics on the model.

void Mc_CheckCTLSpec	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

Verifies that M,s0 |= alpha.

Verifies that M,s0 |= alpha using the fair CTL model checking.

void Mc_CheckInvar	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)

Verifies that M,s0 |= AG alpha.

Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy read from the option variable.

See also:

check_ctlspec check_ltlspec Mc_CheckInvar_With_Strategy

void Mc_CheckInvar_With_Strategy	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		Check_Strategy	strategy,
		Trace_ptr *	trace,
		boolean	silent
	)

Verifies that M,s0 |= AG alpha with the specified strategy.

Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy given in input

If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location.

The result of model checking is stored in the given property.

See also:

check_ctlspec check_ltlspec Mc_CheckInvar

void Mc_CheckInvar_With_Strategy_And_Symbols	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		Check_Strategy	strategy,
		Trace_ptr *	trace,
		boolean	silent,
		NodeList_ptr	symbols
	)

Verifies that M,s0 |= AG alpha with the specified strategy.

Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy given in input.

If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location. A trace is created for variables and defines in 'symbols'. If trace is not required 'symbols' can be NULL.

The result of model checking is stored in the given property.

See also:

check_ctlspec check_ltlspec Mc_CheckInvar

void Mc_CheckInvarSilently	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		Trace_ptr *	trace
	)

Verifies that M,s0 |= AG alpha WITHOUT print results or counterexamples.

Verifies that M,s0 |= AG alpha, with alpha propositional. Uses strategy read from the option variable.

If opt_counter_examples is setted and trace is not null, then a trace is stored (and must be released by caller) in trace parameter location.

The result of model checking is stored in the given property.

See also:

check_ctlspec check_ltlspec Mc_CheckInvar_With_Strategy

void Mc_CheckLanguageEmptiness	(	NuSMVEnv_ptr	env,
		const BddFsm_ptr	fsm,
		boolean	allinit,
		boolean	verbose
	)

Checks whether the language is empty.

Checks whether the language is empty. Basically just a wrapper function that calls the language emptiness algorithm given by the value of the oreg_justice_emptiness_bdd_algorithm option.

If allinit is true the check is performed by verifying whether all initial states are included in the set of fair states. If it is the case from all initial states there exists a fair path and thus the language is not empty. On the other hand, if allinit is false, the check is performed by verifying whether there exists at least one initial state that is also a fair state. In this case there is an initial state from which it starts a fair path and thus the lnaguage is not empty. allinit is not supported for forward Emerson-Lei.

Depending on the global option use_reachable_states the set of fair states computed can be restricted to reachable states only. In this latter case the check can be further simplified. Forward Emerson-Lei requires forward_search and use_reachable_states to be enabled.

If verbose is true, then some information on the set of initial states is printed out too. verbose is ignored for forward Emerson-Lei.

None

See also:

mc_check_language_emptiness_el_bwd, mc_check_language_emptiness_el_fwd

Trace_ptr Mc_create_trace_from_bdd_state_input_list	(	const BddEnc_ptr	bdd_enc,
		const NodeList_ptr	symbols,
		const char *	desc,
		const TraceType	type,
		node_ptr	path
	)

Creates a trace out of a < S (i, S)* > bdd list.

Creates a trace out of a < S (i, S)* > bdd list. The built trace is non-volatile. For more control over the built trace, please see Mc_fill_trace_from_bdd_state_input_list

none

See also:

Trace_create, Bmc_create_trace_from_cnf_model, Mc_fill_trace_from_bdd_state_input_list

Trace_ptr Mc_fill_trace_from_bdd_state_input_list	(	const BddEnc_ptr	bdd_enc,
		Trace_ptr	trace,
		node_ptr	path
	)

Fills the given trace out of a < S (i, S)* > bdd list.

Fills the given trace out of a < S (i, S)* > bdd list. The returned trace is the given one, filled with all steps. The given trace MUST be empty. Path must be non-Nil

none

See also:

Trace_create, Bmc_fill_trace_from_cnf_model

void Mc_trace_step_put_input_from_bdd	(	Trace_ptr	trace,
		TraceIter	step,
		BddEnc_ptr	bdd_enc,
		bdd_ptr	bdd
	)

Populates a trace step with input assignments.

none

void Mc_trace_step_put_state_from_bdd	(	Trace_ptr	trace,
		TraceIter	step,
		BddEnc_ptr	bdd_enc,
		bdd_ptr	bdd
	)

Populates a trace step with state assignments.

none

void McCheckInvarOpts_init	(	McCheckInvarOpts *	options,
		NuSMVEnv_ptr	env
	)

void McCheckInvarOpts_init_invalid

(

McCheckInvarOpts *

options

)

boolean McCheckInvarOpts_is_valid

(

McCheckInvarOpts *

options

)

int minu	(	BddFsm_ptr	,
		bdd_ptr	,
		bdd_ptr
	)

Computes the minimum length of the shortest path from f to g.

This function computes the minimum length of the shortest path from f to g.
Starts from f and proceeds forward until finds a state in g. Notice that this function works correctly only if -f option is used.

See also:

maxu

void print_compute	(	OStream_ptr	file,
		Prop_ptr	,
		Prop_PrintFmt	fmt
	)

Prints out a COMPUTE specification.

Prints out a COMPUTE specification

void print_invar	(	OStream_ptr	file,
		Prop_ptr	n,
		Prop_PrintFmt	fmt
	)

Print an invariant specification.

Print an invariant specification

void print_spec	(	OStream_ptr	file,
		Prop_ptr	prop,
		Prop_PrintFmt	fmt
	)

Prints out a CTL specification.

Prints out a CTL specification