notebook.community

Edit and run 





In [1]:



    


import spot
from spot.jupyter import display_inline
from spot.seminator import seminator, ViaTGBA
spot.setup()

Effect of the Bottom-SCC optimisation on semi-deterministic automata

The orange states below form deterministic bottom SCCs. After processing by Seminator, they are both in the 1st (violet) and 2nd (green) component. Simplifications cannot merge these duplicates as one is accepting and one is not. In fact, we do not need the copy in the first component as there is no non-determinism and so there is nothing to wait for. We have to make every edge entering such SCC as a cut-edge.





In [2]:



    


def example(**opts):
    in_a = spot.translate("(FGp2 R !p2) | GFp1")
    in_a.highlight_states([3,4], 2).set_name("input")
    # Note: the pure=True option disables all optimizations that are usually on by default.
    out_a = seminator(in_a, pure=True, postprocess=False, highlight=True, **opts)
    out_a.set_name("output")
    simp_a = seminator(in_a, pure=True, postprocess=True, highlight=True, **opts)
    simp_a.set_name("simplified output")
    display_inline(in_a, out_a, simp_a, per_row=3, show=".vn")
    
example()



    


















    














input

input
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->1


!p2



2->2


!p2
⓿



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿











output

output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->1


!p2



2->2


!p2



5

{2} , ∅ , 0



2->5


!p2



3->3


1



6

{3} , ∅ , 0



3->6


p1



4->4


p2



7

{4} , ∅ , 0



4->7


p2



5->5


!p2
⓿



6->6


!p1



6->6


p1
⓿



7->7


p2
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->2


!p2
⓿



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿

Enabling the bottom-SCC optimization simplifies the output automata as follows:





In [3]:



    


example(bscc_avoid=True)



    


















    














input

input
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->1


!p2



2->2


!p2
⓿



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿











output

output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

{3} , ∅ , 0



0->3


1



1->1


1



4

{4} , ∅ , 0



1->4


p2



2->1


!p2



2->2


!p2



5

{2} , ∅ , 0



2->5


!p2



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿



5->5


!p2
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


1



4

4



0->4


!p2



1->1


1



3

3



1->3


p2



2->2


!p1



2->2


p1
⓿



4->4


!p2
⓿



3->3


p2
⓿

Cut-deterministic automata

The same idea can be applied to cut-deterministic automata. Removing the states 3 and 4 from the fist part of the cut-deterministic automaton would remove state $\{3\}$ and would merge the states $\{1,3,4\}$ and $\{1,3\}$.





In [4]:



    


example(cut_det=True)



    


















    














input

input
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->1


!p2



2->2


!p2
⓿



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿











output

output
Inf(
⓿
)
[Büchi]



0

{0}



I->0





1

{1,2,3}



0->1


!p2



2

{3}



0->2


p2



1->1


!p2



3

{1,3,4}



1->3


p2



5

{2} , ∅ , 0



1->5


!p2



6

{3} , ∅ , 0



1->6


p1



2->2


1



2->6


p1



3->3


p2



3->6


p1



4

{1,3}



3->4


!p2



7

{4} , ∅ , 0



3->7


p2



5->5


!p2
⓿



6->6


!p1



6->6


p1
⓿



4->3


p2



4->6


p1



4->4


!p2



7->7


p2
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


p2



1->1


!p2



3

3



1->3


p2



5

5



1->5


!p2



6

6



1->6


p1



2->2


!p1



2->6


p1



3->3


p2



3->6


p1



4

4



3->4


!p2



7

7



3->7


p2



5->5


!p2
⓿



6->6


!p1



6->6


p1
⓿



4->3


p2



4->6


p1



4->4


!p2



7->7


p2
⓿





















In [5]:



    


example(cut_det=True, bscc_avoid=True)



    


















    














input

input
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



2

2



0->2


!p2



3

3



0->3


1



1->1


1



4

4



1->4


p2



2->1


!p2



2->2


!p2
⓿



3->3


!p1



3->3


p1
⓿



4->4


p2
⓿











output

output
Inf(
⓿
)
[Büchi]



0

{0}



I->0





1

{1,2}



0->1


!p2



3

{3} , ∅ , 0



0->3


1



1->1


!p2



2

{1}



1->2


p2



4

{4} , ∅ , 0



1->4


p2



5

{2} , ∅ , 0



1->5


!p2



3->3


!p1



3->3


p1
⓿



2->2


1



2->4


p2



4->4


p2
⓿



5->5


!p2
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!p2



3

3



0->3


1



1->1


!p2



2

2



1->2


p2



4

4



1->4


p2



5

5



1->5


!p2



3->3


!p1



3->3


p1
⓿



2->2


1



2->4


p2



4->4


p2
⓿



5->5


!p2
⓿

Exension to semi-deterministic SCCs

We can avoid more than bottom SCC. In fact, we can avoid all SCCs that are already good for semi-deterministic automata (semi-deterministic SCC). SCC $C$ is semi-deterministic if $C$ and all successors of $C$ are deterministic. This is ilustrated on the following example and states 1 and 5.





In [6]:



    


def example2(**opts):
    in_a = spot.translate('G((((a & b) | (!a & !b)) & (GF!b U !c)) | (((!a & b) | (a & !b)) & (FGb R c)))')
    spot.highlight_nondet_states(in_a, 1)
    in_a.set_name("input")
    options = { "cut_det": True, "highlight": True, "jobs": ViaTGBA, "skip_levels": True, "pure": True, **opts}
    out_a = seminator(in_a, **options, postprocess=False)
    out_a.set_name("output")
    simp_a = seminator(in_a, **options, postprocess=True)
    simp_a.set_name("simplified output")
    display_inline(in_a, out_a, simp_a, show=".nhs")

example2()



    


















    














input

input
Inf(
⓿
)&Inf(
❶
)
[gen. Büchi 2]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)
⓿
❶



1

1



0->1


(!a & !b & c) | (a & b & c)



2

2



0->2


!a & b & c



3

3



0->3


(!a & b & c) | (a & !b & c)



4

4



0->4


(!a & b & c) | (a & !b & c)



6

6



6->6


!a & b & c
❶



6->6


a & !b & c
⓿
❶



1->1


!a & !b & c
⓿



1->1


a & b & c



5

5



1->5


!a & !b & !c
⓿
❶



1->5


a & b & !c
❶



5->6


(!a & b & c) | (a & !b & c)



5->1


!a & !b & c
⓿



5->1


a & b & c



5->5


!a & !b & !c
⓿
❶



5->5


a & b & !c
❶



2->2


(!a & b & c) | (a & b & !c)
⓿
❶



3->2


(!a & b & c) | (a & b & !c)



3->3


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



4->2


!a & b & c



4->3


(!a & b & c) | (a & !b & c)



4->4


(!a & b & c) | (a & !b & c)
⓿
❶











output

output
Inf(
⓿
)
[Büchi]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7



cluster_8



cluster_9





0

{0}



I->0





0->0


(!a & !b & !c) | (a & b & !c)



1

{1}



0->1


(!a & !b & c) | (a & b & c)



2

{2,3,4}



0->2


!a & b & c



3

{3,4}



0->3


a & !b & c



8

{0} , ∅ , 0



0->8


(!a & !b & !c) | (a & b & !c)



12

{6} , ∅ , 0



12->12


!a & b & c



12->12


a & !b & c
⓿



7

{6}



7->12


(!a & b & c) | (a & !b & c)



7->7


(!a & b & c) | (a & !b & c)



9

{5} , ∅ , 0



9->9


!a & !b & !c
⓿



9->9


a & b & !c



13

{1} , ∅ , 1



9->13


!a & !b & c
⓿



14

{1} , ∅ , 0



9->14


a & b & c



13->9


a & b & !c
⓿



13->13


(!a & !b & c) | (a & b & c)



15

{5} , ∅ , 1



13->15


!a & !b & !c
⓿



15->9


a & b & !c
⓿



15->13


(!a & !b & c) | (a & b & c)



15->15


!a & !b & !c
⓿



14->9


!a & !b & !c
⓿



14->9


a & b & !c



14->13


!a & !b & c
⓿



14->14


a & b & c



1->9


(!a & !b & !c) | (a & b & !c)



1->1


(!a & !b & c) | (a & b & c)



4

{5}



1->4


(!a & !b & !c) | (a & b & !c)



4->7


(!a & b & c) | (a & !b & c)



4->9


(!a & !b & !c) | (a & b & !c)



4->1


(!a & !b & c) | (a & b & c)



4->4


(!a & !b & !c) | (a & b & !c)



10

{2} , ∅ , 0



10->10


(!a & b & c) | (a & b & !c)
⓿



5

{3}



5->5


(!a & !b & !c) | (a & !b & c)



6

{2,3}



5->6


(!a & b & c) | (a & b & !c)



6->10


(!a & b & c) | (a & b & !c)



6->5


(!a & !b & !c) | (a & !b & c)



6->6


(!a & b & c) | (a & b & !c)



11

{4} , ∅ , 0



11->11


(!a & b & c) | (a & !b & c)
⓿



2->10


(!a & b & c) | (a & b & !c)



2->5


!a & !b & !c



2->6


a & b & !c



2->11


(!a & b & c) | (a & !b & c)



2->2


!a & b & c



2->3


a & !b & c



3->5


!a & !b & !c



3->6


a & b & !c



3->11


(!a & b & c) | (a & !b & c)



3->2


!a & b & c



3->3


a & !b & c



8->8


(!a & !b & !c) | (a & b & !c)
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7



cluster_8





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)



1

1



0->1


(!a & !b & c) | (a & b & c)



2

2



0->2


!a & b & c



3

3



0->3


a & !b & c



7

7



0->7


(!a & !b & !c) | (a & b & !c)



8

8



8->8


!a & !b & !c
⓿



8->8


a & b



12

12



8->12


!a & !b & c
⓿



12->8


a & b & !c
⓿



12->12


!a & !b & !c
⓿



12->12


(!a & !b & c) | (a & b & c)



11

11



11->11


!a & b & c



11->11


a & !b & c
⓿



1->8


(!a & !b & !c) | (a & b & !c)



1->1


(!a & !b & c) | (a & b & c)



4

4



1->4


(!a & !b & !c) | (a & b & !c)



4->8


(!a & !b & !c) | (a & b & !c)



4->11


(!a & b & c) | (a & !b & c)



4->1


(!a & !b & c) | (a & b & c)



4->4


(!a & !b & !c) | (a & b & !c)



9

9



9->9


(!a & b & c) | (a & b & !c)
⓿



5

5



5->5


(!a & !b & !c) | (a & !b & c)



6

6



5->6


(!a & b & c) | (a & b & !c)



6->9


(!a & b & c) | (a & b & !c)



6->5


(!a & !b & !c) | (a & !b & c)



6->6


(!a & b & c) | (a & b & !c)



10

10



10->10


(!a & b & c) | (a & !b & c)
⓿



2->9


(!a & b & c) | (a & b & !c)



2->5


!a & !b & !c



2->6


a & b & !c



2->10


(!a & b & c) | (a & !b & c)



2->2


!a & b & c



2->3


a & !b & c



3->5


!a & !b & !c



3->6


a & b & !c



3->10


(!a & b & c) | (a & !b & c)



3->2


!a & b & c



3->3


a & !b & c



7->7


(!a & !b & !c) | (a & b & !c)
⓿





















In [7]:



    


example2(bscc_avoid=True)



    


















    














input

input
Inf(
⓿
)&Inf(
❶
)
[gen. Büchi 2]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)
⓿
❶



1

1



0->1


(!a & !b & c) | (a & b & c)



2

2



0->2


!a & b & c



3

3



0->3


(!a & b & c) | (a & !b & c)



4

4



0->4


(!a & b & c) | (a & !b & c)



6

6



6->6


!a & b & c
❶



6->6


a & !b & c
⓿
❶



1->1


!a & !b & c
⓿



1->1


a & b & c



5

5



1->5


!a & !b & !c
⓿
❶



1->5


a & b & !c
❶



5->6


(!a & b & c) | (a & !b & c)



5->1


!a & !b & c
⓿



5->1


a & b & c



5->5


!a & !b & !c
⓿
❶



5->5


a & b & !c
❶



2->2


(!a & b & c) | (a & b & !c)
⓿
❶



3->2


(!a & b & c) | (a & b & !c)



3->3


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



4->2


!a & b & c



4->3


(!a & b & c) | (a & !b & c)



4->4


(!a & b & c) | (a & !b & c)
⓿
❶











output

output
Inf(
⓿
)
[Büchi]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7



cluster_8





0

{0}



I->0





0->0


(!a & !b & !c) | (a & b & !c)



5

{2} , ∅ , 0



0->5


!a & b & c



1

{3,4}



0->1


(!a & b & c) | (a & !b & c)



3

{0} , ∅ , 0



0->3


(!a & !b & !c) | (a & b & !c)



4

{1} , ∅ , 0



0->4


(!a & !b & c) | (a & b & c)



5->5


(!a & b & c) | (a & b & !c)
⓿



2

{3}



2->5


(!a & b & c) | (a & b & !c)



2->2


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



6

{4} , ∅ , 0



6->6


(!a & b & c) | (a & !b & c)
⓿



1->5


(!a & b & c) | (a & b & !c)



1->2


(!a & !b & !c) | (a & b & !c)



1->6


(!a & b & c) | (a & !b & c)



1->1


(!a & b & c) | (a & !b & c)



3->3


(!a & !b & !c) | (a & b & !c)
⓿



9

{6} , ∅ , 0



9->9


!a & b & c



9->9


a & !b & c
⓿



11

{6} , ∅ , 1



11->9


!a & b & c
⓿



11->11


a & !b & c
⓿



4->4


a & b & c



7

{5} , ∅ , 0



4->7


!a & !b & !c
⓿



4->7


a & b & !c



8

{1} , ∅ , 1



4->8


!a & !b & c
⓿



7->9


(!a & b & c) | (a & !b & c)



7->4


a & b & c



7->7


!a & !b & !c
⓿



7->7


a & b & !c



7->8


!a & !b & c
⓿



8->7


a & b & !c
⓿



8->8


(!a & !b & c) | (a & b & c)



10

{5} , ∅ , 1



8->10


!a & !b & !c
⓿



10->11


(!a & b & c) | (a & !b & c)



10->7


a & b & !c
⓿



10->8


(!a & !b & c) | (a & b & c)



10->10


!a & !b & !c
⓿











simplified output

simplified output
Inf(
⓿
)
[Büchi]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7



cluster_8





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)



5

5



0->5


!a & b & c



1

1



0->1


(!a & b & c) | (a & !b & c)



3

3



0->3


(!a & !b & !c) | (a & b & !c)



4

4



0->4


(!a & !b & c) | (a & b & c)



5->5


(!a & b & c) | (a & b & !c)
⓿



2

2



2->5


(!a & b & c) | (a & b & !c)



2->2


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



6

6



6->6


(!a & b & c) | (a & !b & c)
⓿



1->5


(!a & b & c) | (a & b & !c)



1->2


(!a & !b & !c) | (a & b & !c)



1->6


(!a & b & c) | (a & !b & c)



1->1


(!a & b & c) | (a & !b & c)



3->3


(!a & !b & !c) | (a & b & !c)
⓿



9

9



9->9


!a & b & c



9->9


a & !b & c
⓿



11

11



11->9


!a & b & c



11->11


a & !b & c
⓿



4->4


a & b & c



7

7



4->7


!a & !b & !c
⓿



4->7


a & b & !c



8

8



4->8


!a & !b & c
⓿



7->9


(!a & b & c) | (a & !b & c)



7->4


a & b & c



7->7


!a & !b & !c
⓿



7->7


a & b & !c



7->8


!a & !b & c
⓿



8->7


a & b & !c
⓿



8->8


(!a & !b & c) | (a & b & c)



10

10



8->10


!a & !b & !c
⓿



10->11


(!a & b & c) | (a & !b & c)



10->7


a & b & !c
⓿



10->8


(!a & !b & c) | (a & b & c)



10->10


!a & !b & !c
⓿

Reusing the semi-deterministic components with TGBA acceptance

In the previous example we have saved several states by not including the semi-deterministic components in the 1st part of the result. However, we still got 6 (and 5 after postprocessing) states out of the 3 deterministic states $1, 5$, and $6$. This can be tackled by reusing the semi-deterministic components as they are. This immediately leads to a TGBA on the output and we have to adress this in the parts which still rely on breakpoint construction. The edges that are accepting will now carry all the marks that are needed (as they do in the original automaton anyway).





In [8]:



    


example2(powerset_on_cut=True, reuse_deterministic=True)



    


















    














input

input
Inf(
⓿
)&Inf(
❶
)
[gen. Büchi 2]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)
⓿
❶



1

1



0->1


(!a & !b & c) | (a & b & c)



2

2



0->2


!a & b & c



3

3



0->3


(!a & b & c) | (a & !b & c)



4

4



0->4


(!a & b & c) | (a & !b & c)



6

6



6->6


!a & b & c
❶



6->6


a & !b & c
⓿
❶



1->1


!a & !b & c
⓿



1->1


a & b & c



5

5



1->5


!a & !b & !c
⓿
❶



1->5


a & b & !c
❶



5->6


(!a & b & c) | (a & !b & c)



5->1


!a & !b & c
⓿



5->1


a & b & c



5->5


!a & !b & !c
⓿
❶



5->5


a & b & !c
❶



2->2


(!a & b & c) | (a & b & !c)
⓿
❶



3->2


(!a & b & c) | (a & b & !c)



3->3


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



4->2


!a & b & c



4->3


(!a & b & c) | (a & !b & c)



4->4


(!a & b & c) | (a & !b & c)
⓿
❶











output

output
Inf(
⓿
)&Inf(
❶
)
[gen. Büchi 2]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7





0

{0}



I->0





0->0


(!a & !b & !c) | (a & b & !c)



5

2



0->5


!a & b & c



1

{3,4}



0->1


(!a & b & c) | (a & !b & c)



3

{0} , ∅ , 0



0->3


(!a & !b & !c) | (a & b & !c)



4

1



0->4


(!a & !b & c) | (a & b & c)



5->5


(!a & b & c) | (a & b & !c)
⓿
❶



2

{3}



2->5


(!a & b & c) | (a & b & !c)



2->2


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



6

{4} , ∅ , 0



6->6


(!a & b & c) | (a & !b & c)
⓿
❶



1->5


(!a & b & c) | (a & b & !c)



1->2


(!a & !b & !c) | (a & b & !c)



1->6


(!a & b & c) | (a & !b & c)



1->1


(!a & b & c) | (a & !b & c)



3->3


(!a & !b & !c) | (a & b & !c)
⓿
❶



8

6



8->8


!a & b & c
❶



8->8


a & !b & c
⓿
❶



4->4


!a & !b & c
⓿



4->4


a & b & c



7

5



4->7


!a & !b & !c
⓿
❶



4->7


a & b & !c
❶



7->8


(!a & b & c) | (a & !b & c)



7->4


!a & !b & c
⓿



7->4


a & b & c



7->7


!a & !b & !c
⓿
❶



7->7


a & b & !c
❶











simplified output

simplified output
Inf(
⓿
)&Inf(
❶
)
[gen. Büchi 2]

cluster_0



cluster_1



cluster_2



cluster_3



cluster_4



cluster_5



cluster_6



cluster_7





0

0



I->0





0->0


(!a & !b & !c) | (a & b & !c)



5

5



0->5


!a & b & c



1

1



0->1


(!a & b & c) | (a & !b & c)



3

3



0->3


(!a & !b & !c) | (a & b & !c)



4

4



0->4


(!a & !b & c) | (a & b & c)



5->5


(!a & b & c) | (a & b & !c)
⓿
❶



2

2



2->5


(!a & b & c) | (a & b & !c)



2->2


(!a & !b & !c) | (!a & b & c) | (a & !b & c) | (a & b & !c)



6

6



6->6


(!a & b & c) | (a & !b & c)
⓿
❶



1->5


(!a & b & c) | (a & b & !c)



1->2


(!a & !b & !c) | (a & b & !c)



1->6


(!a & b & c) | (a & !b & c)



1->1


(!a & b & c) | (a & !b & c)



3->3


(!a & !b & !c) | (a & b & !c)
⓿
❶



8

8



8->8


!a & b & c
❶



8->8


a & !b & c
⓿
❶



4->4


!a & !b & c
⓿



4->4


a & b & c



7

7



4->7


!a & !b & !c
⓿
❶



4->7


a & b & !c
❶



7->8


(!a & b & c) | (a & !b & c)



7->4


!a & !b & c
⓿



7->4


a & b & c



7->7


!a & !b & !c
⓿
❶



7->7


a & b & !c
❶





















In [ ]:

Content source: mklokocka/seminator

Similar notebooks:

notebook.community | gallery | about