In [1]:
import spot
from spot.jupyter import display_inline
spot.setup(show_default='.bav')

Support for alternating automata

The following automata are what we will use as examples.

In [2]:
aut1, aut2, aut3, aut4, aut5 = spot.automata('''
HOA: v1 tool: "ltl3ba" "1.1.3" name: "VWAA for FGa && GFb" States: 6
Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 2 "a" "b" properties:
trans-labels explicit-labels state-acc univ-branch very-weak --BODY--
State: 0 "(FG(a) && GF(b))" [t] 3&1 State: 1 "GF(b)" [(1)] 1 [(!1)]
2&1 State: 2 "F(b)" {0} [(1)] 5 [(!1)] 2 State: 3 "FG(a)" {0} [(0)] 4
[t] 3 State: 4 "G(a)" [(0)] 4 State: 5 "t" [t] 5 --END--
/* Example from ADL's PSL2TGBA talk. */
HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:
3 "a" "b" "p" --BODY-- State: 0 "(a;a*;b)*" {0} [0] 1 [!0] 2 State: 1
"a*;b;(a;a*;b)*" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:
2 [t] 2 --END--
HOA: v1 States: 5 Start: 3 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:
3 "a" "b" "p" --BODY-- State: 0 "(a;a*;b)*" {0} [0] 1 [!0] 2 State: 1
"a*;b;(a;a*;b)*" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:
2 [t] 2 State: 3 [0] 4&0 State: 4 [t] 3 --END--
HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:
3 "a" "b" "p" --BODY-- State: 0 "(a;a*;b)*" {0} [0] 1 [!0] 2 State: 1
"a*;b;(a;a*;b)*" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:
2 [t] 2 --END--
HOA: v1 tool: "ltl3dra" "0.2.2" name: "VWAA for GFa" States: 3 Start: 0
acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 1 "a" properties: trans-labels
explicit-labels state-acc univ-branch very-weak --BODY-- State: 0 "GF(a)"
[t] 1&0 State: 1 "F(a)" {0} [(0)] 2 [t] 1 State: 2 "t" [t] 2 --END--
''')

Various display options

Here is the default output, using the bav options as set by default in the first cell.

In [3]:
display_inline(aut1, aut2, aut3, aut4, aut5)
VWAA for FGa && GFb Fin( ⓿ ) [co-Büchi] 0 (FG(a) && GF(b)) I->0 -1 0->-1 1 1 GF(b) -1->1 3 FG(a) ⓿ -1->3 1->1 b -4 1->-4 !b 3->3 1 4 G(a) 3->4 a -4->1 2 F(b) ⓿ -4->2 2->2 !b 5 t 2->5 b 5->5 1 4->4 a
Fin( ⓿ ) [co-Büchi] 0 (a;a*;b)* ⓿ I->0 1 a*;b;(a;a*;b)* ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1
Fin( ⓿ ) [co-Büchi] 3 3 I->3 -4 3->-4 a 0 (a;a*;b)* ⓿ 1 a*;b;(a;a*;b)* ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
Fin( ⓿ ) [co-Büchi] 0 (a;a*;b)* ⓿ I->0 1 a*;b;(a;a*;b)* ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1
VWAA for GFa Fin( ⓿ ) [co-Büchi] 0 GF(a) I->0 -1 0->-1 1 -1->0 1 F(a) ⓿ -1->1 1->1 1 2 t 1->2 a 2->2 1

If the state labels take too much space, you can reduce the size of the automaton by forcing states to be numbered with option 1. The original label is still displayed as a tooltip when the mouse is over the state.

Note that passing option show=... to display_inline is similar to calling aut.show(...) on each argument.

In [4]:
display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1')
VWAA for FGa && GFb Fin( ⓿ ) [co-Büchi] 0 0 I->0 -1 0->-1 1 1 1 -1->1 3 3 ⓿ -1->3 1->1 b -4 1->-4 !b 3->3 1 4 4 3->4 a -4->1 2 2 ⓿ -4->2 2->2 !b 5 5 2->5 b 5->5 1 4->4 a
Fin( ⓿ ) [co-Büchi] 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1
Fin( ⓿ ) [co-Büchi] 3 3 I->3 -4 3->-4 a 0 0 ⓿ 1 1 ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
Fin( ⓿ ) [co-Büchi] 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 2 2 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b -1 1->-1 a & b & p 2->2 1 -1->0 -1->1
VWAA for GFa Fin( ⓿ ) [co-Büchi] 0 0 I->0 -1 0->-1 1 -1->0 1 1 ⓿ -1->1 1->1 1 2 2 1->2 a 2->2 1

When working with alternating automata, it is quite common to hide "true states", and display "exiting transitions instead". You can do that with option u.

In [5]:
display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1u')
VWAA for FGa && GFb Fin( ⓿ ) [co-Büchi] 0 0 I->0 -1 0->-1 1 1 1 -1->1 3 3 ⓿ -1->3 1->1 b -4 1->-4 !b 3->3 1 4 4 3->4 a -4->1 2 2 ⓿ -4->2 2->2 !b 2->T5T2 b 4->4 a
Fin( ⓿ ) [co-Büchi] 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1
Fin( ⓿ ) [co-Büchi] 3 3 I->3 -4 3->-4 a 0 0 ⓿ 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
Fin( ⓿ ) [co-Büchi] 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1
VWAA for GFa Fin( ⓿ ) [co-Büchi] 0 0 I->0 -1 0->-1 1 -1->0 1 1 ⓿ -1->1 1->1 1 1->T2T1 a

Let's make sure that option u and s (to display SCCs) work well together:

In [6]:
display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1us')
VWAA for FGa && GFb Fin( ⓿ ) [co-Büchi] cluster_1 cluster_2 cluster_3 cluster_4 cluster_5 0 0 I->0 -1 0->-1 1 2 2 ⓿ 2->2 !b 2->T5T2 b 1 1 1->1 b -4 1->-4 !b -4->2 -4->1 4 4 4->4 a 3 3 ⓿ 3->4 a 3->3 1 -1->1 -1->3
Fin( ⓿ ) [co-Büchi] cluster_1 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1
Fin( ⓿ ) [co-Büchi] cluster_1 cluster_2 3 3 I->3 -4 3->-4 a 0 0 ⓿ 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1 -4->0 4 4 -4->4 4->3 1
Fin( ⓿ ) [co-Büchi] cluster_1 0 0 ⓿ I->0 1 1 ⓿ 0->1 a 0->T2T0 !a 1->0 !a & b & p 1->1 !b & p -1 1->-1 a & b & p 1->T2T1 !a & !b -1->0 -1->1
VWAA for GFa Fin( ⓿ ) [co-Büchi] cluster_1 cluster_2 0 0 I->0 -1 0->-1 1 1 1 ⓿ 1->1 1 1->T2T1 a -1->0 -1->1

Alternation removal

The remove_alternation() function works on any alternating automaton that is weak (not necessarily very weak), i.e., in each SCC all transition should belong to the same accepting sets.

The second argument of remove_alternation(), set to True below, simply asks for states to be labeled to help debugging. As the function builds Transition-based Generalized Büchi acceptance, it can be worthwhile to apply scc_filter() in an attempt to reduce the number of acceptance sets.

The next cell shows this two-step process on our first example automaton.

In [7]:
nba1t = spot.remove_alternation(aut1, True)
nba1 = spot.scc_filter(nba1t, True)
display_inline(aut1.show('.bav1u'), nba1t, nba1)
VWAA for FGa && GFb Fin( ⓿ ) [co-Büchi] 0 0 I->0 -1 0->-1 1 1 1 -1->1 3 3 ⓿ -1->3 1->1 b -4 1->-4 !b 3->3 1 4 4 3->4 a -4->1 2 2 ⓿ -4->2 2->2 !b 2->T5T2 b 4->4 a
Inf( ⓿ )&Inf( ❶ ) [gen. Büchi 2] 0 0 I->0 1 1,3 0->1 1 ⓿ 1->1 b ⓿ 2 1,2,3 1->2 !b 3 1,2,4 1->3 a & !b ❶ 4 1,4 1->4 a & b ⓿ ❶ 2->1 b ⓿ 2->2 !b 2->3 a & !b ❶ 2->4 a & b ⓿ ❶ 3->3 a & !b ❶ 3->4 a & b ⓿ ❶ 4->3 a & !b ❶ 4->4 a & b ⓿ ❶
Inf( ⓿ ) [Büchi] 0 0 I->0 1 1,3 0->1 1 1->1 b 2 1,2,3 1->2 !b 3 1,2,4 1->3 a & !b 4 1,4 1->4 a & b 2->1 b 2->2 !b 2->3 a & !b 2->4 a & b 3->3 a & !b 3->4 a & b ⓿ 4->3 a & !b 4->4 a & b ⓿

Let's apply this process to the other 4 automata (which are not very-weak, unlike aut1). The states marked with ~ are part of a break-point construction.

In [8]:
nba2, nba3, nba4, nba5 = [spot.scc_filter(spot.remove_alternation(a, True), True) for a in (aut2, aut3, aut4, aut5)]
display_inline(nba2, nba3, nba4, nba5)
Inf( ⓿ ) [Büchi] 0 ~0 I->0 1 {} 0->1 !a 2 ~1 0->2 a 1->1 1 ⓿ 2->0 !a & b & p 2->1 !a & !b 2->2 !b & p 3 ~1,~0 2->3 a & b & p 3->0 !a & b & p 3->1 !a & !b 3->2 a & !b & p 3->3 a & b & p
Inf( ⓿ ) [Büchi] 0 3 I->0 1 ~0,4 0->1 a ⓿ 1->0 !a ⓿ 2 3,~1 1->2 a 3 0,4,~1 2->3 a & !b & p 4 4,~1,~0 2->4 a & b & p 3->0 !a & !b ⓿ 3->2 a & !b & p 5 3,~0 3->5 !a & b & p 6 3,~1,~0 3->6 a & b & p 4->0 !a & !b ⓿ 4->2 a & !b & p 4->5 !a & b & p 4->6 a & b & p 5->3 a 6->3 a & !b & p 6->4 a & b & p
Inf( ⓿ ) [Büchi] 0 ~0 I->0 1 {} 0->1 !a 2 ~1 0->2 a 1->1 1 ⓿ 2->0 !a & b & p 2->1 !a & !b 2->2 !b & p 3 ~1,~0 2->3 a & b & p 3->0 !a & b & p 3->1 !a & !b 3->2 a & !b & p 3->3 a & b & p
Inf( ⓿ ) [Büchi] 0 0 I->0 1 0,1 0->1 1 1->1 !a 1->1 a ⓿

The following demonstrates that very weak (non-alternating) Büchi automata can be complemented via alternation removal.

In [9]:
pos = spot.automaton("""HOA: v1 name: "(a & (Fa R XFb)) | (!a & (G!a U
XG!b))" States: 6 Start: 0 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1
Inf(0) properties: trans-labels explicit-labels state-acc
semi-deterministic --BODY-- State: 0 [0] 1 [!0] 2 [!0] 3 State: 1 [!1]
1 [1] 4 State: 2 {0} [!1] 2 State: 3 [!0] 3 [!0] 5 State: 4 {0} [t] 4
State: 5 {0} [!0&!1] 5 --END--""")
altneg = spot.dualize(pos)
neg = spot.remove_alternation(altneg)
display_inline(pos, altneg.show('.bvu'), neg)
(a & (Fa R XFb)) | (!a & (G!a U\nXG!b)) Inf( ⓿ ) [Büchi] 0 0 I->0 1 1 0->1 a 2 2 ⓿ 0->2 !a 3 3 0->3 !a 1->1 !b 4 4 ⓿ 1->4 b 2->2 !b 3->3 !a 5 5 ⓿ 3->5 !a 4->4 1 5->5 !a & !b
Fin( ⓿ ) [co-Büchi] 0 0 I->0 1 1 0->1 a -1 0->-1 !a 1->1 !b 2 2 ⓿ -1->2 3 3 -1->3 2->2 !b 2->T5T2 b 3->T5T3 a -4 3->-4 !a -4->3 4 4 ⓿ -4->4 4->4 !a & !b 4->T5T4 a | b
Inf( ⓿ )&Inf( ❶ ) [gen. Büchi 2] 0 0 I->0 1 1 0->1 !a ❶ 2 2 0->2 a ⓿ ❶ 3 3 1->3 !a & !b 4 4 1->4 !a & b ⓿ 5 5 1->5 a & !b ❶ 6 6 1->6 a & b ⓿ ❶ 2->2 !b ⓿ ❶ 3->3 !a & !b 3->4 !a & b ⓿ ❶ 3->5 a & !b ❶ 3->6 a & b ⓿ ❶ 4->4 !a & !b ⓿ 4->4 !a & b ⓿ ❶ 4->6 a ⓿ ❶ 5->5 !b ❶ 5->6 b ⓿ ❶ 6->6 1 ⓿ ❶
In [10]:
# Issue #382.
w = spot.parse_word('cycle{!a&b}').as_automaton()
assert pos.intersects(w) != neg.intersects(w)