This notebook reproduces the examples shown in our CAV'22 paper, as well as a few more. It was part of the CAV'22 artifact, but has been updated to keep up with recent version of Spot.

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

Figure 1¶

Fig. 1 of the paper shows (1) how to convert an LTL formula to an automaton with arbitrary acceptance condition, and (2) how to display the internal representation of the automaton.

In [2]:
aut = spot.translate('GF(a <-> Xa) & FGb', 'det', 'gen')
aut
Out[2]:
b'\n\n\nFin(\n\xe2\x93\xbf\n) & Inf(\n\xe2\x9d\xb6\n)\n[Rabin 1]\n\n\n\n0\n\n0\n\n\n\nI->0\n\n\n\n\n\n0->0\n\n\na & !b\n\xe2\x93\xbf\n\n\n\n0->0\n\n\na & b\n\xe2\x9d\xb6\n\n\n\n1\n\n1\n\n\n\n0->1\n\n\n!a & b\n\n\n\n0->1\n\n\n!a & !b\n\xe2\x93\xbf\n\n\n\n1->0\n\n\na & b\n\n\n\n1->0\n\n\na & !b\n\xe2\x93\xbf\n\n\n\n1->1\n\n\n!a & !b\n\xe2\x93\xbf\n\n\n\n1->1\n\n\n!a & b\n\xe2\x9d\xb6\n\n\n\n'
In [3]:
aut.show_storage()
Out[3]:
b'\n\ng\n\n\n\nstates\n\n\nstates\n\n\n0\n\n\n1\n\nsucc\n\n\n1\n\n\n5\n\nsucc_tail\n\n\n4\n\n\n8\n\n\n\nedges\n\n\nedges\n\n\n1\n\n\n2\n\n\n3\n\n\n4\n\n\n5\n\n\n6\n\n\n7\n\n\n8\n\ncond\n\na & !b\n\na & b\n\n!a & b\n\n!a & !b\n\na & b\n\na & !b\n\n!a & !b\n\n!a & b\n\nacc\n\n{0}\n\n{1}\n\n{}\n\n{0}\n\n{}\n\n{0}\n\n{0}\n\n{1}\n\ndst\n\n\n0\n\n\n0\n\n\n1\n\n\n1\n\n\n0\n\n\n0\n\n\n1\n\n\n1\n\nnext_succ\n\n\n2\n\n\n3\n\n\n4\n\n0\n\n\n6\n\n\n7\n\n\n8\n\n0\n\nsrc\n\n\n0\n\n\n0\n\n\n0\n\n\n0\n\n\n1\n\n\n1\n\n\n1\n\n\n1\n\n\n\nmeta\ninit_state:\n\n0\nnum_sets:\n2\nacceptance:\nFin(0) & Inf(1)\nap_vars:\nb a\n\n\n\n\nprops\nprop_state_acc:\nmaybe\nprop_inherently_weak:\nmaybe\nprop_terminal:\nno\nprop_weak:\nmaybe\nprop_very_weak:\nmaybe\nprop_complete:\nmaybe\nprop_universal:\nyes\nprop_unambiguous:\nyes\nprop_semi_deterministic:\nyes\nprop_stutter_invariant:\nmaybe\n\n\n\n\n'

Figure 2¶

Fig.2 shows an example of alternating automaton, represented in two different ways, along with its internal representation.

In [4]:
# We enter the automaton using the HOA format.
aut2 = spot.automaton("""
HOA: v1
States: 5
Start: 3
acc-name: co-Buchi
Acceptance: 1 Fin(0)
AP: 2 "a" "b"
--BODY--
State: 0 {0} 
[0] 1
[!0] 2
State: 1 {0} 
[0&1] 0&1
State: 2 
[t] 2 
State: 3 
[0] 4&0
State: 4 
[t] 3 
--END--
""")
In [5]:
display_inline(aut2, aut2.show('.u'), per_row=2)
[co-Büchi] 3 3 I->3 -4 3->-4 a 0 0 1 1 0->1 a 2 2 0->2 !a -1 1->-1 a & b 2->2 1 -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
[co-Büchi] 3 3 I->3 -4 3->-4 a 0 0 1 1 0->1 a 0->T2T0 !a -1 1->-1 a & b -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
In [6]:
aut2.show_storage()
Out[6]:
b'\n\ng\n\n\n\nstates\n\n\nstates\n\n\n0\n\n\n1\n\n\n2\n\n\n3\n\n\n4\n\nsucc\n\n\n1\n\n\n3\n\n\n4\n\n\n5\n\n\n6\n\nsucc_tail\n\n\n2\n\n\n3\n\n\n4\n\n\n5\n\n\n6\n\n\n\nedges\n\n\nedges\n\n\n1\n\n\n2\n\n\n3\n\n\n4\n\n\n5\n\n\n6\n\ncond\n\na\n\n!a\n\na & b\n\n1\n\na\n\n1\n\nacc\n\n{0}\n\n{0}\n\n{0}\n\n{}\n\n{}\n\n{}\n\ndst\n\n\n1\n\n\n2\n\n\n~0\n\n\n2\n\n\n~3\n\n\n3\n\nnext_succ\n\n\n2\n\n0\n\n0\n\n0\n\n0\n\n0\n\nsrc\n\n\n0\n\n\n0\n\n\n1\n\n\n2\n\n\n3\n\n\n4\n\n\n\ndests\n\n\ndests\n\n\n~0\n\n\n\n\n~3\n\n\n\n#cnt/dst\n\n#2\n\n\n0\n\n\n1\n\n#2\n\n\n0\n\n\n4\n\n\n\nmeta\ninit_state:\n\n3\nnum_sets:\n1\nacceptance:\nFin(0)\nap_vars:\nb a\n\n\n\n\nprops\nprop_state_acc:\nyes\nprop_inherently_weak:\nmaybe\nprop_terminal:\nmaybe\nprop_weak:\nmaybe\nprop_very_weak:\nmaybe\nprop_complete:\nno\nprop_universal:\nyes\nprop_unambiguous:\nyes\nprop_semi_deterministic:\nyes\nprop_stutter_invariant:\nmaybe\n\n\n\n\n'

Figure 3¶

Fig. 3 shows an example of game generated by ltlsynt from the LTL specification of a reactive controler, and then how this game can be encoded into an And-Inverter-Graph. First we retrieve the game generated by ltlsynt (any argument passed to spot.automaton is interpreted as a command if it ends with a pipe), then we solve it to compute a possible winning strategy.

Player 0 plays from round states and tries to violate the acceptance condition; Player 1 plays from diamond states and tries to satisfy the acceptance condition. Once a game has been solved, the highlight_strategy function will decorate the automaton with winning region and computed strategies for player 0 and 1 in red and green respectively. Therefore this game is winning for player 1 from the initial state.

Compared to the paper, the production of parity automata in ltlsynt has been improved, and it generates a Büchi game instead (but Büchi can be seen one case of parity).

In [7]:
game = spot.automaton("ltlsynt --outs=b -f 'F(a & Xa) <-> Fb' --print-game-hoa |")
spot.solve_game(game)
spot.highlight_strategy(game)
game
Out[7]:
b'\n\n\n[B\xc3\xbcchi]\n\n\n\n4\n\n\n4\n\n\n\nI->4\n\n\n\n\n\n7\n\n\n7\n\n\n\n4->7\n\n\n!a\n\n\n\n12\n\n\n12\n\n\n\n4->12\n\n\na\n\n\n\n0\n\n\n0\n\n\n\n6\n\n\n6\n\n\n\n0->6\n\n\n1\n\n\n\n6->0\n\n\n1\n\n\n\n1\n\n\n1\n\n\n\n1->7\n\n\n!a\n\n\n\n8\n\n\n8\n\n\n\n1->8\n\n\na\n\n\n\n7->4\n\n\n!b\n\n\n\n2\n\n2\n\n\n\n7->2\n\n\nb\n\n\n\n8->0\n\n\nb\n\n\n\n5\n\n5\n\n\n\n8->5\n\n\n!b\n\n\n\n9\n\n9\n\n\n\n2->9\n\n\n!a\n\n\n\n10\n\n10\n\n\n\n2->10\n\n\na\n\n\n\n9->2\n\n\n1\n\n\n\n3\n\n3\n\n\n\n10->3\n\n\n1\n\n\n\n3->9\n\n\n!a\n\n\n\n11\n\n11\n\n\n\n3->11\n\n\na\n\n\n\n11->0\n\n\n1\n\n\n\n12->1\n\n\n!b\n\n\n\n12->3\n\n\nb\n\n\n\n13\n\n13\n\n\n\n5->13\n\n\n1\n\n\n\n13->0\n\n\nb\n\n\n\n13->5\n\n\n!b\n\n\n\n'

The solved_game_to_mealy() shown in the paper does not always produce the same type of output, so it is better to explicitely call solved_game_to_split_mealy() or solved_game_to_separated_mealy() depending on the type of output one need. We also show how to use the reduce_mealy() method to simplify one.

In [8]:
mealy = spot.solved_game_to_separated_mealy(game)
mealy_min = spot.reduce_mealy(mealy, True)
aig = spot.mealy_machine_to_aig(mealy_min, "isop")
display_inline(mealy, mealy_min, aig)
0 0 I->0 0->0 !a / !b 1 1 0->1 a / !b 1->0 !a / !b 2 2 1->2 a / b 2->2 1 / 1
0 0 I->0 0->0 !a / !b 1 1 0->1 a / !b 1->0 !a / !b 1->1 a / b
4 L0_out 6 6 4->6 o0 b 6->o0:s L0 L0_in 2 a 2->6 2->L0