In [1]:
import spot
spot.setup()

Work in progress for a representation of ω-automata (a.k.a. twa in Spot) using MTBDDs. We initially implemented a transition-based variant, before realizing that using MTBDDs, the transition-based and state-based versions of an automaton have exactly the same structure, the state-based version is even slightly more memory efficient.

So even if the transition-based variant still exists, its state-based counterpart is more developed.

This notebook is about the transition-based variant. See mtdswa.ipynb for the state-based version.

Multi-Terminal-BDD-based Deterministic Transition-based ω-Automaton (MTDTwA)¶

In [2]:
a = spot.translate("GFa <-> c", "generic", "deterministic")
a
Out[2]:
(Inf( ⓿ )&Inf( ❶ )) | (Fin( ⓿ ) & Fin( ❶ )) 0 0 I->0 1 1 0->1 c 2 2 0->2 !c 1->1 !a ⓿ 1->1 a ⓿ ❶ 2->2 !a 2->2 a ❶
In [3]:
m = spot.dtwa_to_mtdtwa(a)
m
Out[3]:
mtdtwa (Inf( ⓿ )&Inf( ❶ )) | (Fin( ⓿ ) & Fin( ❶ )) S0 0 I->S0 B38 c S0->B38 S1 1 B56 a S1->B56 S2 2 B60 a S2->B60 B34 2 B38->B34 B37 1 B38->B37 B54 1 ⓿ ❶ B56->B54 B35 1 ⓿ B56->B35 B60->B34 B58 2 ❶ B60->B58

Each terminal stores an integer that allows to retrieve 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_map):
    print(f"terminal_data_map[{i}] = {d}")

terminal_data_map[0] = (spot.mark_t([]), 1)
terminal_data_map[1] = (spot.mark_t([]), 2)
terminal_data_map[2] = (spot.mark_t([0]), 1)
terminal_data_map[3] = (spot.mark_t([0, 1]), 1)
terminal_data_map[4] = (spot.mark_t([1]), 2)
In [5]:
m.as_twa()
Out[5]:
(Inf( ⓿ )&Inf( ❶ )) | (Fin( ⓿ ) & Fin( ❶ )) 0 0 I->0 1 1 0->1 c 2 2 0->2 !c 1->1 !a ⓿ 1->1 a ⓿ ❶ 2->2 !a 2->2 a ❶
In [6]:
m.as_twa(True)
Out[6]:
(Inf( ⓿ )&Inf( ❶ )) | (Fin( ⓿ ) & Fin( ❶ )) 5 5 I->5 0 0 5->0 c 1 1 5->1 !c 2 2 ⓿ 0->2 !a 3 3 ⓿ ❶ 0->3 a 2->2 !a 2->3 a 3->2 !a 3->3 a 1->1 !a 4 4 ❶ 1->4 a 4->1 !a 4->4 a