Documentation for Spot's randltl Python binding¶

import spot

Basic usage¶

Generate random formulas from specified atomic propositions:

f = spot.randltl(['a', 'b', 'c'])
for i in range(3):
    print(next(f))

0
0 R b
F(XG(F!b M Fb) W (b R a))

Generate random formulas using 3 atomic propositions:

f = spot.randltl(3)
for i in range(3):
    print(next(f))

0
0 R p1
F(XG(F!p1 M Fp1) W (p1 R p0))

By default, there is no limit to the number of formulas generated.
To specify a number of formulas:

f = spot.randltl(3, 4)
for formula in f:
    print(formula)

0
0 R p1
F(XG(F!p1 M Fp1) W (p1 R p0))
F(p0 R !p2)

Keyword arguments¶

seed¶

Seed for the pseudo random number generator (default: 0).

f = spot.randltl(3, seed=11)
print(next(f))

G(p1 U Gp0)

output¶

Type of formulas to output: 'ltl', 'psl', 'bool' or 'sere' (default: 'ltl').

f = spot.randltl(3, output='psl', seed=26)
print(next(f))

{{1 | [*0]}[:*] & [*2]}

allow_dups¶

Allow duplicate formulas (default: False).

f = spot.randltl(1, allow_dups=True)
print(next(f))
print(next(f))
print(next(f))

0
0
Fp0

tree_size¶

Tree size of the formulas generated, before mandatory simplifications (default: 15).

f = spot.randltl(3, tree_size=30, seed=11)
print(next(f))

G(((p0 U !Xp1) M Gp1) U Gp0)

A range can be specified as a tuple:

f = spot.randltl(3, tree_size=(1, 40))
print(next(f))
print(next(f))

X!(Gp1 M p2) R (!p2 M Xp1)
F(G(F(Gp0 R (1 U Fp2)) M (p2 -> Gp0)) M F((p0 | Fp0) W Gp2))

boolean_priorities, ltl_priorities, sere_priorities, dump_priorities¶

f = spot.randltl(3, output='bool', boolean_priorities='and=10,or=0')
for i in range(5):
    print(next(f))

0
!p2 & (p1 <-> p2)
p2
p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))
1

To see which operators are available along with their default priorities:

spot.randltl(3, output='psl', dump_priorities=True)

Use argument ltl_priorities=STRING to set the following LTL priorities:

ap	3
false	1
true	1
not	1
F	1
G	1
X	1
Closure	1
equiv	1
implies	1
xor	1
R	1
U	1
W	1
M	1
and	1
or	1
EConcat	1
UConcat	1

Use argument sere_priorities=STRING to set the following SERE priorities:

ap	3
false	1
true	1
not	1
F	1
G	1
X	1
Closure	1
equiv	1
implies	1
xor	1
R	1
U	1
W	1
M	1
and	1
or	1
EConcat	1
UConcat	1
eword	1
boolform	1
star	1
star_b	1
fstar	1
fstar_b	1
first_match	1
and	1
andNLM	1
or	1
concat	1
fusion	1

Use argument boolean_priorities=STRING to set the following Boolean formula priorities:

ap	3
false	1
true	1
not	1
F	1
G	1
X	1
Closure	1
equiv	1
implies	1
xor	1
R	1
U	1
W	1
M	1
and	1
or	1
EConcat	1
UConcat	1
eword	1
boolform	1
star	1
star_b	1
fstar	1
fstar_b	1
first_match	1
and	1
andNLM	1
or	1
concat	1
fusion	1
ap	3
false	1
true	1
not	1
equiv	1
implies	1
xor	1
and	1
or	1

simplify¶

0 No rewriting
1 basic rewritings and eventual/universal rules
2 additional syntactic implication rules
3 better implications using containment
default: 3

f = spot.randltl(3, simplify=0, seed=5)
print(next(f))
f = spot.randltl(3, simplify=3, seed=5)
print(next(f))

G!(!p1 & (Xp2 | F(p0 R Xp2)))
G(p1 | (X!p2 & G(!p0 U X!p2)))

Filters and maps¶

most Boolean functions found in the class formula can be used to filter the random formula generator like this:

f = spot.randltl(3, 20).is_syntactic_stutter_invariant()
for formula in f:
    print(formula)

0
0 R p2
F(p0 R !p1)
G(p0 | Fp2) W (FGp2 R !p2)
(p2 R G!p1) | G(p2 U !p0)
(p2 W p0) U p2
F!G(!Gp1 W p1)
G!p1 & (!((p2 & Fp1) M p1) U p1)

likewise, functions from formula to formula can be applied to map the iterator:

f = spot.randltl(2, 6).remove_x()
for formula in f:
    print(formula)

0
!(F!p1 M 1)
(Gp0 | Fp1) M 1
F!(!p1 <-> FGp1)
Gp1 U (p1 U GFp1)
(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))

Since the Boolean filters and mapping functions return an iterator of the same type, these operations can be chained like this:

f = spot.randltl(3, 20).is_syntactic_stutter_invariant().relabel(spot.Abc).simplify()
for formula in f:
    print(formula)

0
Ga
F(a R !b)
G(a | Fb) | (FGb R !b)
G!b | G(a U !c)
b U a
0
0

for formula in spot.randltl(3, 10).simplify().unabbreviate("WMGFR"): print(formula)

0
!(1 U !p1)
1 U ((p0 U ((p0 & p1) | !(1 U !p0))) | !(1 U !((1 U !p1) & (1 U p1))))
1 U (!p2 U ((p0 & !p2) | !(1 U p2)))
(!p1 U ((!p1 & (1 U !(1 U !p1))) | !(1 U p1))) | !(1 U !(p0 | (1 U p1)))
X(p2 & X(p2 U (!p0 | !(1 U !p2))))
(1 U p2) | (X(!p2 | !(1 U !p2)) U (1 U (!p1 & (1 U p2))))
XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))
0
XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))