notebook.community

Edit and run

This notebook shows an example of a non-deterministic automaton that Seminator can turn into a semi-deterministic automaton that is smaller than the minimal equivalent deterministic automaton.

Beside the Spot bindinges (that start with spot.) we use two functions exported by Seminator: the seminator() function offer services similar to the command-line tool, and the highlight_components() can be used to color the first (purple) and second (green) components of a semi-deterministic automaton.





In [1]:



    


import spot
from spot.jupyter import display_inline
from spot.seminator import seminator, highlight_components
spot.setup(show_default='.v') # vertical display



    











In [2]:



    


nba = spot.translate('F(a & GFb) R c')
sdba = seminator(nba)
dba = spot.postprocess(nba, 'det')
# add some colors
spot.highlight_nondet_edges(nba, 5)
highlight_components(sdba)



    











In [3]:



    


display_inline(nba, sdba, dba)



    


















    















Inf(
⓿
)
[Büchi]



0

0



I->0





0->0


c
⓿



1

1



0->1


a & c



2

2



0->2


!a & c



1->1


!b



1->1


b
⓿



2->1


a



2->2


!a












Inf(
⓿
)
[Büchi]



0

0



I->0





0->0


c



1

1



0->1


c



2

2



0->2


a & c



3

3



0->3


!a & c



1->1


c
⓿



2->2


!b



2->2


b
⓿



3->2


a



3->3


!a












Inf(
⓿
)
[Büchi]



0

0



I->0





1

1



0->1


!a & c



2

2



0->2


a & c



1->1


!a & c
⓿



1->2


a & c



3

3



1->3


!a & !c



4

4



1->4


a & !c



2->2


c
⓿



2->4


!c



3->3


!a



3->4


a



4->4


!b



4->4


b
⓿

To show that the deterministic Büchi automaton on the right is minimal, we use Spot's sat_minimize() function, that uses a SAT-solver to find a smaller equivalent DBA if one exists.





In [4]:



    


assert dba.num_states() == spot.sat_minimize(dba).num_states()

Content source: mklokocka/seminator

Similar notebooks:

notebook.community | gallery | about