Grammar for traces (May 1998)

TRACE           ::= \begin{trace}{NETID} CURR_MARKING TRACE_ITEM \end{trace}

NETID           ::= STRING

TRACE_ITEM      ::= empty
                    | TRANS_FIRE      TRACE_ITEM
                    | CURR_MARKING    TRACE_ITEM
                    | SUCC_MARKING    TRACE_ITEM
                    | CHANGED_MARKING TRACE_ITEM
                    | SERVICE         TRACE_ITEM
                    | FIRING_TIME     TRACE_ITEM

TRANS_FIRE      ::= \fire{ID}{NAME COLOR}
FIRING_TIME     ::= \time{ REAL }

SERVICE         ::= \serve{ID}{NAME COLOR}

CURR_MARKING    ::= \current{ MARKING }
SUCC_MARKING    ::= \succ{ MARKING }
CHANGED_MARKING ::= \add{ MARKING }


ID              ::= STRING
NAME            ::= empty | \name{ STRING }
COLOR           ::= empty | \color{ STRING }

MARKING         ::= empty
  | \place{ ID }{ NAME MULTISET } MARKING

MULTISET        ::= INTEGER | INTEGER`STRING MSLIST
MSLIST          ::= empty | + MULTISET