import spot
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)
Seed for the pseudo random number generator (default: 0).
f = spot.randltl(3, seed=11)
print(next(f))
G(p1 U Gp0)
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 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 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))
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 strongX 0 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: 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 equiv 1 implies 1 xor 1 and 1 or 1
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)))
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))))