PlayGame: A Platform for Diagnostic Games

We introduce an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [6] 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 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. PlayGame implements a μ-calculus game and a full range of equivalence/preorder games on the Concurrency Workbench-New Century (CWB-NC).