The Scribble Multiparty Session model for a WordGuess game

WordGuess.scr

module WordGuess;

// This is an attempt to model a game of "word guess"
// All communication flows through board (maybe that makes this whole thing
// trivial)
// There are 4 players, 2 on red team and 2 on blue team
//
// Roughly, there is a leader selected in a round-robin fashion, the leader sees
// a full board of words and shouts a word+#. The player on that team uses the
// word as a hint and can make up to # of guesses unless they get one wrong.
// If they get one very-wrong, then the round ends instantly and the other team
// wins. The next round starts 

global protocol Proto(role Board, role Red1, role Red2, role Blue1, role Blue2) {
  rec Game {
    choice at Board {
      Leader() from Board to Red1;
      Leader() from Board to Blue1;
      do Round(Board, Red1, Blue1, Red2, Blue2);
      Leader() from Board to Red2;
      Leader() from Board to Blue2;
      do Round(Board, Red2, Blue2, Red1, Blue1);
      continue Game;
    } or {
      do EndGame(Board, Red1, Red2, Blue1, Blue2);
    }
  }
}

global protocol EndGame(role Board, role P1, role P2, role P3, role P4) {
  Done() from Board to P1;
  Done() from Board to P2;
  Done() from Board to P3;
  Done() from Board to P4;
}

global protocol Round(role Board, role RedLeader, role BlueLeader, role RedPlayer, role BluePlayer) {
  // a blank board only shows words after they are guessed
  BlankInit() from Board to RedPlayer;
  BlankInit() from Board to BluePlayer;

  // a full board shows all information
  FullInit() from Board to RedLeader;
  FullInit() from Board to BlueLeader;

  rec FullTurn {
    choice at Board {
      // randomly generate who goes first, wlog assume RedLeader always goes first
      do SingleTurn(Board, RedLeader, RedPlayer);
      choice at Board {
        // the wrong/stop case

        // assume we can always take a full Red/Blue turn cycle
        do SingleTurn(Board, BlueLeader, BluePlayer);
        choice at Board {
          // the wrong/stop case
          continue FullTurn;
        } or {
          // the very-wrong case
          do EndRound(Board, RedLeader, BlueLeader, RedPlayer, BluePlayer);
        }
      } or {
        // the very-wrong case
        do EndRound(Board, RedLeader, BlueLeader, RedPlayer, BluePlayer);
      }
    } or {
      // one team has finished all their words on the board
      do EndRound(Board, RedLeader, BlueLeader, RedPlayer, BluePlayer);
    }
  }

}

global protocol EndRound(role Board, role P1, role P2, role P3, role P4) {
  IncrementScore() from Board to P1;
  IncrementScore() from Board to P2;
  IncrementScore() from Board to P3;
  IncrementScore() from Board to P4;
}

global protocol SingleTurn(role Board, role Leader, role Player) {
  Start() from Board to Leader;
  ShoutWord() from Leader to Board;
  EchoWord() from Board to Player;

  rec Guess {
    choice at Player {
      CorrectGuess() from Player to Board;
      Correct() from Board to Player;
      continue Guess;
    } or {
      WrongGuess() from Player to Board;
      Wrong() from Board to Player;
    } or {
      VeryWrongGuess() from Player to Board;
      VeryWrong() from Board to Player;
    } or {
      // either stopped on purpose or done
      Stop() from Player to Board;
    }
  }
}