PlayGame

PlayGame

PlayGame is an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [Tan02a] to improve code sharing among various diagnostic games and reduce the cost of introducing a new game. PlayGame synthesizes the winning strategy using the evidence [TanCle02, Tan02b] that is an abstract and uniform encoding of the proof computed by a checker, and hence instead of relying on any particular checker the tool works on a variety of checkers that can be extended to produce such evidence. The current version of PlayGame implements game-based diagnostic routines for mu Calculus model checking game and a full range of equivalence/preorder semantics including: bisimulation /simulation, weak bisimulation /simulation, trace equivalence /preorder, and testing equivalence /preorder. Blow is the architecture design of PlayGame. Readers may refer to [Tan04] and its accompanying slides for an overivew of PlayGame.

Features

PlayGame supports several advanced features such as,

  1. A graphic user interface, in addition to a textual user interface. The GUI allows the user to reconfigure the game graph during a play. PlayGame has a build-in graphic layout and manuever algorithm to support the reconfiguration. The graphic user interface is simple and intuitive.
  2. Games for positive verification results. Typically a diagnostic routine will help the user understand the failure when the verification result is false. In addition to this typical application, PlayGame also allows the user to play game with the computer when the verification result is positive, in which case the user may be able to understand the correctness of a verification result by playing game with the computer.
  3. Backtracking. The user can choose to take back aribtrary steps during a play. In the graphic mode, the user may check a previous configuration by simply clicking a node in the game graph.
  4. Branch-time games. The user may play several branches of the game at the same time by trying out different choices during a play. He may also remove a branch if needed.

Implementation note

PlayGame is built on the top of CWB-NC. The core of PlayGame is implemented in SML using SML/NJ. Its graphic user interface is implemented in SML with SML-TK, a TCL/TK graphic extension for SML. Contact me for any questions regarding PlayGame.