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

Thanks for the reply and suggestions. Its also nice to know I didn't completely mess everything up :)

On Monday, August 28, 2017 at 3:42:37 AM UTC-4, Stephan Merz wrote:
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, peng...@xxxxxxxxxxx wrote:

I simply want to get any opinions, and see what I'm doing wrong, best practices, etc.

I started learning today via the video course, I got to the end of the videos so I'll read a book and hopefully learn more from there.

Thanks in advance for any critiques or resources.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.