Hello,
your spec looks good to me. A few details:
| WithinBounds == IF pc = [state |-> "playing"] THEN |
| \/ p1 >= 21 /\ p1 - p2 < 2 |
| \/ p2 >= 21 /\ p2 - p1 < 2 |
| \/ p1 < 21 /\ p2 < 21 |
| ELSE |
| \/ (p1 >= p2 + 2 /\ p1 >= 21) |
| \/ (p2 >= p1 + 2 /\ p2 >= 21) |
| |
I'd write the test as pc.state = "playing", which is a bit easier to read (same in actions P1Scores and P2Scores). Also, the invariant could be strengthened to indicate the winning player in the ELSE case. Overall, I'd perhaps write something like
WithinBounds ==
\/ /\ pc.state = "playing"
/\ \/ p1 < 21 /\ p2 < 21
\/ p1 - p2 < 2 /\ p2 - p1 < 2 \* or: p1 \in p2-1 .. p2+1 /\ p2 \in p1-1 .. p1+1
\/ pc.state = "done" /\ pc.winner = "p1" /\ p1 >= 21 /\ p1 >= p2+2
\/ pc.state = "done" /\ pc.winner = "p2" /\ p2 >= 21 /\ p2 >= p1+2
You could make the spec even more readable by introducing an auxiliary predicate
GameOver ==
\/ p1 >= 21 /\ p1 >= p2+2
\/ p2 >= 21 /\ p2 >= p1+2
and using it to simplify the condition above as
WithinBounds ==
\/ pc.state = "playing" /\ ~ GameOver
\/ /\ pc.state = "done" /\ GameOver
/\ pc.winner = "p1" <=> p1 >= p2+2
That predicate is also helpful in defining the actions, e.g.
P1Scores ==
/\ pc.state = "playing"
/\ p1' = p1 + 1 /\ p2' = p2
/\ IF GameOver' THEN pc' = [state |-> "done", winner |-> "p1"] ELSE pc' = pc
But all of this is just a matter of style and personal preference.
Regards,
Stephan