The "|;|" order operator : strong sequence

Its evaluation terminates only if both P and Q terminate. Otherwise, no effects are preserved, and we go back to the initial context.

Considering 2 processes : P and Q, with strong sequence we execute first P and then Q (non-reflexive operation):

Application on the most basic example

Applying this on our most basic example, the "@moe:" section looks like :

And exploring the different paths with the symbolic engine (3, 4 and 5 evaluation steps) gives us (here, as all transitions cannot do anything else than succeeding, each step integrates the effect of both the automata's transitions simultaneously) :