| | | B.3.5 autostar: Apply auto also to Sibling States |
autostar
: autostar
In proving mode.
This command applies the command auto to the current state and to all of its (not yet closed) subsequent siblings, i.e., to all (not yet closed) states that have the same parent as the current state and appear in the sequence of the parent's children after the current state. Some of these states may be closed; all others remain unchanged.
The proof does not record the application of autostar but the successful applications of auto; when the proof is replayed, only these applications are replayed.
This command is especially useful after an application of the command scatter which potentially generates a large number of child states with simple goals.
During the execution of autostar, the proof states already processed
by auto are displayed and those that are successfully closed are
recorded. If during the execution of autostar the abort button
is pressed, only the current invocation of auto is aborted while the
execution of autostar itself continues with the next state in
sequence. Thus autostar can be used to interactively probe for states
that can be closed by auto without fear to get stuck in some
long-running invocation or to lose successful invocations by aborting.
| | | B.3.5 autostar: Apply auto also to Sibling States |