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]:
In [3]:
aut2 = spot.remove_alternation(aut, True); aut2
Out[3]:
In [4]:
spot.scc_filter(aut2, True)
Out[4]:
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]:
In [6]:
spot.remove_alternation(aut, True)
Out[6]:
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]:
In [8]:
spot.remove_alternation(aut, True)
Out[8]:
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]:
In [10]:
spot.remove_alternation(aut, True)
Out[10]:
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]:
In [12]:
spot.remove_alternation(a, True)
Out[12]: