NuSMV/code/nusmv/shell/bmc/sbmc/sbmcCmd.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"

Go to the source code of this file.

Functions
void	SBmc_AddCmd (NuSMVEnv_ptr env)
	The header file for the cmd module, the user commands handling layer.
void	Sbmc_Cmd_quit (NuSMVEnv_ptr env)
	Adds all bmc-related commands to the interactive shell.
int	Sbmc_CommandCheckLtlSpecSBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Sbmc_CommandGenLtlSpecSBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	Sbmc_CommandLTLCheckZigzagInc (NuSMVEnv_ptr env, int argc, char **argv)

---

Function Documentation

void SBmc_AddCmd

(

NuSMVEnv_ptr

env

)

The header file for the cmd module, the user commands handling layer.

Author:

Timo Latvala, Marco Roveri

Todo:

: Missing description

AutomaticStart

Adds all bmc-related commands to the interactive shell

See also:

CInit_Init

AutomaticEnd

void Sbmc_Cmd_quit

(

NuSMVEnv_ptr

env

)

Adds all bmc-related commands to the interactive shell.

See also:

CInit_Init

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

Command:

check_ltlspec_sbmc: Finds error up to depth k

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-l loopback] [-1] [-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 "<i>length</i>" 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 "<i>loopback</i>" 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 or the -p "formula" 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 <i>length-1</i>"

-1

Generates and solves a single problem with length k

-o filename

filename is the name of the dumped dimacs file. 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

For further information about this implementation see: T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. Copyright (C) Springer-Verlag.

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

Command:

gen_ltlspec_sbmc: 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. Uses Kepa's and Timo's method for doing bmc.

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-l loopback] [-1] [-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 "<i>length</i>" is the bound of the problem that system is going to dump out. Uses Kepa's and Timo's method for doing bmc.
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 or the -p "formula" 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.

-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 <i>length-1</i>"

-1

Generates a single problem with length k

-o filename

filename is the name of the dumped dimacs file. 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

For further information about this implementation see: T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. Copyright (C) Springer-Verlag.

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

Command:

check_ltlspec_sbmc_inc: Incremental SBMC LTL model checking

Command arguments: [-h | -n idx | -p "formula" [IN context] | -P "name"] [-k max_length] [-c] [-N]

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 "<i>length</i>" 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 property to be checked may be specified using the -n idx, -p "formula", or -P "property_name" options.
Completeness check, although slower, can be used to determine whether the property holds.

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.

-c

Performs completeness check at every step. This can be effectively used to determine whether a property holds.

-N

Does not perform virtual unrolling.

For further information about this implementation see: T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. Copyright (C) Springer-Verlag.