/* 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.
*/