PingPong.tla

------------------------------ MODULE PingPong ------------------------------
EXTENDS Integers
(***************************************************************************)
(* A simple ping pong game designed for learning                           *)
(***************************************************************************)

VARIABLES p1, \* Points of player 1
          p2, \* Points of player 2
          pc  \* What the current state of the game is

(***************************************************************************)
(* The state of the game.  We can either be playing or the game can be    *)
(* done with one the two players being the winner                          *)
(***************************************************************************)

PcState == [state: {"playing"}] \cup [state: {"done"}, winner: {"p1", "p2"}]

(***************************************************************************)
(* The basic types of the variables.  p1 and p2 are counters for the score *)
(* of both players.  pc is the current state of the game                   *)
(***************************************************************************)

TypeOK == /\ pc \in PcState
          /\ p1 \in Nat
          /\ p2 \in Nat

(***************************************************************************)
(* What constitutes valid scores in ping pong.  When playing, both can be  *)
(* below 21 or if one of the two players has equal to or above 21 points,  *)
(* the player's score must be within 2 points of the other player.  For    *)
(* example: 21 and 20 is still playable while 21 and 19 or 21 and 18 means *)
(* the game is done.  When finished, one player must have at least 2       *)
(* points more than the other and have over 21 points.                     *)
(***************************************************************************)

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)
                
(***************************************************************************)
(* Games start off with both players at zero points                        *)
(***************************************************************************)

Init == /\ p1 = 0
        /\ p2 = 0
        /\ pc = [state |-> "playing"]

-----------------------------------------------------------------------------

(***************************************************************************)
(* What should occur when p1 scores.  p1's score should increase and if    *)
(* the game is done (p1 has 21 points or over and 2 points more than p2),  *)
(* it should be finished with p1 as the winner                             *)
(***************************************************************************)

P1Scores == /\ pc = [state |-> "playing"]
            /\ p1' = p1 + 1
            /\ IF p1' >= 21 /\ p1' >= p2 + 2 THEN
               /\ pc' = [state |-> "done", winner |-> "p1"]
               /\ p2' = p2
               ELSE UNCHANGED<<pc, p2>>

(***************************************************************************)
(* What should occur when p2 scores, the logic is the exact same as p1     *)
(* scoring; however, the players are switched.                             *)
(***************************************************************************)

P2Scores == /\ pc = [state |-> "playing"]
            /\ p2' = p2 + 1
            /\ IF p2' >= 21 /\ p2' >= p1 + 2 THEN
               /\ pc' = [state |-> "done", winner |-> "p2"]
               /\ p1' = p1
               ELSE UNCHANGED<<pc, p1>>

(***************************************************************************)
(* What should the next state be run off.                                  *)
(***************************************************************************)

Next == \/ P1Scores
        \/ P2Scores

=============================================================================
\* Modification History
\* Last modified Sun Aug 27 21:35:22 EDT 2017 by PenguinSoccer
\* Created Sun Aug 27 20:09:47 EDT 2017 by PenguinSoccer