Untitled

/* constants and mtypes */
mtype = { BALL }

/* global variables and channels */
chan p2p = [1] of { mtype }  
chan r2p = [1] of { mtype }  

/* macros for the property interface -- needed for reference properties */ 
#define allBalls (len(p2p) + len(r2p))

/* Your LTL properties */
ltl singleBallForever { <>(allBalls == 1) } // for PingPong.pml

/* Any mandatory sanity-check LTL properties: these must pass for non-zero grade */

/* for PingPong.pml only */
ltl initiallyNoBallsMustNotFailForCredit { (allBalls == 0) && []true }
ltl allBallsCannotBeConstantMustNotFailForCredit { ![](allBalls == 0) && ![](allBalls == 1) && ![](allBalls == 2) && []true }


/* proctypes */

/* comment your code only if necessary, 
   explaining what each proctype is supposed to be 
*/
proctype Player(short id) {
   bool hasBall = false;
   if 
   :: (id == 0) ->
      do
      :: r2p?BALL -> {
            hasBall = true;
            break;
         }
      od; 
   fi;

   do
   :: (hasBall == true) ->
      p2p!BALL -> hasBall = false;
   :: (hasBall == false) ->
      p2p?BALL -> hasBall = true;
   od;
}

proctype Referee() {
   r2p!BALL;
}

init { 
   run Referee();
   run Player(0);
   run Player(1);
}

/*

REPORT

Your report goes here if required. 

*/