Quick Start
Installation guide
PlayGame is built on the top of CWB-NC. It is available as part of CWB-NC with PlayGame. For the information about how to obtain the CWB-NC with PlayGame, you may refer to the download page. Installing CWB-NC with PlayGame is similiar to installing the CWB-NC 1.2. You may refer to its user manual for the detailed installation instruction.
After obtaining the CWB-NC with PlayGame, put all the distributation files in a directory you selected, say, /user/share/playgame. Change to that the directory and make install-cwb-nc.sh executable.
>chmod +x install-cwb-nc.sh >./install-cwb-nc.sh
You may be asked for the SML/NJ directory during the installation. If you want to use the graphic mode of PlayGame or CWB-NC, you will be asked for the Tcl/Tk binary directory. If you are not sure where is your Tcl/Tk executable, use "which wish" to find out. Please refer to the homepages of SML/NJ and Tcl/Tk for the information about how to obtain them.
To start CWB-NC in command line mode, type
>bin/cwb-nc ccs
This will bring CWB-NC with CCS (Calculus of Communicating Systems) as the front end modelling language.
To start CWB-NC in graphic mode, type
>bin/cwb-nc ccs -gui
Using PlayGame
Graphic mode or Command line mode
PlayGame can be activated in both graphic mode or command line mode, depending on which mode CWB-NC is activated. Besides the differenes on the interface, a major difference between two modes is how branch time is handled. In graphic mode, a play of the game may be branched by choosing different options at user's turns. In other words, The user may explore different possible plays at the same time; in the command line mode a play is a single thread, much like a traditional game like chess, although the user may still explore other options by backtracking.
Games in the graphic mode
Invoke a game
Once you bring up the CWB-NC in the graphic mode, you may invoke PlayGame using command line switch or the menu. To invoke PlayGame in the command line, simply add "-G" to your verification command. For instance, you may enter
>load examples/ccs/abp/abp.ccs >eq -S obseq -G Spec ABP-lossy
CWB-NC will invoke PlayGame after checking the observational equivalence between Spec and ABP-lossy.
You may also invoke PlayGame for the menu. Simply select "Enable playgame" when choosing a verification task. For instance, choose "Equivalences/Observational" from the menu and select "Enable playgame",
Play a game
The main interface of PlayGame shows the current play and the configuration of the selected step. The current play is represented as a tree, in which each node stands for a step. The step highlighted is the current step. To choose a different step, simply click its node.
The left side panel shows the information about the current step. We explain each component from top to bottom.
- The current configuration of the sides A and B. The sides A and B refer to the process and its specification in question. For instance, if we are checking whether the process 1 is equivalent to the process 2 on bisimulation, the sides A and B will refer to the processes 1 and 2 respectively. If the target problem is a model-checking problem whether the process 1 satisfies the temporal property f, then the sides A and B will refer to the process 1 and the formula f.
- Referee command. In addition to traditional two-player game, PlayGame also introduces the role of referee to enforce the rules. A referee executes the game rules: for instance, it will check the start configuration of each round to see whether someone already won the game. If so, it will declare the winner. Otherwise, it will decide who will be the next player in the current round, and so on. In addition to commands, the referee also has to give the reason to justify his decision.
- Current player. This field specifies who will move next.
- Choices and options. Depending on the configuration and the game rules, the current player may be allowed to choose from two sides. If "choice agent" is diabled, you can only select the designated side under the game rules. "Options" shows the list of possible next steps for the selected side. If the user is the current player, he can choose one from "Options" as his next step by either double-clicking his choice, or selecting the choice and clicking "Select".
- Players I and II. Players I and II are two roles the computer and the user can play. The player I is the one who believes that the correct answer to the verification problem is "yes", while the player II believes otherwise. refutes the verification result, and the player II is the one who advocates the result. In verification games, the user always plays the role who refutes the verification result, while the computer plays the one who advocates the result. The "Player I" and "Player II" specifies who will play which role depending on the outcoming of the verification task.
- In. Zoom in the canvas.
- Out. Zoom out the canvas.
- Next. Move on to the next step.
- Quit. Quit the PlayGame.
Backtracking
PlayGame allows the user to take abitrary steps back to examine other possibility. In the graphic mode, the user can do so by simply selecting the step that he want to re-examine. PlayGame will automatically set the selected step as the current step.
View a configuration
To view the configuration of a step in the game tree, the user may simply click the step on the tree, and the information about the selected step is shown on the left-side panel.
Reconfigure a game tree
Since PlayGame supports branch-time games, a play of the game will look like a tree. The user can choose to grow the tree and move a subtree. Growing the tree is just the alias of moving on to the next step. To move a subtree, simply drag and drop its root.
How to win a play?
Unfortunately this is something PlayGame cannot help :-). In PlayGame, the user takes the role who refutes the correctness of a verificaiton result, and the computer has a winning strategy to win each and every play. By losing the game, the user will understand the correctness of the verification result.
Command line mode
Play a game
PlayGame can be invoked by simply adding "-G" to a verification command. For instance,
>load examples/ccs/abp/abp.ccs >eq -S obseq -G Spec ABP-lossy Building automaton... Done building automaton. Transforming automaton... Done transforming automaton. Building reference automaton. Done building reference automaton. Building automaton... Done building automaton. Computing the mapping... Checking the evidence......done initialization succeed Two agents are related. User will act as player I while computer will act as player II. Activate the game module ... Verifying the players. Player I is User and player II is User Starting configuration: Agent1: Spec Agent2: ABP-lossy Referee: User goes first to choose from either agent Type 1 to choose agent 1, and 2 to choose agent 2: (1/2) 1
CWB-NC starts with the regular verification task, but during the process, the underlying model checker also preserves the evidence that will be used in the follow-up PlayGame session. At the beginning of each play, PlayGame will annouce which roles the computer and the user will play depending on the outcoming of verification.
At the beginning of each round, PlayGame shows the starting configuration, and the referee decides who will move next according to the game rules. In this particular example, the user will play as the player I since the verification result is positive, and he can choose a side in each round. Once he decide a side, the play will move on with a list of all the options the user can choose as the next step,
User chose agent 2,
Available user options:
Option 0: --<send>-->(R0 | Mlossy | S0')\Internals
Option 1: --<t>-->('sack1.R0 | Mlossy | S0)\Internals
Which one do you want to choose?[(0-1) to choose, or (r)eview options]:0
The user can make his decision, or choose to review an option.
Step 2: Computer matched user's choice by the transition:
--<<send>>-->'receive.Spec
Continue game?[(c)ontinue, e(x)it or (b)ack]: c
PlayGame will compute the next step for the computer according to the evidence supplied by the checker. The user may also choose to take back a few steps. Finally, the play reachs its end with the winner, which is always the computer, being announced.
################## Round 6####################
Starting configuration:
Agent1: Spec
Agent2: ('sack0.R1 | ('rack0.Mlossy + Mlossy) | S1)\Internals
Found Repetition.
Referee: No computer/user interfere needed.
Reason: Same Configuration is encountered twice.
Computer won. Game over.
Backtracking
At the end of each round, the user will be asked whether he want to take some steps back. If he chooses "yes", he can then specifies how many steps he want to take back.
Continue game?[(c)ontinue, e(x)it or (b)ack]:b How many steps you want to go back?[(0-2)]:1
Using CWB-NC graphic user interface
CWB-NC with PlayGame also includes a new graphic user interface, which is thoroughtly re-written in SML with SML/Tk package. To use CWB-NC gui, you must choose the GUI option when installing CWB-NC. CWB-NC GUI requires that Tcl/Tk be installed.
Activate the GUI
To activate the gui, simply type the command,
>cwb-nc ccs -gui
This will bring the CWB-NC GUI.
The main interface has three parts: a menu, a side panel showing all the bounded variables, and a command window. There are two ways to issue a command: use the menu, or type in the command window just as in command line mode. All the commands in the command line mode is still valid and may be entered in the command window. The interface of some commands may be changed in the graphic mode. For instance, PlayGame will work in the graphic mode if the CWB-NC GUI is used, regardless that the verification command is issued on the command line or by the menu selection.
The side panel lists all the bounded variables. The definition of each variable, you may select the variable and click "Definition", or simply double-click the variable.
Most of commands have their counterparts in the menu and can be activated easily using the menu.
Start a verification task
User can choose to issue verification commands on the command window or use the menu. For instance, to check the process "ABP-lossy " on the property "can_deadlock", user first load the sample files "abp.ccs" and "abp.mu" using "File/Load", and then select "Model Checking/Mu-Calculus and CTL".
Check "Enable playgame" if you want to use PlayGame, and click "Run".
Contacts
Your experience and opinion count! for the questions regarding PlayGame, please contact me. For the general inquries and comments on CWB-NC, please contact CWB development team.