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.