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
gen_ltlspec_bmc_onepb [-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:
- @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 22h:26