Grammar for invariants (May 1998)

INVARIANT  ::=  \begin{invariant}{NETID} INVS \end{invariant}

NETID           ::= STRING

INVS ::= PINV INVS | TINV INVS | empty
 
PINV ::= \pinv{ PSUM }
TINV ::= \tinv{ TSUM }
 
PSUM ::= INTEGER`PID  
    | INTEGER`PID + PSUM
TSUM ::= INTEGER`TID  
    | INTEGER`TID + TSUM
 
PID      ::= PLACEID | PLACEID.COLORID 
           | IDS.PLACEID | IDS.PLACEID.COLORID
TID      ::= TRANSID | TRANSID.COLORID 
           | IDS.TRANSID | IDS.TRANSID.COLORID 
IDS      ::= PLACEID | TRANSID | IDS.PLACEID | IDS.TRANSID
PLACEID  ::= STRING
COLORID  ::= STRING
TRANSID  ::= STRING