Compile-time directives


The following directives may be used in FSP to direct compilation. These directives are keywords in the FSP implementation for LTSA 3.0 and thus may not be used as identifers

minimal
Forces minimisation during compilation. Can be used to prefic either a process or a composition.

deterministic
Makes the prefixed process or composition deterministic during compilation.

property
Makes the prefixed process or composition a safety property.

import
Import a process that has been saved in Aldebarfan(.aut) format.

import P = "fileP.aut"

constraint
When used instead of cosntraint for an LTL property, of the property is a safety property, then the compiler generates a process which is equivalent to the safety property with the transitions to error state removed. The process may be referenced in a composition.

animation, target, actions, controls
Used to declare the mappingto a graphic animation.