Constructing a Game Graph¶
This example demonstrates how to construct a simple game on graph. 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.
IGLSynth v0.2.2 only supports explicit construction of graph.
Define Game by Explicit Construction¶
iglsynth.game.game provides necessary classes to define a game on graph.
Hence, first import the
from iglsynth.game.game import Game
Game class defines a deterministic two-player zero-sum game on graph.
Game can be either
For this example, let us consider a
TURN_BASED game on graph shown in following image.
First, instantiate a game object:
game = Game(kind=TURN_BASED)
Now, add the vertices and assign each vertex to a player.
When a vertex has
turn = 1, player 1 (circle) will make a move.
When a vertex has
turn = 2, player 2 (box) will make a move.
The vertex in a
game (an instance of
Game class) must be of type
Game.Vertex or its derivative.
Hence, it is recommended to instantiate a new game vertex as
vertices = list() for i in range(8): if i in [0, 4, 6]: vertices.append(game.Vertex(name=str(i), turn=1)) else: vertices.append(game.Vertex(name=str(i), turn=2)) game.add_vertices(vertices)
and mark the vertices 3, 4 as final:
# Set the states as final v3 = vertices v4 = vertices game.mark_final(v3) game.mark_final(v4)
Finally, add the edges to the game. Similar to vertices, we instantiate new edges as
# Add edges to the game graph edge_list = [(0, 1), (0, 3), (1, 0), (1, 2), (1, 4), (2, 4), (2, 2), (3, 0), (3, 4), (3, 5), (4, 3), (5, 3), (5, 6), (6, 6), (6, 7), (7, 0), (7, 3)] for uid, vid in edge_list: u = vertices[uid] v = vertices[vid] game.add_edge(game.Edge(u=u, v=v))
Now, given a game we invoke the
to compute the winning regions for players 1 and 2:
from iglsynth.solver.zielonka import ZielonkaSolver solver = ZielonkaSolver(game) solver.solve()
solver.solve() runs the solver on the
game that encodes the game on graph.
The solution of solver can be accessed using the properties:
which returns the winning sets for P1 and P2.