check_ltlspec_bmc_inc - Checks the given LTL specification, or all LTL specifications if no formula is given, using incremental algorithms. Checking parameters are the maximum length and the loopback values
check_ltlspec_bmc_inc [-h | -n idx | -p "formula" [IN context]] [-k max_length] [-l loopback]
This command generates one or more problems, and calls (incremental)
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 or
the -p "formula" options.
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.
- -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"
Last updated on 2009/01/30 14h:53