Download Memorax

Sequence {s0 ;· · ·;sn }
The sequence construct arranges its constituent sub-statements, unsurprisingly, in a sequence from qsrc to qtgt , as shown in the diagram below.
qsrc
s0
sn
···
qtgt
If-statement if bexpr then sthen else selse
An if-statement branches the automaton into two branches where the initial
assume transitions ensure that only one branch can be taken at any one time.
assume:
bexpr
sthen
qtgt
qsrc
assume:
selse
not bexpr
While-statement while bexpr do s
A while-statement translates to a loop that will be taken as long as bexpr
evaluates to true, but no longer.
assume:
s
bexpr
qsrc
assume:
qtgt
not bexpr
0
l
Either-statement either{s00 ;· · ·;sm
0 or · · · or sn ;· · ·;sn }
An either statement is a non-deterministic choice. It translates into multiple
branches with no attached guards (except for what may occur in the constituents
sji ).
21