label=right:[$s$]{}\] ;

\(p) edge node\[above right, pos=0.3\][$x^2$]{} (t); (q) edge node\[below right, pos=0.3\][$y$]{} (t); (t) edge node\[above\][$y^3$]{} (r); (t) edge node\[above\][$0$]{} (s);

The transition $t$ consumes two tokens from place $p$, both of which have the same clock value $x$ (where $0 \le x \le 5$) and one token from place $q$ with clock value $y$ (where $1 < y \le 2$). It produces three tokens on place $r$ who all have the same clock value $y$ (where $y$ comes from the clock value of the token read from $q$), and another token with value $0$ on place $s$.

There are two different binary step relations on markings: *discrete* steps ${\longrightarrow_{t}}$ which fire a transition $t$ as specified by the relations $G,{\mathit{Pre}}$, and ${\mathit{Post}}$, and *time passing* steps ${\longrightarrow_{d}}$ for durations $d\in{{\mathbb R}_{\geq 0}}$, which simply increment all clocks by $d$.

\[def:mtpn:dsteps\] For a transition $t\in T$ and a variable evaluation $\pi:{\mathit{Var}}\to {{\mathbb R}_{\geq 0}}$, we say that *$\pi$ satisfies $G(t)$* if $\pi(x)\in G(t)(x)$ holds for all $x\in {\mathit{Var}}$. By lifting $\pi$ to multisets over $(P{\times}{\mathit{Var}})$ (respectively, to multisets over $(P{\times}(\{0\}\cup{\mathit{Var}}))$ with $\pi(0)=0$) in the canonical way, such an evaluation translates preconditions ${\mathit{Pre}}(t)$ and ${\mathit{Post}}(t)$ into markings $\pi({\mathit{Pre}}(t))$ and $\pi({\mathit{Post}}(t))$, 