Formulas & Automata generators¶

The spot.gen package contains the functions used to generate the patterns produced by genltl and genaut.

In [1]:
import spot
import spot.gen as sg
spot.setup(show_default='.an')
from IPython.display import display

LTL patterns¶

Generation of LTL formulas is done via the ltl_pattern() function. This takes two arguments: a pattern id, and a pattern size (or index if the id refers to a list).

In [2]:
sg.ltl_pattern(sg.LTL_AND_GF, 3)
Out[2]:
$\mathsf{G} \mathsf{F} p_{1} \land \mathsf{G} \mathsf{F} p_{2} \land \mathsf{G} \mathsf{F} p_{3}$
In [3]:
sg.ltl_pattern(sg.LTL_CCJ_BETA_PRIME, 4)
Out[3]:
$\mathsf{F} (p \land \mathsf{X} p \land \mathsf{X} \mathsf{X} p \land \mathsf{X} \mathsf{X} \mathsf{X} p) \land \mathsf{F} (q \land \mathsf{X} q \land \mathsf{X} \mathsf{X} q \land \mathsf{X} \mathsf{X} \mathsf{X} q)$

To see the list of supported patterns, the easiest way is to look at the --help output of genltl. The above pattern for instance is attached to option --ccj-beta-prime. The name of the pattern identifier is the same using capital letters, underscores, and an LTL_ prefix. If a pattern has multiple aliased options in genltl, the first one used for the identifier (e.g., genltl accept both --dac-patterns and --spec-patterns as synonyms to denote the patterns of spot.gen.LTL_DAC_PATTERNS).

Multiple patterns can be generated using the ltl_patterns() function. It's arguments should be either can be:

  • pairs of the form (id, n): in this case the pattern id with size/index n is returned,
  • triplets of the form (id, min, max): in this case the patterns are output for all n between min and max included,
  • an integer id: then this is equivalent to (id, 1, 10) if the pattern has now upper bound, or (id, 1, upper) if the patter id has an upper bound upper. This is mostly used when the pattern id correspond to a hard-coded list of formulas.

Here is an example showing these three types of arguments:

In [4]:
for f in sg.ltl_patterns((sg.LTL_GH_R, 3), (sg.LTL_AND_FG, 1, 3), sg.LTL_EH_PATTERNS):
    display(f)
$(\mathsf{G} \mathsf{F} p_{1} \lor \mathsf{F} \mathsf{G} p_{2}) \land (\mathsf{G} \mathsf{F} p_{2} \lor \mathsf{F} \mathsf{G} p_{3}) \land (\mathsf{G} \mathsf{F} p_{3} \lor \mathsf{F} \mathsf{G} p_{4})$
$\mathsf{F} \mathsf{G} p_{1}$
$\mathsf{F} \mathsf{G} p_{1} \land \mathsf{F} \mathsf{G} p_{2}$
$\mathsf{F} \mathsf{G} p_{1} \land \mathsf{F} \mathsf{G} p_{2} \land \mathsf{F} \mathsf{G} p_{3}$
$p_{0} \mathbin{\mathsf{U}} (p_{1} \land \mathsf{G} p_{2})$
$p_{0} \mathbin{\mathsf{U}} (p_{1} \land \mathsf{X} (p_{2} \mathbin{\mathsf{U}} p_{3}))$
$p_{0} \mathbin{\mathsf{U}} (p_{1} \land \mathsf{X} (p_{2} \land \mathsf{F} (p_{3} \land \mathsf{X} \mathsf{F} (p_{4} \land \mathsf{X} \mathsf{F} (p_{5} \land \mathsf{X} \mathsf{F} p_{6})))))$
$\mathsf{F} (p_{0} \land \mathsf{X} \mathsf{G} p_{1})$
$\mathsf{F} (p_{0} \land \mathsf{X} (p_{1} \land \mathsf{X} \mathsf{F} p_{2}))$
$\mathsf{F} (p_{0} \land \mathsf{X} (p_{1} \mathbin{\mathsf{U}} p_{2}))$
$\mathsf{G} \mathsf{F} p_{0} \lor \mathsf{F} \mathsf{G} p_{1}$
$\mathsf{G} (p_{0} \rightarrow (p_{1} \mathbin{\mathsf{U}} p_{2}))$
$\mathsf{G} (p_{0} \land \mathsf{X} \mathsf{F} (p_{1} \land \mathsf{X} \mathsf{F} (p_{2} \land \mathsf{X} \mathsf{F} p_{3})))$
$\mathsf{G} \mathsf{F} p_{1} \land \mathsf{G} \mathsf{F} p_{2} \land \mathsf{G} \mathsf{F} p_{3} \land \mathsf{G} \mathsf{F} p_{0} \land \mathsf{G} \mathsf{F} p_{4}$
$(p_{0} \mathbin{\mathsf{U}} (p_{1} \mathbin{\mathsf{U}} p_{2})) \lor (p_{1} \mathbin{\mathsf{U}} (p_{2} \mathbin{\mathsf{U}} p_{0})) \lor (p_{2} \mathbin{\mathsf{U}} (p_{0} \mathbin{\mathsf{U}} p_{1}))$
$\mathsf{G} (p_{0} \rightarrow (p_{1} \mathbin{\mathsf{U}} (\mathsf{G} p_{2} \lor \mathsf{G} p_{3})))$

Some LTL patterns take two arguments. In this case, the arguments passed to ltl_pattern() should be one of:

  • (id, n, m) giving the value of both arguments,
  • (id, min1, max1, min2, max2) specifying a range for both arguments,
  • (id, n) equivalent to (id, n, n),
  • id equivalent to (id, 1, 3, 1, 3).
In [5]:
for f in sg.ltl_patterns(sg.LTL_SEJK_F):
    display(f)
$\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} b)$
$\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b)$
$\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} \mathsf{X} b)$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{3} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} b)))$
$\mathsf{G} \mathsf{F} a_{3} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b)))$
$\mathsf{G} \mathsf{F} a_{3} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} \mathsf{X} b)))$
In [6]:
for f in sg.ltl_patterns((sg.LTL_SEJK_F, 2, 3), (sg.LTL_SEJK_F, 2), (sg.LTL_SEJK_F, 1, 2, 1, 2)):
    display(f)
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} b)$
$\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b)$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} b))$
$\mathsf{G} \mathsf{F} a_{2} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{1} \mathbin{\mathsf{U}} \mathsf{G} (\mathsf{G} \mathsf{F} a_{0} \mathbin{\mathsf{U}} \mathsf{X} \mathsf{X} b))$

Automata patterns¶

We currently have only a couple of generators of automata:

In [7]:
examples = []
for p in (sg.AUT_KS_NCA, sg.AUT_L_DSA, sg.AUT_L_NBA, sg.AUT_M_NBA,
          sg.AUT_CYCLIST_PROOF_DBA, sg.AUT_CYCLIST_TRACE_NBA,
          sg.AUT_CYCLE_LOG_NBA, sg.AUT_CYCLE_ONEHOT_NBA):
    aut = sg.aut_pattern(p, 3)
    aut.set_name(sg.aut_pattern_name(p) + "=3")
    examples.append(aut)

display(*examples)
ks-nca=3 ks-nca=3 [co-Büchi] 0 0 I->0 1 1 0->1 1 2 2 0->2 1 3 3 0->3 1 4 4 0->4 1 5 5 0->5 1 6 6 0->6 1 1->0 !a & !b 1->1 a & b 1->2 (!a & b) | (a & !b) 2->1 !a & b 2->2 (!a & !b) | (a & b) 2->3 a & !b 3->3 !a | b 3->4 a & !b 4->4 !a | b 4->5 a & !b 5->5 !a | b 5->6 a & !b 6->1 a & !b 6->6 !a | b
l-dsa=3 l-dsa=3 (Fin( ⓿ ) | Inf( ❶ )) & (Fin( ❷ ) | Inf( ❸ )) & (Fin( ❹ ) | Inf( ❺ )) [Streett 3] 0 0 ⓿ I->0 2 2 0->2 a 3 3 ❶ 2->3 !a 6 6 2->6 a 1 1 1->0 !a 5 5 1->5 a 4 4 ❷ 5->4 !a 9 9 5->9 a 3->1 a 7 7 ❸ 6->7 !a 10 10 6->10 a 4->2 a 9->9 a 8 8 ❹ 9->8 !a 7->1 a 10->10 a 11 11 ❺ 10->11 !a 8->2 a 11->1 a
l-nba=3 l-nba=3 [Büchi] 1 1 I->1 1->1 a | b 7 7 1->7 a & !b 0 0 4 4 0->4 a & !b 4->1 !a & b 5 5 4->5 a & !b 7->0 !a & b 2 2 2->2 a | b 8 8 2->8 a & !b 8->7 a & !b 3 3 3->3 a | b 9 9 3->9 a & !b 9->8 a & !b 9->9 a & !b 5->2 !a & b 6 6 5->6 a & !b 6->3 !a & b 6->6 a & !b
m-nba=3 m-nba=3 [Büchi] 0 0 I->0 3 3 0->3 p0 & p1 2 2 0->2 p0 & !p1 1 1 0->1 !p0 & p1 3->0 p0 & p1 3->3 1 2->0 p0 & !p1 2->2 1 1->0 !p0 & p1 1->1 1
cyclist-proof-dba=3 cyclist-proof-dba=3 [Büchi] 0 0 I->0 1 1 0->1 !p0 & !p1 2 2 1->2 !p0 & p1 3 3 1->3 p0 & !p1 4 4 1->4 p0 & p1 2->1 !p0 & !p1 3->1 !p0 & !p1 4->1 !p0 & !p1
cyclist-trace-nba=3 cyclist-trace-nba=3 [Büchi] 0 0 I->0 0->0 1 1 1 0->1 !p0 & !p1 2 2 1->2 !p0 & p1 3 3 1->3 p0 & !p1 4 4 1->4 p0 & p1 2->1 !p0 & !p1 3->1 !p0 & !p1 4->1 !p0 & !p1
cycle-log-nba=3 cycle-log-nba=3 [Büchi] 0 0 I->0 1 1 0->1 !p0 & !p1 1->1 1 2 2 1->2 !p0 & p1 2->2 1 3 3 2->3 p0 & !p1 4 4 3->4 !p0 & !p1 4->4 1 5 5 4->5 !p0 & p1 5->5 1 6 6 5->6 p0 & !p1 7 7 6->7 !p0 & !p1 7->7 1 8 8 7->8 !p0 & p1 8->0 p0 & !p1 8->8 1
cycle-onehot-nba=3 cycle-onehot-nba=3 [Büchi] 0 0 I->0 1 1 0->1 p0 & !p1 & !p2 1->1 1 2 2 1->2 !p0 & p1 & !p2 2->2 1 3 3 2->3 !p0 & !p1 & p2 4 4 3->4 p0 & !p1 & !p2 4->4 1 5 5 4->5 !p0 & p1 & !p2 5->5 1 6 6 5->6 !p0 & !p1 & p2 7 7 6->7 p0 & !p1 & !p2 7->7 1 8 8 7->8 !p0 & p1 & !p2 8->0 !p0 & !p1 & p2 8->8 1

Multiple automata can be generated using the aut_patterns() function, which works similarly to ltl_patterns().

In [8]:
for aut in sg.aut_patterns(sg.AUT_KS_NCA):
    print(aut.num_states())

3
5
7
9
11
13
15
17
19
21