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:37