op <_;_;_> <_;_;_> : Location Real Real Real Real Real -> State .
op [_;_;_] <_;_;_> : Location Real Real Real Real Real -> State .
...
...
@@ -18,11 +18,11 @@ mod MODEL is
crl [tick-idle] : [ idle ; x ; y ] < p1 ; p2 ; p3 > => < idle ; x + T ; y + T > < p1 ; p2 ; p3 > if (T >= 0/1) = true [nonexec] .
crl [sugar-sugar] : < sugar ; x ; y > < p1 ; p2 ; p3 > => [ sugar ; 0/1 ; y ] < p1 ; p2 ; p3 > if (y <= p2 and x >= p1) = true .
crl [sugar-coffee] : < sugar ; x ; y > < p1 ; p2 ; p3 > => [ coffee ; x ; y ] < p1 ; p2 ; p3 > if (y <= p3 and y === p2) = true .
crl [sugar-preparing] : < sugar ; x ; y > < p1 ; p2 ; p3 > => [ preparing ; x ; y ] < p1 ; p2 ; p3 > if (y <= p3 and y === p2) = true .
crl [tick-sugar] : [ sugar ; x ; y ] < p1 ; p2 ; p3 > => < sugar ; x + T ; y + T > < p1 ; p2 ; p3 > if (T >= 0/1 and y + T <= p2) = true [nonexec] .
crl [coffee-cdone] : < coffee ; x ; y > < p1 ; p2 ; p3 > => [ cdone ; 0/1 ; y ] < p1 ; p2 ; p3 > if (0/1 <= 10/1 and y === p3) = true .
crl [tick-coffee] : [ coffee ; x ; y ] < p1 ; p2 ; p3 > => < coffee ; x + T ; y + T > < p1 ; p2 ; p3 > if (T >= 0/1 and y + T <= p3) = true [nonexec] .
crl [preparing-cdone] : < preparing ; x ; y > < p1 ; p2 ; p3 > => [ cdone ; 0/1 ; y ] < p1 ; p2 ; p3 > if (0/1 <= 10/1 and y === p3) = true .
crl [tick-preparing] : [ preparing ; x ; y ] < p1 ; p2 ; p3 > => < preparing ; x + T ; y + T > < p1 ; p2 ; p3 > if (T >= 0/1 and y + T <= p3) = true [nonexec] .