# Gridworld Problem: Game on Graph¶

This example demonstrates how to construct a game on graph using a `Gridworld`

transition system and an `LTL`

specification for P1.

In general, there are three ways to define a game on graph, namely

- By explicitly adding vertices and edges to the graph and marking the accepting states,
- By providing a transition system and a formal specification,
- By providing a game field and player objects.

Presently, in IGLSynth v0.2.3, only first two are supported. See Gridworld Problem: Game on Graph for an example of constructing game on graph by explicitly adding vertices and edges.

## Define Transition System¶

To define a game using transition system and P1’s specification, first define the transition system.
In general, a transition system may be defined using `TSys`

class.
In this example, we use a predefined `Gridworld`

transition system from
`iglsynth.game.gridworld`

module:

```
from iglsynth.game.gridworld import *
# Define transition system
tsys = Gridworld(kind=TURN_BASED, dim=(3, 3), p1_actions=CONN_4, p2_actions=CONN_4)
tsys.generate_graph()
```

## Define LTL Specification¶

To define P1’s objective using an LTL specification, import the logic module:

```
from iglsynth.logic.ltl import *
```

An `LTL`

formula is defined over an alphabet. Hence, we start by defining `AP`

objects
using which we will construct an alphabet.

In this demo example, we will represent P1’s objective to reach to a goal. Such a reachability specification can be written as \(\varphi = \Diamond a\) where \(a\) is an AP representing goal. So, define the AP as:

```
GOAL = (0, 0)
a = AP("a", lambda st, *args, **kwargs: st.coordinate[0:2] == GOAL)
```

and the specification as:

```
spec = LTL("Fa", alphabet=Alphabet([a]))
```

## Define Game Object¶

Given a transition system and specification, we will now define a game. To define game, we require the game module:

```
from iglsynth.game.game import *
```

Now, instantiate and define a game as follows:

```
game = Game(kind=TURN_BASED)
game.define(tsys, spec)
```

## Solve the Game¶

The final step is to invoke a solver to solve the game. We will use Zielonka’s algorithm to solve the above game. Note that Zielonka’s algorithm computes winning region for P1 in a deterministic two-player zero-sum game.

In IGLSynth, Zielonka’s algorithm is implemented in `zielonka`

module:

```
from iglsynth.solver.zielonka import ZielonkaSolver
```

To run the solver, first instantiate it and call the `solve`

method:

```
solver = ZielonkaSolver(game)
solver.solve()
```

The `solver.solve()`

runs the solver on the `Game`

object `game`

that encodes the game on graph.
The solution of solver can be accessed using the properties:

```
print(solver.p1_win)
print(solver.p2_win)
```

which returns the winning sets for P1 and P2.