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.
- -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 2011/04/06 21h:12