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


check_ltlspec_bmc [-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:
- @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

Last updated on 2010/05/19 15h:56