| Nr | Name | Value |
|---|---|---|
| 1 | board | ? |
| 2 | joueur | ? |
| 3 | lastpos | ? |
| Nr | Name | Value |
|---|---|---|
| 1 | count | /*@symbolic*/ %(x,y,c,b,dx,dy).(x : INTEGER & y : INTEGER & c : Couleurs & b : POW(INTEGER * INTEGER * Couleurs) & dx : INTEGER & dy : INTEGER|(IF x |-> y |-> c : b THEN 1 + count(x + dx |-> y + dy |-> c |-> b |-> dx |-> dy) ELSE 0 END)) |
| 2 | maxRow | 6 |
| 3 | maxCol | 7 |
| Nr | Name | Value |
|---|---|---|
| 1 | Couleurs | {jaune,rouge,vide} |
| 2 | PHASES | {jouer,compter,verifier} |
| 3 | INT | (-1 .. 3) |
| Nr | Event | Target State ID |
|---|---|---|
| 1 | SETUP_CONSTANTS(count=/*@symbolic*/ %(x,y,c,b,dx,dy).(x : INTEGER & y : INTEGER & c : Couleurs & b : POW(INTEGER * INTEG... | State 0 |
| 2 | INITIALISATION(joueur=rouge) | |
| 3 | joue(4) | |
| 4 | joue(5) | |
| 5 | joue(4) | |
| 6 | joue(5) | |
| 7 | joue(4) | |
| 8 | joue(4) | |
| 9 | joue(5) | |
| 10 | joue(2) | |
| 11 | joue(2) | |
| 12 | joue(5) | |
| 13 | joue(2) | |
| 14 | joue(2) | |
| 15 | joue(4) | |
| 16 | joue(7) | |
| 17 | joue(4) | |
| 18 | joue(1) | |
| 19 | joue(1) | |
| 20 | joue(1) | |
| 21 | joue(3) | |
| 22 | joue(2) | |
| 23 | joue(3) |