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] | -P "name"] [-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.
- -P name
- Checks the LTLSPEC property with name name in the property
database.
- -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 2010/05/19 22h:26