CoVer Observer BNF

<obsSyntax>	::=	observer <obsID> ( <paramDeclList> ) { <nodeDecls> <rules> <accepting> }
<nodeDecls>	::=	/* empty */ | <nodeDecl> node <nodeID> [ ( <paramtypeList> )] ;
<paramDeclList>	::=	/* empty */ | <paramDeclList> <paramDecl>
<paramDecl>	::=	procid <procID> ; | varid <varID> ; | templid <templID> ; | syncid <syncID> ; | locid <locID> ; | edgeid <edgeID> ; | int <ID> ;
<paramtypeList>	::=	<paramtype> | <paramtypeList> , <paramtype>
<paramtype>	::=	procid | varid | templid | syncid | locid | edgeid | int
<rules>	::=	/* empty */ | <rules> <rule>
<rule>	::=	rule <nodeID> [ ( argList ) ] to <nodeID> [ ( argList ) ] with <conjuncts> ;
<argList>	::=	ID | <argList> , ID
<conjuncts>	::=	<conjunct> | <conjuncts> , <conjunct>
<conjunct>	::=	<topConj>
<topConj>	::=	<noConj> | <cmpConj> | <assConj> | <defConj> | <useConj>
<noConj>	::=	no <topConj>
<cmpConj>	::=	<exprConj> <cmpOp> <exprConj>
<cmpOp>	::=	== | <= | >= | != | < | >
<assConj>	::=	ID ':=' <exprConj>
<defConj>	::=	def ( <varID> ) | def ( <varID> , <edgeID> ) | def ( <varID> , <edgeID> , <procID> )
<useConj>	::=	use ( <varID> ) | use ( <varID> , <edgeID> ) | use ( <varID> , <edgeID> , <procID> )
<exprConj>	::=	<varExpr> | <evalExpr> | <edgeExpr> | <locExpr> | <syncExpr>
<varExpr>	::=	<varID>
<evalExpr>	::=	eval ( <varID> )
<edgeExpr>	::=	edge | edge ( <procID> )
<locExpr>	::=	loc | loc ( <procID> )
<syncExpr>	::=	event | event ( <procID> )
<accepting>	::=	accepting <nodeIdList> ;
<nodeIdList>	::=	<nodeID> | <nodeIdList> , <nodeID>

% Name of observer (same as file name)
<obsID> ::= ID

% Parameters can hold identifiers of (or set of) locations, edges,
% variables, processes, templates, channels, or values of ints
% identifier of a variable in the model
<locID> ::= ID % return of loc()
<edgeID> ::= ID % return of edge()
<varID> ::= ID
<syncID> ::= ID % return of event()
<procID> ::= ID
% nodes are declared in the observer
<nodeID> ::= ID

Observer example:

observer edgeObs( procid P; ) {
 node edgeNode(edgeid);
 rule start to edgeNode(E) with E := edge(P);
 accepting edgeNode;
}

For this observer a property can be:

cover edgeObs({P1,P2})

This property observe edge coverage on both process P1 and process P2. The formal parameter P is instantiated with the set {P1, P2}, thus both covered edges in P1 and P2 are observed.