// Place global declarations here.
const int N = 3; // # player minions
const int MOVES_NUM = 2; // # Number of moves
typedef int[0,N-1] id_t;
typedef int[1,MOVES_NUM] move_t;
typedef int[0,MOVES_NUM] firebase_move_t; // 0 is for null (when no moves has yet been selected)
chan clientMove[N], serverUpdate[N], getMove, timerReset;
broadcast chan stateChanged, resetFirebase;
clock x;
firebase_move_t moveBuffer = 0;
firebase_move_t firebaseMoves[N];ClientMinionconst id_t id// Place local declarations here.
move_t move = 1;ReadyToSendWaitClientWaitServerWaitPlayerFirebaseMinionconst id_t idResetSentMoveNullFirebaseResetterWaitForFirebaseIdleServerThreadconst id_t id
firebase_move_t movesCopy[N];
bool shouldCalculate;
bool haveAllDecided() {
int i;
for (i = 0; i < N; i++) {
if (movesCopy[i] == 0) {
return false;
}
}
return true;
}
void resetMovesCopy() {
int i;
for (i = 0; i < N; i++) {
movesCopy[i] = 0;
}
}WaitFirebaseCalWaitServerMoveconst move_t idServerTimeoutconst int TIMEOUT = 30;
firebase_move_t movesCopy[N];
void resetMovesCopy() {
int i;
for (i = 0; i < N; i++) {
movesCopy[i] = 0;
}
}CalTimeoutRunning// Place template instantiations here.
// List one or more processes to be composed into a system.
system ClientMinion, FirebaseMinion, FirebaseResetter, ServerThread, ServerTimeout, Move;
E<>ServerTimeout.Timeout
E[] not ServerTimeout.Timeout
A[] not deadlock
A[] forall(i:id_t) (ServerThread(i).Cal imply forall(j:id_t) (ServerThread(i).movesCopy[j] == ClientMinion(j).move))
A[] ServerTimeout.Cal imply forall(i:id_t) (ServerTimeout.movesCopy[i] == ClientMinion(i).move)