The formula editor is a text editor with some temporal logic formula specific features.
In the main part of the editor window formulae can be edited.
If the keyboard offers this possibility the cut , copy and paste keys can be used.
The icons underneath the pull-down menu (except the far right one) allow to type parts of a formula by clicking on them. Thus the user need not be familiar with the abbreviations of the operators. The following listing shows, for each button, the characters that is inserted if you click on the button.
not -
and *
or +
iff <=>
implies =>
Forall !
Exists ?
True 1
False 0
Box #
Diamond ^
Formulae involve place names of a net (e.g., # P1 ). Furthermore variable bindings can be used (e.g., # 'Variable-name = Value' ). They are automatically transformed into place names. Parantheses can be used to structure formulae (i.e. to overrule priorities of the operators). You can keep different formulae within one file if you prefix the currently unused formulae with a % .
Note: Using characters as in the right column of the above table is a compromise because formulae must be ASCII text to be of any use for tools.