# Re: [tlaplus] New to TLA, made my first ever specification, thoughts?

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

On 28 Aug 2017, at 03:53, pengui...@xxxxxxxxxxx wrote: