This module implements functions for solving parity games with Zielonka's algorithm.
Type  Description 
Function or value  Description 
Full Usage:
Attractor pg i phi
Parameters:
ParityGame
i : int
phi : Set<int>
Returns: Set<int> * Set<int * int>




Full Usage:
Automaton2MooreGame auto
Parameters:
AutomatonExpl<string, string, int>
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

Automaton2MooreGame converts an automaton to a parity game that aims at the synthesis of a Moore machine, i.e., outputs are determined by the state only. The ranks are determined in that accepting states get rank 1 while other states of the automaton have rank 0, and the intermediate states will have the rank of their source state.




CopsAndRobber game: a cop and a robber are placed on an undirected graph and make alternating moves. Clearly, the cop aims at catching the robber and the robber wants to escape forever, so that we have a safety or liveness game. The game is also known as a video game called Pacman, and graphs that are copwin graphs are well researched [AiFr84,GaTT18]. The function below is given the edge relation where only one direction between two vertices is sufficient, and the initial state (r,c,t) where r and c are the vertices where the robber and the cop are located at the beginning, and t is a boolean value that is true if the cop is making the next move. The function converts the graph to a game graph whose nodes are triples (r,c,t) like the initial state, and solves the game. The function returns a triple (pg,win,strat) where pg is the parity game and win[i] are the winning states of player i and finally strat[i] is the strategy of player i, where player 0 is the cop and player 1 is the robber.


This function is the teaching tool for the CopRobberGame; it reads the edge relation, and the initial state from a html form input, and uses function CopRobberGame to generate and solve the graph game. The tool then prints the solved graph game as svg graphics on the generated html page and prints also a transition relation for the graph game if viewed as a Kripke structure. The locations of the robber and cop are then binary encoded with boolean variables rN,...,r0 and cN,...,c0, resp.

Full Usage:
DetF2LivenessGame auto
Parameters:
AutomatonExpl<string, string, int>
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetF2LivenessGame converts a given DetF automaton to a LivenessGame where player 0 tries to reach accepting states, i.e., rank1 states, and where player 1 tries to avoid these.

Full Usage:
DetFG2ParityGame auto
Parameters:
AutomatonExpl<string, string, int>
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetFG2ParityGame converts a given DetFG automaton to a ParityGame where player 0 tries to visit from a certain point of time onwards only accepting states of the given DetFG automaton, and player 1 tries to infinitely often escape from these.

Full Usage:
DetG2SafetyGame auto
Parameters:
AutomatonExpl<string, string, int>
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetG2SafetyGame converts a DetG automaton to a safety game where player 0 aims at exclusively using safe states (having rank 1), and where player 1 aims at reaching a rank0 state.

Full Usage:
DetGF2ParityGame auto
Parameters:
AutomatonExpl<string, string, int>
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetGF2ParityGame converts a given DetGF automaton to a ParityGame where player0 tries to infinitely often visit accepting states of the DetGF automaton, and player 1 tries to visit them only finitely often.




generic example from Frie11 where Frie11(n) recursively calls Frie11(n1) and Frie11(n2) to prove exponential runtime

Full Usage:
ParityGame2Dot ostr stateLabel transLabel (win, strat) pg
Parameters:
TextWriter
stateLabel : Map<int, string>
transLabel : Map<(int * int), string>
win : Set<int>[]
strat : Set<int * int>[]
pg : ParityGame





parsing a parity game from a string; the syntax is explained by the following example: player0 3,4,5,6; player1 0,1,2,7; ranks 0:0; 1:1; 2:2; 3:3; 4:4; 5:5; 6:6; 7:8; transitions 0>1; 0>3; 1>4; 1>6; 2>0; 2>5; 3>2; 4>0; 4>1; 5>7; 6>1; 6>7; 7>2; 7>5;






Solve a liveness game which is encoded as a parity game with ranks 1 for the states that must be reached by player 0 (liveness) and must be avoided by player 1 (safety).


This function solves a given parity game by Zielonka's recursive algorithm. It returns a tuple (win,strat) where win[i] are the winning states of player i and strat[i] is the strategy of player i.


Solve a safety game which is encoded as a parity game with ranks 1 for the safe states that must be exclusively used by player 0 (safety) and where player 1 tries to escape from.





Full Usage:
ZielonkaExplain gameNum pg
Parameters:
int
pg : ParityGame
Returns: Set<int>[] * Set<int * int>[] * (int * ParityGame * int * Set<int> * int * (Set<int> * Set<int * int>) * (Set<int>[] * Set<int * int>[]) * (int * (Set<int> * Set<int * int>) * (Set<int>[] * Set<int * int>[])) option * Set<int>[] * Set<int * int>[]) list * int

This function solves a given parity game by Zielonka's recursive algorithm. It returns a tuple (win,st,traceL,gA) where win[i] are the winning states of player i, st[i] is the strategy of player i, traceL is a list of the recursive calls with detailed information of intermediate steps, and gA is the latest game number used in that list. The initial call requires a number gameNum which is the first number of these games.
