In [1]:
import spot
spot.setup(show_default='.ba')

These test cases for the remove_alternation() algorithm.


In [2]:
aut = spot.automaton('''
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--
'''); aut.show('.1ab')


Out[2]:
G Fin( ) 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

In [3]:
aut2 = spot.remove_alternation(aut, True); aut2


Out[3]:
G Inf( )&Inf( ) 0 0 I->0 1 1,3 0->1 1 1->1 b 2 1,4 1->2 a & b 3 1,2,3 1->3 !b 4 1,2,4 1->4 a & !b 2->2 a & b 2->4 a & !b 3->1 b 3->2 a & b 3->3 !b 3->4 a & !b 4->2 a & b 4->4 a & !b

In [4]:
spot.scc_filter(aut2, True)


Out[4]:
G Inf( ) 0 0 I->0 1 1,3 0->1 1 1->1 b 2 1,4 1->2 a & b 3 1,2,3 1->3 !b 4 1,2,4 1->4 a & !b 2->2 a & b 2->4 a & !b 3->1 b 3->2 a & b 3->3 !b 3->4 a & !b 4->2 a & b 4->4 a & !b

In [5]:
# Example from ADL's PSL2TGBA talk.
aut = spot.automaton('''
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--
'''); aut.show('.1ab')


Out[5]:
G Fin( ) 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

In [6]:
spot.remove_alternation(aut, True)


Out[6]:
G Inf( ) 0 ~0 I->0 1 ~1 0->1 a 2 {} 0->2 !a 1->0 !a & b & p 1->1 !b & p 1->2 !a & !b 3 ~1,~0 1->3 a & b & p 2->2 1 3->0 !a & b & p 3->1 a & !b & p 3->2 !a & !b 3->3 a & b & p

In [7]:
aut = spot.automaton('''
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--
'''); aut.show('.1ab')


Out[7]:
G Fin( ) 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

In [8]:
spot.remove_alternation(aut, True)


Out[8]:
G Inf( ) 0 3 I->0 1 ~0,4 0->1 a 1->0 !a 2 3,~1 1->2 a 3 4,~1,~0 2->3 a & b & p 4 0,4,~1 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->4 a 6->3 a & b & p 6->4 a & !b & p

In [9]:
# Example from ADL's PSL2TGBA talk.
aut = spot.automaton('''
HOA: v1
States: 6
Start: 0&3
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] 3
 [!0] 3&4
State: 4 {0}
 [!0] 4
 [0] 5
State: 5
 [t] 5
--END--
'''); aut.show('.1ab')


Out[9]:
G Fin( ) -7 I->-7 0 0 -7->0 3 3 -7->3 1 1 0->1 a 2 2 0->2 !a 3->3 a -4 3->-4 !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->3 4 4 -4->4 4->4 !a 5 5 4->5 a 5->5 1

In [10]:
spot.remove_alternation(aut, True)


Out[10]:
G Inf( )&Inf( ) 0 ~0,3 I->0 1 3,~1 0->1 a 2 3,4 0->2 !a 1->1 a & !b & p 1->2 !a & !b 4 3,4,~1 1->4 !a & !b & p 5 3,4,~0 1->5 !a & b & p 6 3,~1,~0 1->6 a & b & p 2->2 !a 3 3 2->3 a 4->1 a & !b & p 4->2 !a & !b 4->4 !a & !b & p 4->5 !a & b & p 4->6 a & b & p 5->1 a 5->2 !a 6->1 a & !b & p 6->2 !a & !b 6->5 !a & b & p 6->6 a & b & p 3->2 !a 3->3 a

In [11]:
a = spot.automaton('''
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--
'''); a


Out[11]:
G Fin( ) 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

In [12]:
spot.remove_alternation(a, True)


Out[12]:
G Inf( ) 0 0 I->0 1 0,1 0->1 1 1->1 1 1->1 a