Board.alt 1.03 KB
Newer Older
point's avatar
point committed
1
2
3
4
node Board
  state
   /* 1 */ c : [0, 1][2][2];
  event
5
6
7
8
   /* 1 */ '$';
   /* 2 */ diagonal;
   /* 3 */ col_or_line;
   /* 4 */ one;
point's avatar
point committed
9
10
11
12
13
14
15
16
17
18
19
20
21
  trans
   true |- one -> 'c[0][0]' := ('c[0][0]'+1) mod 2;
   true |- one -> 'c[0][1]' := ('c[0][1]'+1) mod 2;
   true |- one -> 'c[1][0]' := ('c[1][0]'+1) mod 2;
   true |- one -> 'c[1][1]' := ('c[1][1]'+1) mod 2;
   true |- col_or_line -> 'c[1][0]' := ('c[1][0]'+1) mod 2, 'c[0][0]' := ('c[0][0]'+1) mod 2;
   true |- col_or_line -> 'c[1][1]' := ('c[1][1]'+1) mod 2, 'c[0][1]' := ('c[0][1]'+1) mod 2;
   true |- col_or_line -> 'c[0][1]' := ('c[0][1]'+1) mod 2, 'c[0][0]' := ('c[0][0]'+1) mod 2;
   true |- col_or_line -> 'c[1][1]' := ('c[1][1]'+1) mod 2, 'c[1][0]' := ('c[1][0]'+1) mod 2;
   true |- diagonal -> 'c[1][1]' := ('c[1][1]'+1) mod 2, 'c[0][0]' := ('c[0][0]'+1) mod 2;
   true |- diagonal -> 'c[1][0]' := ('c[1][0]'+1) mod 2, 'c[0][1]' := ('c[0][1]'+1) mod 2;
   true |- '$' -> ;
  // assertion is (implicitly) 'true'.
22
23
  // no initial assignment is specified.
  // no initial constraint is specified.
point's avatar
point committed
24
edon