(dtptb) Deterministic Two-Player Turn-based Games

SWinReach

class ggsolver.dtptb.SWinReach(graph, final=None, player=1, **kwargs)[source]

Computes sure winning region for player 1 or player 2 to reach a set of final states in a deterministic two-player turn-based game.

Implements Zielonka’s recursive algorithm.

Parameters

  • graph – (Graph or SubGraph instance) A graph or subgraph of a deterministic two-player turn-based game.

  • final – (Iterable) The set of final states. By default, the final states are determined using node property “final” of the graph.

  • player – (int) The player who has the reachability objective. Value should be 1 for player 1, and 2 for player 2.

get_final_states()[source]

Determines the final states using “final” property of the input graph.

graph()

Returns the input game graph.

is_solved()

Returns if the game is solved or not.

reset()[source]

Resets the solver to initial state.

solution()

Returns the solved game graph. The graph contains two special properties:

  • node_winner (node property): Maps each node to the id of player (1/2) who wins from that node.

  • edge_winner (edge property): Maps each edge to the id of player (1/2) who wins using that edge.

solve()[source]

Implements Zielonka’s recursive algorithm to determine winning nodes and edges for each player.

state2node(state)

Helper function to get the node id associated with given state.

win_acts(state)

Retuns the list of winning actions from the given state.

win_region(player)

Returns the winning region for the player.

winner(state)

Returns the player who wins from the given state.

SWinSafe

class ggsolver.dtptb.SWinSafe(graph, final=None, player=1, **kwargs)[source]

Computes sure winning region for player 1 or player 2 to remain within a set of final states in a deterministic two-player turn-based game.

Solves the dual reachability game to determine the winning nodes and edges in the safety game.

Parameters

  • graph – (Graph or SubGraph instance) A graph or subgraph of a deterministic two-player turn-based game.

  • final – (Iterable) The set of final states. By default, the final states are determined using node property “final” of the graph.

  • player – (int) The player who has the reachability objective. Value should be 1 for player 1, and 2 for player 2.

get_final_states()[source]

Determines the final states using “final” property of the input graph.

graph()

Returns the input game graph.

is_solved()

Returns if the game is solved or not.

reset()

Resets the solver to initial state.

solution()

Returns the solved game graph. The graph contains two special properties:

  • node_winner (node property): Maps each node to the id of player (1/2) who wins from that node.

  • edge_winner (edge property): Maps each edge to the id of player (1/2) who wins using that edge.

solve()[source]

Solves the dual reachability game to solve the safety game.

state2node(state)

Helper function to get the node id associated with given state.

win_acts(state)

Retuns the list of winning actions from the given state.

win_region(player)

Returns the winning region for the player.

winner(state)

Returns the player who wins from the given state.

ASWinReach

ggsolver.dtptb.ASWinReach

alias of SWinReach

ASWinSafe

ggsolver.dtptb.ASWinSafe

alias of SWinSafe