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.
Safety
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.
Progress
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.
LTL Property
Compiles the selected LTL property into a Buchi automata using Giannakopoulou's
LTL2Buchi translator and performs a model check to see if the selected target
system is a model of the property. The model checking algorithm for liveness
properties is a depth first search for commected components as for progress
properties. If an LTL property can be determined to be a safety property, then
a breadth first search as in safety above is performed. Partial Order Reduction
can be used in both searches to reduce the number of states that have to be
explored to check a property.
Run
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 DEFAULT entry in the Run list
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 the Draw panel is updated by the animator. 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 are not enabled 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.
Supertrace
Depth first reachability analysis using Holtzmann's bitstate hashing technique
(Supertrace). Note that Supertrace is not a complete search of the state space.
Supertrace should be used only where a complete search of the state space is
not possible due to size.
Stop
This item is enabled whenever the LTSA is performing a lengthy computation.
If invoked, Stop aborts the computation. It is usually invoked
from the tool bar.