check_ltlspec_bmc_onepb - Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the single problem bound and the loopback values


check_ltlspec_bmc_onepb [-h | -n idx | -p "formula" [IN context]] [-k length] [-l loopback] [-o filename]

As command check_ltlspec_bmc but it produces only one single problem with fixed bound and loopback values, with no iteration of the problem bound from zero to max_length.

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.
-k length
length is the problem bound used when generating the single problem. 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 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 2009/01/30 15h:04