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


gen_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 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:
- @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/11/04 13h:33