bmc_simulate - Generates a trace of the model from 0 (zero) to k
bmc_simulate [-h] [-p | -v] [-r] [[-c "constraints"] | [-t "constraints"]
bmc_simulate does not require a specification
to build the problem, because only the model is used to build it.
The problem length is represented by the -k command parameter,
or by its default value stored in the environment variable
bmc_length.
Command Options:
- -p
- Prints current generated trace (only those variables whose value
changed from the previous state).
- -v
- Verbosely prints current generated trace (changed and unchanged
state variables).
- -r
- Picks a state from a set of possible future states in a random way.
- -c "constraints"
- Performs a simulation in which computation is restricted
to states satisfying those constraints. The desired
sequence of states could not exist if such constraints were too
strong or it may happen that at some point of the simulation a
future state satisfying those constraints doesn't exist: in
that case a trace with a number of states less than
steps trace is obtained. The expression cannot contain
next operators, and is automatically shifted by one state in
order to constraint only the next steps
- -t "constraints"
- Performs a simulation in which computation is restricted
to states satisfying those constraints. The desired
sequence of states could not exist if such constraints were too
strong or it may happen that at some point of the simulation a
future state satisfying those constraints doesn't exist: in
that case a trace with a number of states less than
steps trace is obtained. The expression can contain
next operators, and is NOT automatically shifted by one state
as done with option -c
- -k steps
- Maximum length of the path according to the constraints.
The length of a trace could contain less than steps states:
this is the case in which simulation stops in an intermediate
step because it may not exist any future state satisfying those
constraints.
Last updated on 2012/11/18 14h:16