bmc_pick_state - Picks a state from the set of initial states


bmc_pick_state [-h] [-v] ] [-c "constraint" | -s trace.state] [-r] [-a [-i]]

Chooses an element from the set of initial states, and makes it the current state (replacing the old one). The chosen state is stored as the first state of a new trace ready to be lengthened by steps states by the bmc_simulate or bmc_inc_simulate commands. A constraint can be provided to restrict the set of candidate states.

Command Options:

-v
Verbosely prints out chosen state (all state variables, otherwise it prints out only the label t.1 of the state chosen, where t is the number of the new trace, that is the number of traces so far generated plus one).
-r
Randomly picks a state from the set of initial states.
-i
Enters simulation's interactive mode.
-a
Displays all the state variables (changed and unchanged) in the interactive session
-c "constraint"
Uses constraint to restrict the set of initial states in which the state has to be picked.
-s trace.state
Picks state from trace.state label. A new simulation trace will be created by copying prefix of the source trace up to specified state.

Last updated on 2012/11/18 14h:37