bmc_pick_state - Picks a state from the set of initial states


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

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).
-c "constraint"
Uses constraint to restrict the set of initial states in which the state has to be picked. constraint must be enclosed between double quotes " ".
-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 2010/05/19 22h:25