CoVer Propery BNF

The Property.q file have the following BNF:

COVERPROP    ::= 'cover' OBSERVER [ '(' COVARGS ')' ] [ 'restrict' APPL ]
OBSERVER     ::= the name of the observer (file) e.g., Observer for Observer.obs
COVARGS      ::= ARGSET | ARGSET ',' COVARGS 
ARGSET       ::= '{' comma separated list of model identifiers '}'
APPL         ::= '(' comma separated list of model processes ')'

We observe that this property covers according to an external observer e.g., edgeObs. The egdeObs is supposed to be found in the file edgeObs.obs. The observer takes optionally arguments which is sets of identifiers from the model. Inside such set all identifiers must be of the same type. The coverage observations may be restricted to a set of model processes.

CoVer Propery Examples

Example 1:

       cover observer1 ( { modelproc } ) restrict ( modelproc ) 

where observer1.obs is a file specifying an observer modelproc is a process name from the UPPAAL model

Example 2:

      cover obsFile ( { modelvar1, modelvar1 }, {modelproc1, modelproc2} )

where obsFile is a file specifying an observer modelvar1 and modelvar2 are variables from the UPPAAL model modelproc1 and modelproc2 are process names from the UPPAAL model