# Reactive Synthesis

## Solving Parity Games

The tool below can be used to solve parity games by Zielonka's algorithm. For the specified parity game, it computes the winning states of both players as well as their strategies, and shows how these were computed by Zielonka's algorithm.

The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed for both players. The ranks of the states are given as declarations in the rank section where state s is given rank r by writing s:r. Finally, transitions are given in the form i->j denoting a transition from state i to state j.

 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;

## Reactive Synthesis

The tool below can be used to synthesize a Moore automaton (if possible) that will select output values in each state such that a given safety/liveness/persistence/fairness property is achieved. Note that the given omega-automaton has to be deterministic in the sense that every states has for every pair (i,o) of an input and an output exactly one transition.

The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed for both players. The ranks of the states are given as declarations in the rank section where state s is given rank r by writing s:r. Finally, transitions are given in the form i->j denoting a transition from state i to state j.

 automaton: inputs i0,i1; outputs o0,o1; init 0; transitions (0,i0,o0,0); (0,i0,o1,1); (0,i1,o0,2); (0,i1,o1,2); (1,i0,o0,0); (1,i0,o1,1); (1,i1,o0,1); (1,i1,o1,1); (2,i0,o0,2); (2,i0,o1,2); (2,i1,o0,2); (2,i1,o1,2); accept 0,1; acceptance Safety Liveness Co-Büchi Büchi

## Boolean Unification

The tool below can be used to find a most general unifier for two boolean functions that is computed by boolean unification. This means, it computes, if possible, a substitution of the variables by boolean functions such that the two given boolean functions become the same.

 formula 1: a & c formula 2: a | b & c