In [1]:
from IPython.display import display
import spot
from spot.jupyter import display_inline
spot.setup()

To build an automaton from an LTL formula, simply call translate() with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the ltl2tgba tool, and they can be abbreviated).

In [2]:
a = spot.translate('(a U b) & GFc & GFd', 'Buchi', 'state-based', 'complete'); a
Out[2]:
[Büchi] 0 0 I->0 0->0 a & !b 1 1 0->1 b & c & d 2 2 0->2 b & !d 3 3 0->3 b & !c & d 4 4 0->4 !a & !b 1->1 c & d 1->2 !d 1->3 !c & d 2->1 c & d 2->2 !d 2->3 !c & d 3->1 c 3->3 !c 4->4 1

The call the spot.setup() in the first cells has installed a default style for the graphviz output. If you want to change this style temporarily, you can call the show(style) method explicitly. For instance here is a vertical layout with the default font of GraphViz.

In [3]:
a.show("v")
Out[3]:
[Büchi] 0 0 I->0 0->0 a & !b 1 1 0->1 b & c & d 2 2 0->2 b & !d 3 3 0->3 b & !c & d 4 4 0->4 !a & !b 1->1 c & d 1->2 !d 1->3 !c & d 2->1 c & d 2->2 !d 2->3 !c & d 3->1 c 3->3 !c 4->4 1

If you want to add some style options to the existing one, pass a dot to the show() function in addition to your own style options:

In [4]:
a.show(".st")
Out[4]:
Inf( ⓿ ) [Büchi] cluster_0 cluster_1 cluster_2 0 0 I->0 0->0 a & !b 1 1 0->1 b & c & d 2 2 0->2 b & !d 3 3 0->3 b & !c & d 4 4 0->4 !a & !b 1->1 c & d ⓿ 1->2 !d ⓿ 1->3 !c & d ⓿ 2->1 c & d 2->2 !d 2->3 !c & d 3->1 c 3->3 !c 4->4 1

The translate() function can also be called with a formula object. Either as a function, or as a method.

In [5]:
f = spot.formula('a U b'); f
Out[5]:
$a \mathbin{\mathsf{U}} b$
In [6]:
spot.translate(f)
Out[6]:
[Büchi] 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1
In [7]:
f.translate()
Out[7]:
[Büchi] 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1

When used as a method, all the arguments are translation options. Here is a monitor:

In [8]:
f.translate('mon')
Out[8]:
t [all] 1 1 I->1 1->1 a & !b 0 0 1->0 b 0->0 1

The following three cells show a formulas for which it makes a difference to select 'small' or 'deterministic'.

In [9]:
f = spot.formula('Ga | Gb | Gc'); f
Out[9]:
$\mathsf{G} a \lor \mathsf{G} b \lor \mathsf{G} c$
In [10]:
f.translate('buchi', 'state-based', 'small').show('.v')
Out[10]:
[Büchi] 0 0 I->0 1 1 0->1 a 2 2 0->2 b 3 3 0->3 c 1->1 a 2->2 b 3->3 c
In [11]:
f.translate('buchi', 'state-based', 'det').show('v.')
Out[11]:
[Büchi] 6 6 I->6 6->6 a & b & c 0 0 6->0 !a & !b & c 1 1 6->1 !a & b & !c 2 2 6->2 a & !b & !c 3 3 6->3 !a & b & c 4 4 6->4 a & !b & c 5 5 6->5 a & b & !c 0->0 c 1->1 b 2->2 a 3->0 !b & c 3->1 b & !c 3->3 b & c 4->0 !a & c 4->2 a & !c 4->4 a & c 5->1 !a & b 5->2 a & !b 5->5 a & b

Here is how to build an unambiguous automaton:

In [12]:
spot.translate('GFa -> GFb', 'unambig')
Out[12]:
Inf( ⓿ ) [Büchi] 0 0 I->0 1 1 0->1 1 2 2 0->2 !a & !b 3 3 0->3 !a & !b 4 4 0->4 a | b 1->1 !b 1->1 b ⓿ 2->2 !a & !b 2->4 a | b 3->3 !a & !b ⓿ 4->2 !a & !b 4->3 !a & !b 4->4 a | b

Compare with the standard translation:

In [13]:
spot.translate('GFa -> GFb')
Out[13]:
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 1 1 1 0->1 b 2 2 0->2 !a 1->1 !b 1->1 b ⓿ 2->2 !a ⓿

And here is the automaton above with state-based acceptance:

In [14]:
a = spot.translate('GFa -> GFb', 'sbacc')
a
Out[14]:
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 b 2 2 0->2 !a 1->1 b 3 3 1->3 !b 2->2 !a 3->1 b 3->3 !b

Some example of running the self-loopization algorithm on an automaton:

In [15]:
a.is_empty()
Out[15]:
False

Reading from file (see automaton-io.ipynb for more examples).

In [16]:
%%file example1.aut
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 5 Inf(0)&Fin(1)&Fin(4) | Inf(2)&Inf(3) | Inf(1)
--BODY--
State: 0 {3}
[t] 0
[0] 1 {1}
[!0] 2 {0 4}
State: 1 {3}
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2 4}
State: 2 
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0 4}
--END--

Writing example1.aut
In [17]:
a = spot.automaton('example1.aut')
display(a)
display(spot.remove_fin(a))
display(a.postprocess('GeneralizedBuchi', 'complete'))
display(a.postprocess('Buchi', "SBAcc"))
(Inf( ⓿ ) & Fin( ❶ ) & Fin( ❹ )) | (Inf( ❷ )&Inf( ❸ )) | Inf( ❶ ) 0 0 I->0 0->0 1 ❸ 1 1 0->1 a ❶ ❸ 2 2 0->2 !a ⓿ ❸ ❹ 1->0 b ❸ 1->1 a & b ⓿ ❸ 1->2 !a & b ❷ ❸ ❹ 2->0 !b 2->1 a & !b ⓿ 2->2 !a & !b ⓿ ❹
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 1 1 1 0->1 a ⓿ 2 2 0->2 !a 3 3 0->3 1 1->0 b 1->1 a & b 1->2 !a & b ⓿ 4 4 1->4 a & b 2->0 !b 2->1 a & !b 2->2 !a & !b 3->3 1 4->4 a & b ⓿
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 1 1 1 0->1 a ⓿ 1->0 b 1->1 a & b 2 2 1->2 !a & b ⓿ 3 3 1->3 a & b 4 4 1->4 !b 2->0 !b 2->1 a & !b 2->4 b 3->3 a & b ⓿ 3->4 !a | !b 4->4 1
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 a 1->0 b 2 2 1->2 a & b 3 3 1->3 !a & b 4 4 1->4 a & b 2->2 a & b 2->3 !a & b 2->4 a & b 3->0 !b 3->2 a & !b 4->4 a & b
In [18]:
!rm example1.aut
In [19]:
spot.complete(a)
Out[19]:
(Inf( ⓿ ) & Fin( ❶ ) & Fin( ❹ )) | (Inf( ❷ )&Inf( ❸ )) | Inf( ❶ ) 0 0 I->0 0->0 1 ❸ 1 1 0->1 a ❶ ❸ 2 2 0->2 !a ⓿ ❸ ❹ 1->0 b ❸ 1->1 a & b ⓿ ❸ 1->2 !a & b ❷ ❸ ❹ 3 3 1->3 !b 2->0 !b 2->1 a & !b ⓿ 2->2 !a & !b ⓿ ❹ 2->3 b 3->3 1
In [20]:
spot.complete(spot.translate('Ga'))
Out[20]:
[Büchi] 0 0 I->0 0->0 a 1 1 0->1 !a 1->1 1
In [21]:
spot.formula('(a W c) & FGa').is_syntactic_persistence()
Out[21]:
True
In [22]:
# Using +1 in the display options is a convenient way to shift the 
# set numbers in the output, as an aid in reading the product.
a1 = spot.translate('GF(a <-> Xa)')
a2 = spot.translate('a U b & GFc')
display_inline(a1.show('.t'), a2.show('.t+1'))
# the product should display pairs of states, unless asked not to (using '1').
p = spot.product(a1, a2)
display_inline(p.show('.t'), p.show('.t1'), per_row=2)
Inf( ⓿ ) [Büchi] 0 0 I->0 0->0 a ⓿ 1 1 0->1 !a 1->0 a 1->1 !a ⓿
Inf( ❶ ) [Büchi] 0 0 I->0 0->0 a & !b 1 1 0->1 b 1->1 !c 1->1 c ❶
Inf( ⓿ )&Inf( ❶ ) [gen. Büchi 2] 0 0,0 I->0 0->0 a & !b ⓿ 1 0,1 0->1 a & b ⓿ 2 1,1 0->2 !a & b 1->1 a & !c ⓿ 1->1 a & c ⓿ ❶ 1->2 !a & !c 1->2 !a & c ❶ 2->1 a & !c 2->1 a & c ❶ 2->2 !a & !c ⓿ 2->2 !a & c ⓿ ❶
Inf( ⓿ )&Inf( ❶ ) [gen. Büchi 2] 0 0 I->0 0->0 a & !b ⓿ 1 1 0->1 a & b ⓿ 2 2 0->2 !a & b 1->1 a & !c ⓿ 1->1 a & c ⓿ ❶ 1->2 !a & !c 1->2 !a & c ❶ 2->1 a & !c 2->1 a & c ❶ 2->2 !a & !c ⓿ 2->2 !a & c ⓿ ❶

Explicit determinization after translation:

In [23]:
a = spot.translate('FGa')
display(a)
display(a.is_deterministic())
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 a 1->1 a 
False
In [24]:
spot.tgba_determinize(a)
Out[24]:
Fin( ⓿ ) & Inf( ❶ ) [Rabin 1] 0 0 I->0 0->0 !a 1 1 0->1 a ❶ 1->0 !a ⓿ 1->1 a ❶

Determinization by translate(). The generic option allows any acceptance condition to be used instead of the default generalized Büchi.

In [25]:
spot.translate('FGa', 'generic', 'deterministic')
Out[25]:
Fin( ⓿ ) [co-Büchi] 0 0 I->0 0->0 !a ⓿ 0->0 a

Translation to state-based co-Büchi automaton

In [26]:
spot.translate('FGa', 'coBuchi', 'deterministic', 'sbacc').show('.b')
Out[26]:
Fin( ⓿ ) [co-Büchi] 1 1 ⓿ I->1 1->1 !a 0 0 1->0 a 0->1 !a 0->0 a

Translation to parity automaton. Specifying just parity max odd requires a parity acceptance. Adding colored ensures that each transition (or state if sbacc is also given) has a color, as people usually expect in parity automata.

In [27]:
spot.translate('FGa', 'parity max odd', 'colored')
Out[27]:
Fin( ❷ ) & (Inf( ❶ ) | Fin( ⓿ )) [parity max odd 3] 0 0 I->0 0->0 a ❶ 0->0 !a ❷

Adding an atomic proposition to all edges

In [28]:
import buddy
display(a)
b = buddy.bdd_ithvar(a.register_ap('b'))
for e in a.edges():
    e.cond &= b
display(a)
[Büchi] 0 0 I->0 0->0 1 1 1 0->1 a 1->1 a
[Büchi] 0 0 I->0 0->0 b 1 1 0->1 a & b 1->1 a & b

Adding an atomic proposition to the edge between 0 and 1:

In [29]:
c = buddy.bdd_ithvar(a.register_ap('c'))
for e in a.out(0):
    if e.dst == 1:
        e.cond &= c
a
Out[29]:
[Büchi] 0 0 I->0 0->0 b 1 1 0->1 a & b & c 1->1 a & b
In [ ]: