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.
After a successful parse, the target choice will contain the list of composite processes. The visible process is the target for compilation etc. In addition, the list of actions menu's available from Check/Run is updated.
Generates an LTS for each of the component processes (whether primitive or composite) of the target composite process. 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). However, if a new target or action menu is added, Parse must be invoked explicitly to update the target and run lists
Generates a single LTS by composing the component LTSs 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.