The Automaton/Game Editors

Note for ω-automata: in the standard presentation of an ω-automaton, input symbols are labeled on transitions rather than states; we call these label-on-transition automata. Those with input symbols labeled on states are called label-on-state automata. At present, label-on-transition automata are the default and fully supported, while label-on-state automata can only be reshaped or converted to label-on-transition automata for further manipulation.

Note for alternating automata: the standard presentation of an alternating automaton contains and-branches and or-branches. In GOAL, an and-branch is represented by bundling transitions with a box node, while an or-branch is the same as in ω-automata.

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

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

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

1.

: This is the pointer icon. Select it when you want to point to some automaton 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.

2.

: This is the state creator icon. Select it when you want to create an automaton state. 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 icon. Select it when you want to create a state. It works the same way as in the case of ω-automata.

: This is the and-branch creator icon. Select it when you want to create an and-branch. Once the pointer is correctly positioned at the location where a new and-branch should be, click the left mouse button to drop a new box node on that location. Every transition in the and-branch should go first to the box node (this can be shared among the transitions) and then to the destination state. The input symbol should be placed on the transition from the source state to the box.

: This is the state creator for player 0 icon. Select it when you want to create a state of player 0. It works the same way as in the case of ω-automata.

: This is the state creator for player 1 icon. Select it when you want to create a state of player 1. It works the same way as in the case of ω-automata.

More options are available by pointing at the background and clicking the right mouse button.

3.

: 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 input 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.

More options are available by pointing at the background and clicking the right mouse button.

4.

: This is the eraser icon. Select it when you want to delete some automaton 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.

5.

: This is the acceptance condition setter icon. Select it when you want to define the acceptance condition of the automaton you have created. It essentially works by your pointing and clicking; try it and you will see how it works. To define a parity condition may be less intuitive. You will need to create a collection of sets named F0, F1, F2, etc. that represent an assignment of colors/parities to the states. States in F0 are assigned color 0, states in F1 assigned 1, states in F2 assigned 2, etc. We assume the min-even parity condition, i.e., a run is accepting if the minimum color of infinitely repeated states in the run is even.

: This is the winning condition setter icon. Select it when you want to define the winning condition of the game you have created. It works the same way as the acceptance condition setter icon of ω-automata.

More options are available by pointing at the background and clicking the right mouse button.