Game Module¶

Two-Player Deterministic Game¶

class iglsynth.game.game.Game(kind, vtype=None, etype=None, graph=None, file=None)[source]¶

Bases: iglsynth.util.graph.Graph

Represents a two-player deterministic zero-sum game.

The game could be concurrent or turn-based.

Game instance can be constructed by adding vertices and edges (See Constructing a Game Graph).

Parameters:

kind – (CONCURRENT or TURN_BASED) Whether the game is concurrent or turn-based.
vtype – (Game.Vertex or sub-class) The vertex type used to define the game instance.
etype – (Game.Edge or sub-class) The edge type used to define the game instance.
graph – (Game) A game instance from which “self” instance should be created.
file – (str) An absolute path of file from which the game should be loaded.

class Edge(u: iglsynth.game.game.Game.Vertex, v: iglsynth.game.game.Game.Vertex, act=None)[source]¶

Bases: iglsynth.util.graph.Edge

Represents an action-labeled edge of a game.

Edge represents a directed edge labeled with an action.
Two edges are equal if they share equal source and target vertices and have identical action labels.

Parameters:	u – (`Vertex`) Source vertex of edge. v – (`Vertex`) Target vertex of edge. act – (`Action` or None) An action label of edge. (Default: None)

Note

We have following cases depending on whether game is turn-based or concurrent.

(Turn-based) Action must be an Action object.
(Concurrent) Action must be a 2-tuple of (Action, Action)

act¶: Returns action associated with game edge.

source¶: Returns the source vertex of edge.

target¶: Returns the target vertex of edge.

class Vertex(name, turn=None, tsys_v=None, aut_v=None)[source]¶

Bases: iglsynth.util.graph.Vertex

Represents a vertex in game.

A game vertex is a 3-tuple, (name, tsys.v, aut.v). When game is defined using a graph, tsys.v and aut.v are both set to None.

Vertex must have a name.
When game is constructed from transition system and an automaton the vertex stores tsys and aut vertices.

Parameters:	name – (str) The name of the vertex. turn – (int) The id of player who will make the move at this state. tsys_v – (`iglsynth.game.tsys.TSys.Vertex`) Vertex of transition system. aut_v – (`iglsynth.logic.core.Automaton.Vertex`) Vertex of automaton.

Note

When game is defined using transition system and automaton, it is conventional to name vertices as (tsys_v.name, aut_v.name).

aut_vertex¶: Returns the automaton vertex associated with game vertex.

name¶: Returns the name of game vertex.

tsys_vertex¶: Returns the transition system vertex associated with game vertex.

turn¶: Returns the id of player who will make move in current state.

add_edge(e: iglsynth.game.game.Game.Edge)[source]¶

Adds an edge to the graph. Both the vertices must be present in the graph.

Parameters:	e – (`Graph.Edge`) An edge to be added to the graph.
Raises:	AttributeError – When at least one of the vertex is not in the graph. AssertionError – When argument e is not an `Graph.Edge` object.

add_edges(ebunch: Iterable[Graph.Edge])¶

Adds a bunch of edges to the graph. Both the vertices of all edges must be present in the graph.

Raises:	AttributeError – When at least one of the vertex is not in the graph. AssertionError – When argument e is not an `Graph.Edge` object.

add_vertex(v: iglsynth.game.game.Game.Vertex)[source]¶

Adds a new vertex to graph. An attempt to add existing vertex will be ignored, with a warning.

Parameters:	v – (`Graph.Vertex`) Vertex to be added to graph.

add_vertices(vbunch: Iterable[Graph.Vertex])¶

Adds a bunch of vertices to graph. An attempt to add existing vertex will be ignored, with a warning.

Parameters:	vbunch – (Iterable over `Graph.Vertex`) Vertices to be added to graph.

define(tsys=None, p1_spec=None)[source]¶

Defines and constructs the deterministic zero-sum game graph.

Parameters:	tsys – (`TSys`) Transition system over which game is defined. p1_spec – (`ILogic`) Logical specification that P1 must satisfy over transition system.

Note

A game graph can be defined in three possible ways.

Explicit construction of graph by adding vertices and edges.
By providing transition system and a logical specification for P1.
By providing an game field and two players. (Not presently supported).

edges¶: Returns an iterator over edges in graph.

final¶: Returns the set of final states of the game.

get_edges(u: iglsynth.util.graph.Graph.Vertex, v: iglsynth.util.graph.Graph.Vertex)¶

Returns all edges with source u and target v.

Parameters:	u – (`Graph.Vertex`) Vertex of the graph. v – (`Graph.Vertex`) Vertex of the graph.
Returns:	(iterator(`Graph.Edge`)) Edges between u, v.

has_edge(e: iglsynth.util.graph.Graph.Edge)¶

Checks whether the graph has the given edge or not.

Parameters:	e – (`Graph.Edge`) An edge to be checked for containment in the graph.
Returns:	(bool) True if the graph has the given edge, False otherwise.

has_vertex(v: iglsynth.util.graph.Graph.Vertex)¶

Checks whether the graph has the given vertex or not.

Parameters:	v – (`Graph.Vertex`) Vertex to be checked for containment.
Returns:	(bool) True if given vertex is in the graph, else False.

in_edges(v: Union[Graph.Vertex, Iterable[Graph.Vertex]])¶

Returns an iterator over incoming edges to given vertex or vertices. In case of vertices, the iterator is defined over the union of set of incoming edges of individual vertices.

Parameters:	v – (`Graph.Vertex`) Vertex of graph.
Raises:	AssertionError – When v is neither a `Graph.Vertex` object nor an iterable of `Graph.Vertex` objects.

in_neighbors(v: Union[Graph.Vertex, Iterable[Graph.Vertex]])¶

Returns an iterator over sources of incoming edges to given vertex or vertices. In case of vertices, the iterator is defined over the union of set of incoming edges of individual vertices.

Parameters:	v – (`Graph.Vertex`) Vertex of graph.
Raises:	AssertionError – When v is neither a `Graph.Vertex` object nor an iterable of `Graph.Vertex` objects.

kind¶: Returns the kind of game, whether TURN_BASED or CONCURRENT.

mark_final(v)[source]¶

Adds the given state to the set of final states in the game.

Parameters:	v – (`Game.Vertex`) Vertex to be marked as final.

num_edges¶: Returns the number of edges in graph.

num_vertices¶: Returns the number of vertices in graph.

out_edges(v: Union[Graph.Vertex, Iterable[Graph.Vertex]])¶

Returns an iterator over outgoing edges to given vertex or vertices. In case of vertices, the iterator is defined over the union of set of incoming edges of individual vertices.

Parameters:	v – (`Graph.Vertex`) Vertex of graph.
Raises:	AssertionError – When v is neither a `Graph.Vertex` object nor an iterable of `Graph.Vertex` objects.

out_neighbors(v: Union[Graph.Vertex, Iterable[Graph.Vertex]])¶

Returns an iterator over targets of incoming edges to given vertex or vertices. In case of vertices, the iterator is defined over the union of set of incoming edges of individual vertices.

Parameters:	v – (`Graph.Vertex`) Vertex of graph.
Raises:	AssertionError – When v is neither a `Graph.Vertex` object nor an iterable of `Graph.Vertex` objects.

p1_spec¶: Returns the specification of P1 in the game.

rm_edge(e: iglsynth.util.graph.Graph.Edge)¶

Removes an edge from the graph. An attempt to remove a non-existing edge will be ignored, with a warning.

Parameters:	e – (`Graph.Edge`) Edge to be removed.

rm_edges(ebunch: Iterable[Graph.Edge])¶

Removes a bunch of edges from the graph. An attempt to remove a non-existing edge will be ignored, with a warning.

Parameters:	ebunch – (Iterable over `Graph.Edge`) Edges to be removed.

rm_vertex(v: iglsynth.util.graph.Graph.Vertex)¶

Removes a vertex from the graph. An attempt to remove a non-existing vertex will be ignored, with a warning.

Parameters:	v – (`Graph.Vertex`) Vertex to be removed.

rm_vertices(vbunch: Iterable[Graph.Vertex])¶

Removes a bunch of vertices from the graph. An attempt to remove a non-existing vertex will be ignored, with a warning.

Parameters:	vbunch – (Iterable over `Graph.Vertex`) Vertices to be removed.

vertices¶: Returns an iterator over vertices in graph.