SpotAutomaton class

SpotAutomaton Interface¶

SpotAutomaton class provides an interface between spot and ggsolver. Given an LTL formula, SpotAutomaton determines the best options for spot.translate() function to generate a deterministic automaton in ggsolver.Automaton format.

In [61]:

# This code block is necessary when running in `ggsolver:v0.1` docker image.
import sys
sys.path.append('/home/ggsolver/')

SpotAutomaton class is available in the interfaces subpackage.

In [62]:

from ggsolver.interfaces.i_spot import *

The constructor takes two arguments: formula and options. If options are not provided, then options are selected based on where the LTL formula lies in Manna-Pnueli Hierarchy.

See documentation to understand how options are selected.

In [63]:

aut = SpotAutomaton("Fa & Gb ")

[INFO] Translating Fa & Gb  with options=('Buchi', 'Deterministic', 'High', 'Complete', 'Unambiguous', 'SBAcc') ...

In [64]:

aut1 = SpotAutomaton("FGa")

[INFO] Translating FGa with options=('coBuchi', 'Deterministic', 'High', 'Complete', 'Unambiguous', 'SBAcc') ...

In [65]:

aut2 = SpotAutomaton("FGa & GFb")

[INFO] Translating FGa & GFb with options=('parity', 'Deterministic', 'High', 'Complete', 'Unambiguous', 'SBAcc', 'colored') ...

SpotAutomaton is a GraphicalModel that inherits from Automaton model. Hence, we can access states, sigma, delta, init_state, final functions as usual.

Note: By default, Automaton defines atoms() to be the set of atomic propositions and sigma() as the powerset of atomic propositions.

Warning: Currently, the size of atoms() set is limited to 16 atoms because sigma() explicitly constructs the powerset of atoms().

In [66]:

aut.states()

Out[66]:

[0, 1, 2]

In [67]:

aut.atoms()

Out[67]:

['a', 'b']

In [68]:

aut.sigma()

Out[68]:

[(), ('a',), ('b',), ('a', 'b')]

The input to delta function is an element of sigma. It should either be a list or tuple of atoms.

In [69]:

print(aut.delta(0, []))
print(aut.delta(0, ['a']))
print(aut.delta(1, ['b']))

2
2
1

In [70]:

aut.init_state()

Out[70]:

1

Since the definition of final states varies based on acceptance condition, we follow spot's convention and define final to be a function that maps each state to a list (or tuple) of acceptance sets.

In [71]:

print(aut.final(0))
print(aut.final(1))
print(aut.final(2))

[0]
[]
[]

In [72]:

print(aut2.final(0))
print(aut2.final(1))
print(aut2.final(2))

[0]
[2]
[2]

In addition, SpotAutomaton also exposes the properties assigned by spot to the automaton.

In [73]:

print("formula: ", aut.formula())
print("acc_name: ", aut.acc_name())
print("spot_acc_cond: ", aut.spot_acc_cond())
print("num_acc_sets: ", aut.num_acc_sets())
print("is_deterministic: ", aut.is_deterministic())
print("is_unambiguous: ", aut.is_unambiguous())
print("is_state_based_acc: ", aut.is_state_based_acc())
print("is_terminal: ", aut.is_terminal())
print("is_weak: ", aut.is_weak())
print("is_inherently_weak: ", aut.is_inherently_weak())
print("is_stutter_invariant: ", aut.is_stutter_invariant())

formula:  Fa & Gb 
acc_name:  Büchi
spot_acc_cond:  Inf(0)
num_acc_sets:  1
is_deterministic:  True
is_unambiguous:  True
is_state_based_acc:  True
is_terminal:  False
is_weak:  True
is_inherently_weak:  True
is_stutter_invariant:  True

Since SpotAutomaton is a GraphicalModel, it can be serialized or converted to PNG in the same way as any other graphical model.

In [ ]: