NuSMV/code/nusmv/shell/bmc/bmcCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/bmc/bmcCmd.h"
#include "nusmv/core/bmc/bmc.h"
#include "nusmv/core/bmc/bmcBmc.h"
#include "nusmv/core/bmc/bmcUtils.h"
#include "nusmv/core/bmc/bmcSimulate.h"
#include "nusmv/core/bmc/bmcTest.h"
#include "nusmv/shell/bmc/sbmc/sbmcCmd.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/node/printers/MasterPrinter.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/simulate/simulate.h"
#include "nusmv/core/trace/exec/SATCompleteTraceExecutor.h"
#include "nusmv/core/trace/exec/SATPartialTraceExecutor.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include "nusmv/core/utils/Logger.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/wff/w2w/w2w.h"

Defines
#define	BMC_USAGE 2
	Bmc.Cmd module.
Functions
void	Bmc_AddCmd (NuSMVEnv_ptr env)
	Adds all bmc-related commands to the interactive shell.
Outcome	Bmc_Cmd_compute_rel_loop (NuSMVEnv_ptr const env, int const l, const char str_loop, const int k)
	Check k and l and assign to l the right value.
Outcome	Bmc_cmd_options_handling (NuSMVEnv_ptr env, int argc, char *argv, Prop_Type prop_type, Prop_ptr res_prop, int res_k, int res_l, char res_a, char res_s, char *res_o, boolean res_e, int *res_step_k)
	Bmc commands options handling for commands (optionally) acceping options -k -l -o -a -n -p -P -e.
void	Bmc_Cmd_quit (NuSMVEnv_ptr env)
	Remove all bmc-related commands to the interactive shell.
int	Bmc_CommandBmcIncSimulate (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandBmcPickState (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandBmcSetup (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandBmcSimulate (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandBmcSimulateCheckFeasibleConstraints (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandCheckInvarBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandCheckLtlSpecBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandCheckLtlSpecBmcOnePb (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandGenInvarBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandGenLtlSpecBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_CommandGenLtlSpecBmcOnePb (NuSMVEnv_ptr env, int argc, char **argv)
int	Bmc_TestTableau (NuSMVEnv_ptr env, int argc, char **argv)

Define Documentation

#define BMC_USAGE 2

Bmc.Cmd module.

Author:: Roberto Cavada This module contains all the bmc commands implementation. Options parsing and checking is performed here, than the high-level Bmc layer is called

Todo:: Missing synopsis

Todo:: Missing description

Function Documentation

void Bmc_AddCmd ( NuSMVEnv_ptr env )

Adds all bmc-related commands to the interactive shell.

AutomaticEnd

Outcome Bmc_Cmd_compute_rel_loop	(	NuSMVEnv_ptr const	env,
		int *const	rel_loop,
		const char *	str_loop,
		const int	k
	)

Check k and l and assign to l the right value.

l is changed

Outcome Bmc_cmd_options_handling	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv,
		Prop_Type	prop_type,
		Prop_ptr *	res_prop,
		int *	res_k,
		int *	res_l,
		char **	res_a,
		char **	res_s,
		char **	res_o,
		boolean *	res_e,
		int *	res_step_k
	)

Bmc commands options handling for commands (optionally) acceping options -k -l -o -a -n -p -P -e.

Output variables called res_* are pointers to variables that will be changed if the user specified a value for the corresponding option. For example if the user specified "-k 2", then res_k will be assigned to 2. The caller can selectively choose which options can be specified by the user, by passing either a valid pointer as output parameter, or NULL to disable the corresponding option. For example by passing NULL as actual parameter of res_l, option -l will be not accepted.

If both specified, k and l will be checked for mutual consistency. Loop will contain a relative value, like the one the user specified.

prop_type is the expected property type, if specified.

All integers values will not be changed if the corresponding options had not be specified by the user, so the caller might assign them to default values before calling this function.

All strings will be allocated by the function if the corresponding options had been used by the user. In this case it is responsability of the caller to free them. Strings will be assigned to NULL if the user had not specified any corresponding option.

Returns OUTCOME_GENERIC_ERROR if an error has occurred; Returns OUTCOME_SUCCESS_REQUIRED_HELP if -h options had been specified; Returns OUTCOME_SUCCESS in all other cases.

Result parameters might change

void Bmc_Cmd_quit ( NuSMVEnv_ptr env )

Remove all bmc-related commands to the interactive shell.

Remove env sbmc command

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

Command:: bmc_inc_simulate: Incrementally generates a trace of the model performing a given number of steps.

Command arguments: [-h] [-p | -v] [-r] [[-c "constraints"] | [-t "constraints"] ] [-k steps]

bmc_inc_simulate performs incremental simulation of the model. If no length is specified with -k command parameter, then the number of steps of simulation to perform is taken from the value stored in the environment variable bmc_length.
Command Options:

-p: Prints current generated trace (only those variables whose value changed from the previous state).
-v: Verbosely prints current generated trace (changed and unchanged state variables).
-r: Picks a state from a set of possible future states in a random way.
-i: Enters simulation's interactive mode.
-a: Displays all the state variables (changed and unchanged) in the interactive session
-c "constraints": Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression cannot contain next operators, and is automatically shifted by one state in order to constraint only the next steps
-t "constraints": Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression can contain next operators, and is NOT automatically shifted by one state as done with option -c
-k steps: Maximum length of the path according to the constraints. The length of a trace could contain less than steps states: this is the case in which simulation stops in an intermediate step because it may not exist any future state satisfying those constraints.

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

Command:: bmc_pick_state: Picks a state from the set of initial states

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

Chooses an element from the set of initial states, and makes it the current state (replacing the old one). The chosen state is stored as the first state of a new trace ready to be lengthened by steps states by the bmc_simulate or bmc_inc_simulate commands. A constraint can be provided to restrict the set of candidate states.

Command Options:

-v: Verbosely prints out chosen state (all state variables, otherwise it prints out only the label t.1 of the state chosen, where t is the number of the new trace, that is the number of traces so far generated plus one).
-r: Randomly picks a state from the set of initial states.
-i: Enters simulation's interactive mode.
-a: Displays all the state variables (changed and unchanged) in the interactive session
-c "constraint": Uses constraint to restrict the set of initial states in which the state has to be picked.
-s trace.state: Picks state from trace.state label. A new simulation trace will be created by copying prefix of the source trace up to specified state.

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

Command:: bmc_setup: Builds the model in a Boolean Epression format.

Command arguments: [-h] | [-f]

You must call this command before use any other bmc-related command. Only one call per session is required.
Command options:

-f: Forces the BMC model to be built.

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

Command:: bmc_simulate: Generates a trace of the model from 0 (zero) to k

Command arguments: [-h] [-p | -v] [-r] [[-c "constraints"] | [-t "constraints"] ] [-k steps]

bmc_simulate does not require a specification to build the problem, because only the model is used to build it. The problem length is represented by the -k command parameter, or by its default value stored in the environment variable bmc_length.
Command Options:

-p: Prints current generated trace (only those variables whose value changed from the previous state).
-v: Verbosely prints current generated trace (changed and unchanged state variables).
-r: Picks a state from a set of possible future states in a random way.
-c "constraints": Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression cannot contain next operators, and is automatically shifted by one state in order to constraint only the next steps
-t "constraints": Performs a simulation in which computation is restricted to states satisfying those constraints. The desired sequence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn't exist: in that case a trace with a number of states less than steps trace is obtained. The expression can contain next operators, and is NOT automatically shifted by one state as done with option -c
-k steps: Maximum length of the path according to the constraints. The length of a trace could contain less than steps states: this is the case in which simulation stops in an intermediate step because it may not exist any future state satisfying those constraints.

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

Command:: bmc_simulate_check_feasible_constraints: Performs a feasibility check on the list of given constraints. Constraints that are found to be feasible can be safely assumed not to cause deadlocks if used in the following step of incremental simulation.

Command arguments: [-h | -q] [-c "formula"]*

This command generates feasibility problems for each constraint. Every constraint is checked against current state and FSM's transition relation, in order to exclude the possibility of deadlocks. Constraints found to be feasible can be safely assumed not to cause deadlocks if used in the following step of incremental simulation.

Command options:

-q: Enables quiet mode. For each analyzed constraint "0" is printed if the constraint is found to be unfeasible, "1" is printed otherwise.
-c "formula": Provide a constraint as a formula specified on the command-line. This option can be specified multiple times, in order to analyze a list of constraints.

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

Command:: check_invar_bmc: Generates and solve the given invariant, or all invariants if no formula is given

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-a algorithm] [-o filename]

Command options:

-n index

index is the numeric index of a valid INVAR specification formula actually located in the properties database.
The validity of index value is checked out by the system.

-p "formula [IN context]"

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P name

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

-k max_length

(Use only when selected algorithm is een-sorensson). Use to specify the maximal deepth to be reached by the een-sorensson invariant checking algorithm. If not specified, the value assigned to the system variable bmc_length is taken.

-a algorithm

Uses the specified algorithm to solve the invariant. If used, this option will override system variable bmc_invar_alg. At the moment, possible values are: "classic", "een-sorensson".

-e

Uses an additional step clause for algorithm "een-sorensson". filename is the name of the dumped dimacs file, without extension.
It may contain special symbols which will be macro-expanded to form the real file name. Possible symbols are:

: model name with path part
: model name without path part
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_GenSolveInvar

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

Command:: check_ltlspec_bmc: Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the maximum length and the loopback values

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-l loopback] [-o filename]

This command generates one or more problems, and calls SAT solver for each one. Each problem is related to a specific problem bound, which increases from zero (0) to the given maximum problem length. Here "length" is the bound of the problem that system is going to generate and/or solve.
In this context the maximum problem bound is represented by the -k command parameter, or by its default value stored in the environment variable bmc_length.
The single generated problem also depends on the "loopback" parameter you can explicitly specify by the -l option, or by its default value stored in the environment variable bmc_loopback.
The property to be checked may be specified using the -n idx, the -p "formula" or the -P "name" options.
If you need to generate a dimacs dump file of all generated problems, you must use the option -o "filename".

Command options:

-n index

index is the numeric index of a valid LTL specification formula actually located in the properties database.

-p "formula" [IN context]

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P name

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

-k max_length

max_length is the maximum problem bound must be reached. Only natural number are valid values for this option. If no value is given the environment variable bmc_length is considered instead.

-l loopback

loopback value may be:

a natural number in (0, max_length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of length and loopback will be skipped during the generation/solving process.
a negative number in (-1, -bmc_length). In this case loopback is considered a value relative to max_length. Any invalid combination of length and loopback will be skipped during the generation/solving process.
the symbol 'X', which means "no loopback"
the symbol '*', which means "all possible loopback from zero to length-1"

-o filename

filename is the name of the dumped dimacs file, without extension.
It may contain special symbols which will be macro-expanded to form the real file name. Possible symbols are:

: model name with path part
: model name without path part
: current problem bound
: current loopback value
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_CommandCheckLtlSpecBmcOnePb, Bmc_GenSolveLtl

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

Command:: check_ltlspec_bmc_onepb: Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the single problem bound and the loopback values

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k length] [-l loopback] [-o filename]

As command check_ltlspec_bmc but it produces only one single problem with fixed bound and loopback values, with no iteration of the problem bound from zero to max_length.

Command options:

-n index

index is the numeric index of a valid LTL specification formula actually located in the properties database.
The validity of index value is checked out by the system.

-p "formula [IN context]"

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P name

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

-k length

length is the problem bound used when generating the single problem. Only natural number are valid values for this option. If no value is given the environment variable bmc_length is considered instead.

-l loopback

loopback value may be:

a natural number in (0, max_length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of length and loopback will be skipped during the generation/solving process.
a negative number in (-1, -bmc_length). In this case loopback is considered a value relative to length. Any invalid combination of length and loopback will be skipped during the generation/solving process.
the symbol 'X', which means "no loopback"
the symbol '*', which means "all possible loopback from zero to length-1"

-o filename

filename is the name of the dumped dimacs file, without extension.
It may contain special symbols which will be macro-expanded to form the real file name. Possible symbols are:

: model name with path part
: model name without path part
: current problem bound
: current loopback value
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_CommandCheckLtlSpecBmc, Bmc_GenSolveLtl

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

Command:: gen_invar_bmc: Generates the given invariant, or all invariants if no formula is given

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-o filename]

Command options:

-n index

index is the numeric index of a valid INVAR specification formula actually located in the properties database.
The validity of index value is checked out by the system.

-p "formula" [IN context]

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P "name"

Checks the invariant property stored in the properties database with name "name"

-o filename

filename is the name of the dumped dimacs file, without extension.
If you do not use this option the dimacs file name is taken from the environment variable bmc_invar_dimacs_filename.
File name may contain special symbols which will be macro-expanded to form the real dimacs file name. Possible symbols are:

: model name with path part
: model name without path part
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_GenSolveInvar

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

Command:: gen_ltlspec_bmc: Dumps into one or more dimacs files the given LTL specification, or all LTL specifications if no formula is given. Generation and dumping parameters are the maximum bound and the loopback values

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-l loopback] [-o filename]

This command generates one or more problems, and dumps each problem into a dimacs file. Each problem is related to a specific problem bound, which increases from zero (0) to the given maximum problem bound. In this short description "length" is the bound of the problem that system is going to dump out.
In this context the maximum problem bound is represented by the max_length parameter, or by its default value stored in the environment variable bmc_length.
Each dumped problem also depends on the loopback you can explicitly specify by the -l option, or by its default value stored in the environment variable bmc_loopback.
The property to be checked may be specified using the -n idx, the -p "formula" or the -P "name" options.
You may specify dimacs file name by using the option -o "filename", otherwise the default value stored in the environment variable bmc_dimacs_filename will be considered.

Command options:

-n index

index is the numeric index of a valid LTL specification formula actually located in the properties database.
The validity of index value is checked out by the system.

-p "formula [IN context]"

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P name

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

-k max_length

max_length is the maximum problem bound used when increasing problem bound starting from zero. Only natural number are valid values for this option. If no value is given the environment variable bmc_length value is considered instead.

-l loopback

loopback value may be:

a natural number in (0, max_length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of bound and loopback will be skipped during the generation and dumping process.
a negative number in (-1, -bmc_length). In this case loopback is considered a value relative to max_length. Any invalid combination of bound and loopback will be skipped during the generation process.
the symbol 'X', which means "no loopback"
the symbol '*', which means "all possible loopback from zero to length-1"

-o filename

filename is the name of dumped dimacs files, without extension.
If this options is not specified, variable bmc_dimacs_filename will be considered. The file name string may contain special symbols which will be macro-expanded to form the real file name. Possible symbols are:

: model name with path part
: model name without path part
: current problem bound
: current loopback value
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_CommandGenLtlSpecBmcOnePb, Bmc_GenSolveLtl

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

Command:: gen_ltlspec_bmc_onepb: Dumps into one dimacs file the problem generated for the given LTL specification, or for all LTL specifications if no formula is explicitly given. Generation and dumping parameters are the problem bound and the loopback values

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k length] [-l loopback] [-o filename]

As the gen_ltlspec_bmc command, but it generates and dumps only one problem given its bound and loopback.

Command options:

-n index

index is the numeric index of a valid LTL specification formula actually located in the properties database.
The validity of index value is checked out by the system.

-p "formula [IN context]"

Checks the formula specified on the command-line.
context is the module instance name which the variables in formula must be evaluated in.

-P name

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

-k length

length is the single problem bound used to generate and dump it. Only natural number are valid values for this option. If no value is given the environment variable bmc_length is considered instead.

-l loopback

loopback value may be:

a natural number in (0, length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of length and loopback will be skipped during the generation and dumping process.
a negative number in (-1, -length). Any invalid combination of length and loopback will be skipped during the generation process.
the symbol 'X', which means "no loopback"
the symbol '*', which means "all possible loopback from zero to length-1"

-o filename

filename is the name of the dumped dimacs file, without extension.
If this options is not specified, variable bmc_dimacs_filename will be considered. The file name string may contain special symbols which will be macro-expanded to form the real file name. Possible symbols are:

: model name with path part
: model name without path part
: current problem bound
: current loopback value
: index of the currently processed formula in the properties database
@: the '@' character

See also:: Bmc_CommandGenLtlSpecBmc, Bmc_GenSolveLtl

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

Command:: check_pslspec_bmc_inc: Performs fair PSL model checking using incremental BMC.

Command arguments: [-h] [-m | -o output-file] [-n number | -p "psl-expr [IN context]" | -P "name"] [-1] [-k bmc_length] [-l loopback]\

Performs fair PSL model checking using incremental BMC.

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.

-1 Generates and solves a single problem instead of iterating through 0 and bmc_length.

-k bmc_length

bmc_length is the maximum problem bound must be reached if the option -1 is not specified. If -1 is specified, bmc_length is the exact length of the problem to be generated. Only natural number are valid values for this option. If no value is given the environment variable bmc_length is considered instead.

-l loopback

loopback value may be:

a natural number in (0, bmc_length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of length and loopback will be skipped during the generation/solving process.
a negative number in (-1, -bmc_length). In this case loopback is considered a value relative to bmc_length. Any invalid combination of length and loopback will be skipped during the generation/solving process.
the symbol 'X', which means "no loopback"
the symbol '*', which means "all possible loopback from zero to bmc_length-1"

NuSMV/code/nusmv/shell/bmc/bmcCmd.c File Reference

Defines

Functions

Define Documentation

Function Documentation