In [ ]:
import spot
spot.setup()

Work in progress for a representation of EL-automata (a.k.a. twa in Spot) using MTBDDs.

In [2]:
a = spot.translate("(G(Fa U b) <-> FGc)", "generic", "deterministic")
a
Out[2]:
((Inf( ⓿ )&Inf( ❶ )) & Fin( ❷ )) | ((Fin( ⓿ )|Fin( ❶ )) & Inf( ❷ )) 0 0 I->0 0->0 a & !b & c ⓿ 0->0 b & c ⓿ ❶ 0->0 a & !b & !c ⓿ ❷ 0->0 b & !c ⓿ ❶ ❷ 1 1 0->1 !a & !b & c 0->1 !a & !b & !c ❷ 1->0 a & !b & c ⓿ 1->0 a & b & c ⓿ ❶ 1->0 a & !b & !c ⓿ ❷ 1->0 a & b & !c ⓿ ❶ ❷ 1->1 !a & !b & c 1->1 !a & b & c ❶ 1->1 !a & !b & !c ❷ 1->1 !a & b & !c ❶ ❷
In [3]:
m = spot.dtwa_to_mtdtwa(a)
m
Out[3]:
mtdtwa ((Inf( ⓿ )&Inf( ❶ )) & Fin( ❷ )) | ((Fin( ⓿ )|Fin( ❶ )) & Inf( ❷ )) S0 0 I->S0 B304 c S0->B304 S1 1 B331 c S1->B331 B330 a B331->B330 B321 a B331->B321 B303 a B304->B303 B296 a B304->B296 B288 b B330->B288 B329 b B330->B329 B303->B288 B302 b B303->B302 B277 b B296->B277 B295 b B296->B295 B321->B277 B320 b B321->B320 B280 0 ⓿ ❷ B288->B280 B285 0 ⓿ ❶ ❷ B288->B285 B270 0 ⓿ B277->B270 B274 0 ⓿ ❶ B277->B274 B316 1 ❶ B320->B316 B291 1 B320->B291 B298 1 ❷ B329->B298 B325 1 ❶ ❷ B329->B325 B295->B274 B295->B291 B302->B298 B302->B285

Each terminal stores a integerer that allows to retrive the data presented in the leaves above: a set of colors, and a destination state.

In [4]:
for i, d in enumerate(m.terminal_data):
    print(f"terminal_data[{i}] = {d}")

terminal_data[0] = (spot.mark_t([0]), 0)
terminal_data[1] = (spot.mark_t([0, 1]), 0)
terminal_data[2] = (spot.mark_t([0, 2]), 0)
terminal_data[3] = (spot.mark_t([0, 1, 2]), 0)
terminal_data[4] = (spot.mark_t([]), 1)
terminal_data[5] = (spot.mark_t([2]), 1)
terminal_data[6] = (spot.mark_t([1]), 1)
terminal_data[7] = (spot.mark_t([1, 2]), 1)