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.
gen_ltlspec_sbmc [-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 "length" 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
length-1"
- -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:
- @F: model name with path part
- @f: model name without path part
- @k: current problem bound
- @l: current loopback value
- @n: 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 ©
Springer-Verlag.
Last updated on 2011/04/06 21h:12