bmc_inc_simulate - Incrementally generates a trace of the model performing a given number of steps.
bmc_inc_simulate [-h] [-p | -v] [-r] [[-c "constraints"] | [-t "constraints"]
bmc_inc_simulate performs incremental simulation
of the model. If no length is specified with -k command
parameter, then the number of steps of simulation to perform is
taken from the 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.
- -i
- Enters simulation's interactive mode.
- -a
- Displays all the state variables (changed and unchanged)
in the interactive session
- -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