Averest


ReactiveSynthesis Module

This module implements functions for solving parity games with Zielonka's algorithm.

Types

Type Description

ParityGame

data type for storing parity games

Functions and values

Function or value Description

Attractor pg i phi

Full Usage: Attractor pg i phi

Parameters:
Returns: Set<int> * Set<int * int>

compute the i-attractor of a set of states phi in paritry game pg

pg : ParityGame
i : int
phi : Set<int>
Returns: Set<int> * Set<int * int>

AutomataSynthesisTool qscoll

Full Usage: AutomataSynthesisTool qscoll

Parameters:

The teaching tool for omega-automata synthesis.

qscoll : NameValueCollection

Automaton2MooreGame auto

Full Usage: Automaton2MooreGame auto

Parameters:
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.

auto : Automaton
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

BooleanUnificationTool qscoll

Full Usage: BooleanUnificationTool qscoll

Parameters:

The teaching tool for boolean unification.

qscoll : NameValueCollection

DetF2LivenessGame auto

Full Usage: DetF2LivenessGame auto

Parameters:
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., rank-1 states, and where player 1 tries to avoid these.

auto : Automaton
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetFG2ParityGame auto

Full Usage: DetFG2ParityGame auto

Parameters:
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.

auto : Automaton
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetG2SafetyGame auto

Full Usage: DetG2SafetyGame auto

Parameters:
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 rank-0 state.

auto : Automaton
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DetGF2ParityGame auto

Full Usage: DetGF2ParityGame auto

Parameters:
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.

auto : Automaton
Returns: ParityGame * Map<int, string> * Map<(int * int), string>

DiRu19

Full Usage: DiRu19

Returns: ParityGame

example of DiRu10:

Returns: ParityGame

Frie11 n

Full Usage: Frie11 n

Parameters:
    n : int

Returns: ParityGame

generic example from Frie11 where Frie11(n) recursively calls Frie11(n-1) and Frie11(n-2) to prove exponential runtime

n : int
Returns: ParityGame

ParityGame2Dot ostr stateLabel transLabel (win, strat) pg

Full Usage: ParityGame2Dot ostr stateLabel transLabel (win, strat) pg

Parameters:

writing a parity game as graphiz graph

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

ParityGameTool qscoll

Full Usage: ParityGameTool qscoll

Parameters:

The teaching tool for solving parity games.

qscoll : NameValueCollection

ParseParityGame s

Full Usage: ParseParityGame s

Parameters:
    s : string

Returns: 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;

s : string
Returns: ParityGame

Remove pg q

Full Usage: Remove pg q

Parameters:
Returns: ParityGame
pg : ParityGame
q : Set<int>
Returns: ParityGame

Restrict pg q

Full Usage: Restrict pg q

Parameters:
Returns: ParityGame
pg : ParityGame
q : Set<int>
Returns: ParityGame

SolveLivenessGame pg

Full Usage: SolveLivenessGame pg

Parameters:
Returns: Set<int>[] * Set<int * int>[]

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).

pg : ParityGame
Returns: Set<int>[] * Set<int * int>[]

SolveParityGame pg

Full Usage: SolveParityGame pg

Parameters:
Returns: Set<int>[] * Set<int * int>[]

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.

pg : ParityGame
Returns: Set<int>[] * Set<int * int>[]

SolveSafetyGame pg

Full Usage: SolveSafetyGame pg

Parameters:
Returns: Set<int>[] * Set<int * int>[]

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.

pg : ParityGame
Returns: Set<int>[] * Set<int * int>[]

Wiki

Full Usage: Wiki

Returns: ParityGame

example of Wikipedia:

Returns: ParityGame

ZielonkaExplain gameNum pg

Full Usage: ZielonkaExplain gameNum pg

Parameters:
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.

gameNum : 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