NuSMV/code/nusmv/shell/mc/mcCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/bmc/bmcCmd.h"
#include "nusmv/shell/bmc/sbmc/sbmcCmd.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/mc/mc.h"
#include "nusmv/shell/mc/mcCmd.h"
#include "nusmv/core/bmc/bmcPkg.c"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include "nusmv/core/parser/symbols.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/prop/PropDb.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/utils/utils_io.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/utils/ucmd.h"
#include "nusmv/core/bmc/bmcUtils.h"
#include "nusmv/core/bmc/bmcBmc.h"
#include "nusmv/core/fsm/bdd/bdd.h"

Functions
int	CommandCheckCompute (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandCheckCtlSpec (NuSMVEnv_ptr env, int argc, char **argv)
	Model checking commands.
int	CommandCheckInvar (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandCheckPslSpec (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandCompute (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandLanguageEmptiness (NuSMVEnv_ptr env, int argc, char **argv)
void	Mc_End (NuSMVEnv_ptr env)
	Quit the mc package.
void	Mc_Init (NuSMVEnv_ptr env)
	Module header file for shell commands.

---

Function Documentation

int CommandCheckCompute	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

check_compute: Performs computation of quantitative characteristics

Command arguments: [-h] [-m | -o output-file] [-n number | -p "compute-expr [IN context]" | -P "name"]

This command deals with the computation of quantitative characteristics of real time systems. It is able to compute the length of the shortest (longest) path from two given set of states.

MAX [ alpha , beta ]

MIN [ alpha , beta ]

Properties of the above form can be specified in the input file via the keyword COMPUTE or directly at command line, using option -p.

Option -n can be used for computing a particular expression in the model. If neither -n nor -p nor -P are used, all the COMPUTE specifications are computed.

Command options:

-m

Pipes the output generated by the command in processing COMPUTEs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command in processing COMPUTEs to the file output-file.

-p "compute-expr [IN context]"

A COMPUTE formula to be checked. context is the module instance name which the variables in compute-expr must be evaluated in.

-n number

Computes only the property with index number

-P name

Computes only the property named name

int CommandCheckCtlSpec	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Model checking commands.

Author:

Marco Roveri This file contains all the shell command to deal with model checking and for counterexample navigation.

Command:

check_ctlspec: Performs fair CTL model checking.

Command arguments: [-h] [-m | -o output-file] [-n number | -p "ctl-expr [IN context]" | -P "name"]

Performs fair CTL model checking.

A ctl-expr to be checked can be specified at command line using option -p. Alternatively, option -n or -P can be used for checking a particular formula in the property database. If neither -n nor -p are used, all the SPEC formulas in the database are checked.

Command options:

-m

Pipes the output generated by the command in processing SPECs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command in processing SPECs to the file output-file.

-p "ctl-expr [IN context]"

A CTL formula to be checked. context is the module instance name which the variables in ctl-expr must be evaluated in.

-n number

Checks the CTL property with index number in the property database.

-P name

Checks the CTL property with name name in the property database.

If the ag_only_search environment variable has been set, and the set of reachable states has already been computed, then a specialized algorithm to check AG formulas is used instead of the standard model checking algorithms.

int CommandCheckInvar	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

check_invar: Performs model checking of invariants

Command arguments: [-h] [-m | -o output-file] [-s "strategy"] [-e "heuristic"] [-t number] [-k number] [-j "heuristic"] [-n number | -p "invar-expr [IN context]" | -P "name"]

Performs invariant checking on the given model. An invariant is a set of states. Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant.

Invariants to be verified can be provided as simple formulas (without any temporal operators) in the input file via the INVARSPEC keyword or directly at command line, using the option -p.

Option -n can be used for checking a particular invariant of the model. If neither -n nor -p are used, all the invariants are checked.

During checking of invariant all the fairness conditions associated with the model are ignored.

If an invariant does not hold, a proof of failure is demonstrated. This consists of a path starting from an initial state to a state lying outside the invariant. This path has the property that it is the shortest path leading to a state outside the invariant.

Command options:

-m

Pipes the output generated by the program in processing INVARSPECs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command in processing INVARSPECs to the file output-file.

-s strategy

Force the analysis strategy.

-e heuristic

Force the search heuristic for the forward-backward strategy.

-t number

When using the mixed BDD and BMC approach specify the heuristic threshold.

-k number

When using the mixed BDD and BMC approach specify the BMC max k.

-j heuristic

Force the switch heuristic for the BDD-BMC strategy.

-p "invar-expr [IN context]"

The command line specified invariant formula to be verified. context is the module instance name which the variables in invar-expr must be evaluated in.

-P name

Checks the INVARSPEC with name name in the property database.

int CommandCheckPslSpec	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

check_pslspec: Performs fair PSL model checking.

Command arguments: [-h] [-m | -o output-file] [-n number | -p "psl-expr [IN context]" | -P "name"]

Performs fair PSL model checking.

A psl-expr to be checked can be specified at command line using option -p. Alternatively, option -n can be used for checking a particular formula in the property database. If neither -n nor -p are used, all the PSLSPEC formulas in the database are checked.

Command options:

-m

Pipes the output generated by the command in processing SPECs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command in processing PSLSPECs to the file output-file.

-p "psl-expr [IN context]"

A PSL formula to be checked. context is the module instance name which the variables in ctl-expr must be evaluated in.

-n number

Checks the PSL property with index number in the property database.

-P name

Checks the PSL property named name in the property database.

int CommandCompute	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

compute: Performs computation of quantitative characteristics

{}

This command is deprecated. It has been substituted by the command check_compute.

See also:

check_compute

int CommandLanguageEmptiness	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

language_emptiness: Checks for language emptiness.

Command arguments: [-h] [-v] [-a]

Checks for the language emptiness.

If -a is given 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 no -a is specified, the check is performed by verifying whether there exists at least one inital 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.

if -v is specified, then some information on the set of initial states is printed out too.

void Mc_End

(

NuSMVEnv_ptr

env

)

Quit the mc package.

Quit the mc package

void Mc_Init

(

NuSMVEnv_ptr

env

)

Module header file for shell commands.

Author:

Michele Dorigatti

Todo:

: Missing description

AutomaticStart

Initializes the mc package. Initializes the mc package.