In [1]:
import spot
spot.setup()
from spot.jupyter import display_inline

This notebook presents functions that can be used to solve the Reactive Synthesis problem using games. If you are not familiar with how Spot represent games, please read the games notebook first.

In Reactive Synthesis, the goal is to build an electronic circuit that reacts to some input signals by producing some output signals, under some LTL constraints that tie both input and output. Of course the input signals are not controlable, so only job is to decide what output signal to produce.

Reactive synthesis in four steps

A strategy/control circuit can be derived more conveniently from an LTL/PSL specification. The process is decomposed in three steps:

  • Creating the game
  • Solving the game
  • Simplifying the winnning strategy
  • Building the circuit from the strategy

Each of these steps is parametrized by a structure called synthesis_info. This structure stores some additional data needed to pass fine-tuning options or to store statistics.

The ltl_to_game function takes the LTL specification, and the list of controlable atomic propositions (or output signals). It returns a two-player game, where player 0 plays the input variables (and wants to invalidate the acceptance condition), and player 1 plays the output variables (and wants to satisfy the output condition). The conversion from LTL to parity automata can use one of many algorithms, and can be specified in the synthesis_info structure (this works like the --algo= option of ltlsynt).

In [2]:
si = spot.synthesis_info()
si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm

game = spot.ltl_to_game("G((F(i0) && F(i1))->(G(i1<->(X(o0)))))", ["o0"], si)
print("game has", game.num_states(), "states and", game.num_edges(), "edges")
print("output propositions are:", ", ".join(spot.get_synthesis_output_aps(game)))
display(game)
game has 29 states and 55 edges
output propositions are: o0
Inf( ) | (Fin( ) & (Inf( ) | Fin( ))) [parity max odd 4] 9 9 I->9 25 25 9->25 !i0 & !i1 26 26 9->26 i0 & !i1 27 27 9->27 !i0 & i1 28 28 9->28 i0 & i1 0 0 10 10 0->10 !i1 11 11 0->11 i1 1 1 10->1 o0 11->0 o0 12 12 1->12 !i1 13 13 1->13 i1 12->1 !o0 13->0 !o0 2 2 14 14 2->14 i1 16 16 2->16 !i1 15 15 14->15 1 16->2 1 3 3 3->13 i1 17 17 3->17 !i1 17->2 o0 17->3 !o0 4 4 4->14 i0 18 18 4->18 !i0 18->4 1 5 5 5->14 i0 & i1 5->16 i0 & !i1 5->18 !i0 & i1 19 19 5->19 !i0 & !i1 19->5 1 6 6 6->10 i0 & !i1 6->11 i0 & i1 20 20 6->20 !i0 & !i1 21 21 6->21 !i0 & i1 20->4 !o0 7 7 20->7 o0 21->4 !o0 21->6 o0 7->12 i0 & !i1 7->13 i0 & i1 22 22 7->22 !i0 & !i1 23 23 7->23 !i0 & i1 22->4 o0 22->7 !o0 23->4 o0 23->6 !o0 8 8 8->13 i0 & i1 8->17 i0 & !i1 8->23 !i0 & i1 24 24 8->24 !i0 & !i1 24->5 o0 24->8 !o0 25->8 1 26->3 1 27->6 1 28->0 1 15->14 1

Solving the game, is done with solve_game() as with any game. There is also a version that takes a synthesis_info as second argument in case the time it takes has to be recorded. Here passing si or not makes no difference.

In [3]:
print("Found a solution:", spot.solve_game(game, si))
spot.highlight_strategy(game)
game.show('.g')
Found a solution: True
Out[3]:
Inf( ) | (Fin( ) & (Inf( ) | Fin( ))) [parity max odd 4] 9 9 I->9 25 25 9->25 26 26 9->26 27 27 9->27 28 28 9->28 0 0 10 10 0->10 11 11 0->11 1 1 10->1 11->0 12 12 1->12 13 13 1->13 12->1 13->0 2 2 14 14 2->14 16 16 2->16 15 15 14->15 16->2 3 3 3->13 17 17 3->17 17->2 17->3 4 4 4->14 18 18 4->18 18->4 5 5 5->14 5->16 5->18 19 19 5->19 19->5 6 6 6->10 6->11 20 20 6->20 21 21 6->21 20->4 7 7 20->7 21->4 21->6 7->12 7->13 22 22 7->22 23 23 7->23 22->4 22->7 23->4 23->6 8 8 8->13 8->17 8->23 24 24 8->24 24->5 24->8 25->8 26->3 27->6 28->0 15->14

Once a strategy has been found, it can be extracted as an automaton and simplified using 6 different levels (the default is 2). The output should be interpreted as a mealy automaton, where transition have the form (ins)&(outs) where ins and outs are Boolean formulas representing possible possibles inputs and outputs (they could be more than just conjunctions of atomic proposition). Mealy machines with this type of labels are called "separated" in Spot.

In [4]:
# We have different levels of simplification:
# 0 : No simplification
# 1 : bisimulation-based reduction
# 2 : bisimulation-based reduction with output output assignement
# 3 : SAT-based exact minimization
# 4 : First 1 then 3 (exact)
# 5 : First 2 then 3 (not exact)

descr = ["0 : No simplification", 
         "1 : bisimulation-based reduction", 
         "2 : bisimulation-based reduction with output output assignement",
         "3 : SAT-based exact minimization",
         "4 : First 1 then 3 (exact)",
         "5 : First 2 then 3 (not exact)"]


for i in range(6):
    print("simplification lvl ", descr[i])
    si.minimize_lvl = i
    mealy = spot.solved_game_to_separated_mealy(game, si)
    display(mealy.show())
simplification lvl  0 : No simplification
0 0 I->0 1 1 0->1 !i0 & !i1 / 1 2 2 0->2 i0 & !i1 / 1 3 3 0->3 !i0 & i1 / 1 4 4 0->4 i0 & i1 / 1 1->1 !i0 & !i1 / !o0 1->2 i0 & !i1 / !o0 1->3 !i0 & i1 / !o0 1->4 i0 & i1 / !o0 2->2 !i1 / !o0 2->4 i1 / !o0 3->3 !i0 & i1 / o0 3->4 i0 & i1 / o0 5 5 3->5 i0 & !i1 / o0 6 6 3->6 !i0 & !i1 / o0 4->4 i1 / o0 4->5 !i1 / o0 5->4 i1 / !o0 5->5 !i1 / !o0 6->3 !i0 & i1 / !o0 6->4 i0 & i1 / !o0 6->5 i0 & !i1 / !o0 6->6 !i0 & !i1 / !o0
simplification lvl  1 : bisimulation-based reduction
0 0 I->0 1 1 0->1 !i0 & !i1 / 1 0->1 i0 & !i1 / 1 2 2 0->2 !i0 & i1 / 1 0->2 i0 & i1 / 1 1->1 i0 & !i1 / !o0 1->1 !i0 & !i1 / !o0 1->2 i0 & i1 / !o0 1->2 !i0 & i1 / !o0 2->1 i0 & !i1 / o0 2->1 !i0 & !i1 / o0 2->2 i0 & i1 / o0 2->2 !i0 & i1 / o0
simplification lvl  2 : bisimulation-based reduction with output output assignement
1 1 I->1 1->1 i0 & i1 / o0 1->1 !i0 & i1 / o0 0 0 1->0 i0 & !i1 / o0 1->0 !i0 & !i1 / o0 0->1 i0 & i1 / !o0 0->1 !i0 & i1 / !o0 0->0 i0 & !i1 / !o0 0->0 !i0 & !i1 / !o0
simplification lvl  3 : SAT-based exact minimization
0 0 I->0 0->0 i1 / o0 1 1 0->1 !i1 / o0 1->0 i1 / !o0 1->1 !i1 / !o0
simplification lvl  4 : First 1 then 3 (exact)
0 0 I->0 0->0 !i1 / !o0 1 1 0->1 i1 / !o0 1->0 !i1 / o0 1->1 i1 / o0
simplification lvl  5 : First 2 then 3 (not exact)
0 0 I->0 0->0 i0 & i1 / o0 0->0 !i0 & i1 / o0 1 1 0->1 i0 & !i1 / o0 0->1 !i0 & !i1 / o0 1->0 i0 & i1 / !o0 1->0 !i0 & i1 / !o0 1->1 i0 & !i1 / !o0 1->1 !i0 & !i1 / !o0

If needed, a separated Mealy machine can be turned into game shape using split_sepearated_mealy(), which is more efficient than split_2step().

In [5]:
display_inline(mealy, spot.split_separated_mealy(mealy), per_row=2)
0 0 I->0 0->0 i0 & i1 / o0 0->0 !i0 & i1 / o0 1 1 0->1 i0 & !i1 / o0 0->1 !i0 & !i1 / o0 1->0 i0 & i1 / !o0 1->0 !i0 & i1 / !o0 1->1 i0 & !i1 / !o0 1->1 !i0 & !i1 / !o0
t [all] 0 0 I->0 2 2 0->2 i0 & !i1 0->2 !i0 & !i1 3 3 0->3 i0 & i1 0->3 !i0 & i1 1 1 2->1 o0 3->0 o0 4 4 1->4 i0 & i1 1->4 !i0 & i1 5 5 1->5 i0 & !i1 1->5 !i0 & !i1 4->0 !o0 5->1 !o0

Converting the separated mealy machine to AIGER

A separated mealy machine can be converted to a circuit in the AIGER format using mealy_machine_to_aig(). This takes a second argument specifying what type of encoding to use (exactly like ltlsynt's --aiger=... option).

In this case, the circuit is quite simple: o0 should be the negation of previous value of i1. This is done by storing the value of i1 in a latch. And the value if i0 can be ignored.

In [6]:
aig = spot.mealy_machine_to_aig(mealy, "isop")
display(aig)
6 L0_out o0 o0 6->o0:s L0 L0_in 2 i1 2->L0 4 i0

While we are at it, let us mention that you can render those circuits horizontally as follows:

In [7]:
aig.show('h')
Out[7]:
6 L0_out o0 o0 6->o0:w L0 L0_in 2 i1 2->L0 4 i0

To encode the circuit in the aig format (ASCII version) use:

In [8]:
print(aig.to_str())
aag 3 2 1 1 0
2
4
6 3
7
i0 i1
i1 i0
o0 o0

Adding more inputs and outputs by force

It can happen that propositions declared as output are ommited in the aig circuit (either because they are not part of the specification, or because they do not appear in the winning strategy). In that case those values can take arbitrary values.

For instance so following constraint mention o1 and i1, but those atomic proposition are actually unconstrained (F(... U x) can be simplified to Fx). Without any indication, the circuit built will ignore those variables:

In [9]:
game = spot.ltl_to_game("i0 <-> F((Go1 -> Fi1) U o0)", ["o0", "o1"])
spot.solve_game(game)
spot.highlight_strategy(game)
display(game)
mealy = spot.solved_game_to_separated_mealy(game)
display(mealy)
aig = spot.mealy_machine_to_aig(mealy, "isop")
display(aig)
Inf( ) | (Fin( ) & (Inf( ) | (Fin( ) & (Inf( ) | Fin( ))))) [parity max odd 6] 3 3 I->3 6 6 3->6 i0 7 7 3->7 !i0 0 0 4 4 0->4 1 4->0 1 1 1 5 5 1->5 1 5->1 !o0 2 2 2->6 1 6->0 o0 6->2 !o0 7->1 !o0
0 0 I->0 0->0 i0 / o0 1 1 0->1 !i0 / !o0 1->1 1 / !o0
4 L0_out 6 6 4->6 L0 L0_in 6->L0 o0 o0 6->o0:s 2 i0 2->6

To force the presence of extra variables in the circuit, they can be passed to mealy_machine_to_aig().

In [10]:
display(spot.mealy_machine_to_aig(mealy, "isop", ["i0", "i1"], ["o0", "o1"]))
6 L0_out 8 8 6->8 L0 L0_in 8->L0 o0 o0 8->o0:s o1 o1 2 i0 2->8 4 i1 0 False 0->o1:s

Combining mealy machines

It can happen that the complet specification of the controller can be separated into sub-specifications with DISJOINT output propositions, see Finkbeiner et al. Specification Decomposition for Reactive Synthesis. This results in multiple mealy machines which have to be converted into one single aiger circuit.

This can be done using the function mealy_machines_to_aig(), which takes a vector of separated mealy machines as argument. In order for this to work, all mealy machines need to share the same bdd_dict. This can be ensured by passing a common options strucuture.

In [17]:
g1 = spot.ltl_to_game("G((i0 xor i1) <-> o0)", ["o0"], si)
g2 = spot.ltl_to_game("G((i0 xor i1) <-> (!o1))", ["o1"], si)
spot.solve_game(g1)
spot.highlight_strategy(g1)
spot.solve_game(g2)
spot.highlight_strategy(g2)
print("Solved games:")
display_inline(g1, g2)
strat1 = spot.solved_game_to_separated_mealy(g1)
strat2 = spot.solved_game_to_separated_mealy(g2)
print("Reduced strategies:")
display_inline(strat1, strat2)
print("Circuit implementing both machines:")
aig = spot.mealy_machines_to_aig([strat1, strat2], "isop")
display(aig)
Solved games:
Inf( ) | (Fin( ) & (Inf( ) | Fin( ))) [parity max odd 4] 0 0 I->0 1 1 0->1 (!i0 & !i1) | (i0 & i1) 2 2 0->2 (!i0 & i1) | (i0 & !i1) 1->0 !o0 2->0 o0
Inf( ) | (Fin( ) & (Inf( ) | Fin( ))) [parity max odd 4] 0 0 I->0 1 1 0->1 (!i0 & !i1) | (i0 & i1) 2 2 0->2 (!i0 & i1) | (i0 & !i1) 1->0 o1 2->0 !o1
Reduced strategies:
0 0 I->0 0->0 (!i0 & !i1) | (i0 & i1) / !o0 0->0 (!i0 & i1) | (i0 & !i1) / o0
0 0 I->0 0->0 (!i0 & !i1) | (i0 & i1) / o1 0->0 (!i0 & i1) | (i0 & !i1) / !o1
Circuit implementing both machines:
6 6 10 10 6->10 8 8 8->10 o0 o0 10->o0:s o1 o1 10->o1:s 2 i0 2->6 2->8 4 i1 4->6 4->8

Reading an AIGER-file

Note that we do not support the full AIGER syntax. Our restrictions corresponds to the conventions used in the type of AIGER file we output:

  • Input variables start at index 2 and are consecutively numbered.
  • Latch variables start at index (1 + #inputs)×2 and are consecutively numbered.
  • If some inputs or outputs are named in comments, all of them have to be named.
  • Gate number $n$ can only connect to latches, inputs, or previously defined gates ($<n$).
In [12]:
aag_txt = """aag 5 2 0 2 3
2
4
10
6
6 2 4
8 3 5
10 7 9
i0 a
i1 b
o0 c
o1 d"""
In [13]:
this_aig = spot.aiger_circuit(aag_txt)
display(this_aig)
6 6 10 10 6->10 o1 d 6->o1:s 8 8 8->10 o0 c 10->o0:s 2 a 2->6 2->8 4 b 4->6 4->8
In [14]:
print(this_aig.to_str())
aag 5 2 0 2 3
2
4
10
6
6 2 4
8 3 5
10 7 9
i0 a
i1 b
o0 c
o1 d
In [15]:
print(this_aig.gates())
((2, 4), (3, 5), (7, 9))

An aiger circuit can be transformed into a monitor/mealy machine. This can be used for instance to check that it does not intersect the negation of the specification.

In [16]:
this_aig.as_automaton()
Out[16]:
0 0 I->0 0->0 !a & !b / !c & !d a & b / !c & d (!a & b) | (a & !b) / c & !d