Property specification

Properties are defined using PRISM’s property specification language. For details, we refer to the PRISM manual. ProFeat provides a syntactic construct for embedding ProFeat expressions in properties. All expressions between ${ and } are interpreted as ProFeat expressions. Consider the following example:

P=? [ F ${ Consumer[0].work = 0 & Buffer.cell[0] = -1 } ];

Here, a ProFeat expression is used to define the set of states for the F operator.

Note

The ${ ... } construct cannot be nested.

All expressions marked with ${ ... } are translated into a PRISM expression when translating a properties file using ProFeat.