Options Menu


Display warning messages
LTSA displays a warning message when an undefined state is mapped to the ERROR state during compilation. Default is set.

Treat warnings as errors
Halts compilation with an error message when an undefined state is found. Default is not set.

Fair Choice for LTL check
When set, the LTL checklooks for terminal connected components as for the Progress check. In other words, the same fair choice assumoption is implemented. If not set then no fairness assumption is made for the check and fairness assumptions must be explicitly encoded in the LTL property.

Partial Order Reduction
If set, enables partial order reduction during Composition and Safety, Progress, LTL property and Supertrace analysis. Default is not set.

Preserve OE for POR composition
If set, ensures that Observational Equivalence is preserved when Partial Order Reduction is used for composition. Default is set.

Enable Tau reduction
When set this speeds up minimization by collapsing tau chains before minimisation is performed. Care should be taken when using this reduction since it does not preserve observational equivalence. The reduction does of course preserve trace equivalnce and is always OK when perfroming safety analysis.

Set Supertrace parameters
Set depth bound (ie maximum stack depth) for Supertrace search. Set hash table size for Supertrace in kilobytes.


Use big fonts
Use large font in all windows. Useful for demonstrations and presentations. Default is not set.

Display name when drawing LTS
Displays the process name for an LTS in the Draw Pane. Default is set.

Use V2.0 label format when drawing LTS
If not set, labels are displayed with "." as in a.1 rather than a[1]. In addition, in V2.0, sets and ranges are combined. Default is set.

Multiple LTS in Draw window
Changes Draw Pane to multiple LTS display mode. Default is not set.


Autorun actions in Animator
Enables Run and Step buttons in Animator window. Actions are selected until an action in the menu set is enabled. Default is not set.