lab2
1
2
3
4
const N = 10
range R = 0..N
Count = Count[N],
Count[i:R] = (when (i>0) one -> Count[i-1]).
const N = 10
range R = 0..N
Count = Count[N],
Count[i:R] = (when (i>0) one -> Count[i-1]).
Pile = Pile[N],
Pile[i:R] = (when (i>=6) take6 -> Pile[i-6] | when (i>=4) take4 ->
Pile[i-4] | when(i > 0) take1 -> Pile[i-1]).
const N = 10
range R = 0..N
Count = Count[N],
Count[i:R] = (when (i>0) one -> Count[i-1]).
1
2
3
4
1
2
3
4
5
6
7
1
2
3
4
5
5
6
Pile = Pile[N],
Pile[i:R] = (when (i>=6) take6 -> Pile[i-6] | when (i>=4) take4 ->
Pile[i-4] | when(i > 0) take1 -> Pile[i-1]).
set Take6 = {a.take6, b.take6}
set Take4 = {a.take4, b.take4}
set Take1 = {a.take1, b.take1}
Game = Game[N],
Game[i:R] = (when (i>=6) Take6 -> Game[i-6] | when (i>=4) Take4 ->
Game[i-4] | when(i > 0) Take1 -> Game[i-1]).
const N = 10
range R = 0..N
Count = Count[N],
Count[i:R] = (when (i>0) one -> Count[i-1]).
Pile = Pile[N],
Pile[i:R] = (when (i>=6) take6 -> Pile[i-6] | when (i>=4) take4 ->
Pile[i-4] | when(i > 0) take1 -> Pile[i-1]).
set Take6 = {a.take6, b.take6}
set Take4 = {a.take4, b.take4}
set Take1 = {a.take1, b.take1}
Game = Game[N],
Game[i:R] = (when (i>=6) Take6 -> Game[i-6] | when (i>=4) Take4 ->
Game[i-4] | when(i > 0) Take1 -> Game[i-1]).
set A = {a.take6, a.take4, a.take1}
set B = {b.take6, b.take4, b.take1}
Alternate = (A -> B -> Alternate).
const N = 10
range R = 0..N
Count = Count[N],
6
7
8
9
10
11
12
13
14
15
16
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
1
2
3
7
There are 25 states in the resulting LTS.
After minimized, there are 17 states.
The minimized LTS is as following.
Count[i:R] = (when (i>0) one -> Count[i-1]).
Pile = Pile[N],
Pile[i:R] = (when (i>=6) take6 -> Pile[i-6] | when (i>=4) take4 ->
Pile[i-4] | when(i > 0) take1 -> Pile[i-1]).
set Take6 = {a.take6, b.take6}
set Take4 = {a.take4, b.take4}
set Take1 = {a.take1, b.take1}
Game = Game[N],
Game[i:R] = (when (i>=6) Take6 -> Game[i-6] | when (i>=4) Take4 ->
Game[i-4] | when(i > 0) Take1 -> Game[i-1]).
set A = {a.take6, a.take4, a.take1}
set B = {b.take6, b.take4, b.take1}
Alternate = (A -> B -> Alternate).
||Final = (Game || Alternate).
Process:
Final
States:
17
Transitions:
Final = Q0,
Q0 = (a.take6 -> Q1
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
1
2
3
4
5
6
7
8
There is no states where both a and b have valid moves.
9
States where a or b have a winning strategy are listed below.
|a.take4 -> Q6
|a.take1 -> Q10),
Q1 = (b.take4 -> Q2
|b.take1 -> Q3),
Q2 = STOP,
Q3 = (a.take1 -> Q4),
Q4 = (b.take1 -> Q5),
Q5 = (a.take1 -> Q2),
Q6 = (b.take6 -> Q2
|b.take4 -> Q7
|b.take1 -> Q9),
Q7 = (a.take1 -> Q8),
Q8 = (b.take1 -> Q2),
Q9 = (a.take1 -> Q1
|a.take4 -> Q8),
Q10 = (b.take6 -> Q3
|b.take4 -> Q9
|b.take1 -> Q11),
Q11 = (a.take4 -> Q1
|a.take6 -> Q4
|a.take1 -> Q12),
Q12 = (b.take4 -> Q3
|b.take6 -> Q5
|b.take1 -> Q13),
Q13 = (a.take6 -> Q2
|a.take4 -> Q4
|a.take1 -> Q14),
Q14 = (b.take4 -> Q5
|b.take1 -> Q15),
Q15 = (a.take4 -> Q2
|a.take1 -> Q16),
Q16 = (b.take1 -> Q7).
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
state num pebble who’s turn who always win
3 3 a a
4 2 b a
5 1 a a
6 6 b b
7 2 a b
8 1 b b
9 5 a b
12 7 b b
16 3 b b
1
2
3
4
5
6
7
8
9