State = (Tr x Store
x Res)
Res = Store -> P(State)
step: (Store -> Store) -> Res
step(f,s) = { (true, f(s), _) }
pause: Res -> Res
pause(r,s) = { (false, s, r) }
seq: Res x Res ->
Res
(r_1 seq r_2)(s) = (f+ o
r_1)(s)
where f(t,s,r) = t ->
{ (false, s, r_2) }
[] { (false, s, r seq r_2) }
par: Res x Res -> Res
(r_1 par r_2)(s) = (r_1 then r_2)(s)
union (r_2 then r_1)(s)
where then: Res x Res
-> Res
(r_1 then r_2)(s) = (f+ o
r_1)(s)
where f(t,s,r) = t -> { (false, s, r_2)
} []
{ (false, s, r then r_2), (false, s, r_2
then r) }
flatten: Res -> Store ->
P(Store)
flatten r s = (f+ o
r)(s)
where f(t,s,r) = t -> {s} []
(flatten r)(s)