This menu contains all the functions necessary to generate an LTS from an FSP description. However, usually, it is not necessary to invoke these functions directly. For example, compilation is implicitly invoked if the description is changed between successive calls to the safety check function.
Performs a syntax check on the text in the FSP window. The location of the first error detected is highlighted and an error message displayed in the output window. Consequently, errors are located and fixed one at a time. For the error location to be highlighted the FSP window must be selected (focus for mouse clicks).
After a successful parse, the target choice will contain the list of composite processes. The visible process is the target for compilation etc.
Generates an LTS for each of the component processes (whether primitive or composite) of the target composite process. Composite component processes are minimised by default - see Options. After compilation, the component processes may be viewed either graphically or textually - see Window. Compile will automatically invoke parse if the FSP window has been changed since the last Compile (or Parse).
Generates a single LTS by composing the component LTS produced by compile for a specified target. After composition, the LTS may be viewed graphically or textually. Error messages produced during composition indicate safety property violations and deadlocks.
Minimises the LTS produced by composition according to Milner's observation equivalence relation.