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()
```

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

In [3]:

```
aut.show_storage()
```

Out[3]:

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

In [6]:

```
aut2.show_storage()
```

Out[6]:

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

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