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. Traces are produced for cycles which cause liveness property violations.
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. The set of actions controlled by a user is by default the alphabet of the target composite process. This may be reduced by including a process MENU explicitly in the target composition. The alphabet of this process is then used
e.g. MENU = (toss -> MENU)
will restrict the controlled alphabet of the coin tossing example to toss. The current state of each component LTS displayed in a Draw window is updated by the animator.
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.