The Game Editor

Note: currently, only two-player games are supported.

Different editing steps are conveniently indicated by clicking on the appropriate icons. Currently, there are six of them.

: This is the pointer icon. Select it when you want to point to some game component and change its attributes. Once the pointer is correctly positioned on the component, click the right mouse button and follow the instructions. You may left-click on a state, hold the mouse button, and drag the state to a new location. You may also drag and reshape the arrow of a transition. To change the label of a transition, point and then click the left mouse button.
More options are available by pointing at the background and clicking the right mouse button.

: This is the state creator for player 0 icon. Select it when you want to create a state of player 0. Once the pointer is correctly positioned at the location where a new state should be, click the left mouse button to drop the new state on that location.

: This is the state creator for player 1 icon. Select it when you want to create a state of player 1. Once the pointer is correctly positioned at the location where a new state should be, click the left mouse button to drop the new state on that location.

: This is the transition creator icon, whose usage is similar to the state creator icon. For a transition to go from state s₀ to state s₁, point and click on state s₀ and then drag the arrow to state s₁.
There are two types of symbols:

1. Propositional Symbols
   A propositional input symbol to the automaton is represented by a string, consisting of blank-separated substrings, that encodes a truth assignment to the atomic propositions appearing in the intended temporal formula. For temporal formulae with two atomic propositions p and q, the alphabet will be {p q, p ~q, ~p q, ~p ~q}, where "p q", "p ~q", "~p q", and "~p ~q" are the four "symbols" encoding all four possible truth assignments. The symbol "p ~q", for instance, encodes the truth assignment that p is true and q is false. A transition labled with a partially specified symbol "p" will be treated as two transitions labeled respectively with "p q" and "p ~q". The order in which the propositional literals appear is immaterial, but they must be separated by a blank space.

2. Classical Symbols
   A classical input symbol to the automaton is represented by a character string without blank spaces. For example, the alphabet may be {stop, go, turn}, where "stop", "go", and "turn" are the three symbols.

: This is the eraser icon. Select it when you want to delete some game component. Once the pointer is correctly positioned at the component that is to be deleted, click the left mouse button to commit the deletion. It is possible to undo a deletion; click the right mouse button for instructions.

: This is the acceptance condition setter icon. Select it when you want to define the acceptance condition of the game you have created. It essentially works by your pointing and clicking; try it and you will see how it works.

You can zoom in/out by Ctrl+Mouse wheel.