The analysis functions operate on the target composite process indicated in the Target choice box. If this has not been compiled or composed, compilation and composition are automatically invoked.
Performs a breadth first search on the target LTS. If a property violation or deadlock is found, the shortest trace of actions that would lead to the property violation or deadlock is displayed in the output window.
Computes the connected components for the target LTS. Checks for progress violations with respect to the declared progress properties. If no progress properties are declared then a check with respect to a default property is performed. The default property has all the actions in the alphabet of the current target.
Performs a user-controlled animation of the target composite process. Uses the component LTSs rather than the composite LTS, so larger systems can be animated even if they cannot be exhaustively checked. DEFAULT is the alphabet of the target composite process and allows explicit contol of all actions. This may be reduced by declaring an explicit menu e.g.
menu RUN = {toss}
The current state of each component LTS displayed in a Draw window is updated by the animator. By default, the Animator window includes Run and Step buttons. These are used to control actions which are not in the action menu and consequently do not have click boxes. These buttons do not appear if the autorun option is selected in the Options menu. The Run button permits a sequence of actions to occur where these actions are not explicitly controlled. The Step button permits a single such action to occur.
Performs an "on-the-fly" depth first search on the set of component LTS for the target. Since the composite LTS is not required, this uses less storage than Safety. Property violations and deadlocks are detected, however, no counter examples (traces) are produced.