1
2
const N = 10
range R = 0..N
Count = Count[N],
Count[i:R] = (when (i>0) one -> Count[i-1]).
3
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]).
4
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]).
5
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).
6
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).
||Final = (Game || Alternate).
7
There are 25 states in the resulting LTS.
After minimized, there are 17 states.
The minimized LTS is as following.
Process:
Final
States:
17
Transitions:
Final = Q0,
Q0 = (a.take6 -> Q1
|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
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.
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