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]:
Fin( ⓿ ) & Inf( ❶ ) [Rabin 1] 0 0 I->0 0->0 a & !b ⓿ 0->0 a & b ❶ 1 1 0->1 !a & b 0->1 !a & !b ⓿ 1->0 a & b 1->0 a & !b ⓿ 1->1 !a & !b ⓿ 1->1 !a & b ❶
In [3]:
aut.show_storage()
Out[3]:
g states states 0 1 succ 1 5 succ_tail 4 8 edges edges 1 2 3 4 5 6 7 8 cond a & !b a & b !a & b !a & !b a & b a & !b !a & !b !a & b acc {0} {1} {} {0} {} {0} {0} {1} dst 0 0 1 1 0 0 1 1 next_succ 2 3 4 0 6 7 8 0 src 0 0 0 0 1 1 1 1 meta init_state: 0 num_sets: 2 acceptance: Fin(0) & Inf(1) ap_vars: b a props prop_state_acc: maybe prop_inherently_weak: maybe prop_terminal: no prop_weak: maybe prop_very_weak: maybe prop_complete: maybe prop_universal: yes prop_unambiguous: yes prop_semi_deterministic: yes prop_stutter_invariant: maybe

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]:
g states states 0 1 2 3 4 succ 1 3 4 5 6 succ_tail 2 3 4 5 6 edges edges 1 2 3 4 5 6 cond a !a a & b 1 a 1 acc {0} {0} {0} {} {} {} dst 1 2 ~0 2 ~3 3 next_succ 2 0 0 0 0 0 src 0 0 1 2 3 4 dests dests ~0 ~3 #cnt/dst #2 0 1 #2 0 4 meta init_state: 3 num_sets: 1 acceptance: Fin(0) ap_vars: b a props prop_state_acc: yes prop_inherently_weak: maybe prop_terminal: maybe prop_weak: maybe prop_very_weak: maybe prop_complete: no prop_universal: yes prop_unambiguous: yes prop_semi_deterministic: yes prop_stutter_invariant: maybe

Figure 3

Fig. 3 shows an example of game generated by ltlsynt from the LTL specification of a reactive controller, 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üchi] 4 4 I->4 7 7 4->7 !a 12 12 4->12 a 0 0 6 6 0->6 1 6->0 1 1 1 1->7 !a 8 8 1->8 a 7->4 !b 2 2 7->2 b 8->0 b 5 5 8->5 !b 9 9 2->9 !a 10 10 2->10 a 9->2 1 3 3 10->3 1 3->9 !a 11 11 3->11 a 11->0 1 12->1 !b 12->3 b 13 13 5->13 1 13->0 b 13->5 !b

The solved_game_to_mealy() shown in the paper does not always produce the same type of output, so it is better to explicitly 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