B.9 Property, Progress and Menu

B.9 Property, Progress and Menu

A safety property is defined by a process prefixed by the keyword property.

 PropertyDef:               property ProcessDef 

There are two forms of progress property, though we have used only the simpler form in the main text of this book. The first form asserts that at least one action in aset S must occur infinitely often. The second form is conditional progress, which takes the form if C then S. This asserts that if one of the actions in the set C occurs infinitely often, then so must one of the actions in the set S.

 ProgressDef:               progress ProgressIdent Rangesopt = Set               progress ProgressIdent Rangesopt = if Set then Set 

A set of progress properties may be declared using an index range.

Example

 progress G[i:1..3] = {{a,b}[i]}

A menu definition specifies the set of actions that the user can control in an animation.

 MenuDef:               menu MenuIdent = Set