ltlmix

For each formula that it generates, ltlmix constructs a random syntax-tree of a certain size (5 by default) in which internal nodes represent operators selected randomly from a list of operators. Leaves of that tree are subformulas selected randomly from the set of input formulas. As an example, the syntax tree of !φ₁ xor !φ₂ has size 5, and its leaves φ₁ and φ₂ will be taken randomly from the set of input formulas.

The algorithm is actually the same as for randltl, except that randltl uses random atomic propositions as leaves when ltlmix uses random formulas.

The same input formula can be picked several times to be used on multiple leaves of the tree. Note that because Spot implements some trivial rewritings directly during the construction of any formula, formulas like FGb | !!FGb (which correspond to a tree of size 5 in the above example) cannot be represented: they are automatically simplified to FGb. Similarly, something like φ xor φ will be output as 0.

The size of the tree can be changed using the --tree-size option.

for i in 1 2 3 4 5 6 7 8 9 10 11 12; do
    ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i
done

Fc
!Xd
0
Ge xor !Fc
!Xd xor !Ge
!Xd xor (Fc | Xd)
!Ge
Ge xor (!Ge -> Gb)
Ge xor (!Xa -> !Fc)
(Ge & !Fc) xor (!Gb xor !Ge)
(Ge & !Fc) xor (!Gb xor (Gb | Fc))
(Ge & (Gb xor Xd)) xor (!Fc -> (Gb | Fc))

The above shows that while the size of the syntax tree generally grows along with --tree-size there are several cases where it reduces trivially.

It is possible to control the set of operators used in the generation. The first step is to obtain that list of operators with --dump-priorities. For instance:

ltlmix -fXa -fGb -fFc -fXd -fGe --dump-priorities

Use --boolean-priorities to set the following Boolean formula priorities:
sub	5
false	0
true	0
not	1
equiv	1
implies	1
xor	1
and	1
or	1

In the above list, false and true represent the Boolean constants: those are usually undesirable when building random Boolean formulas, especially with Spot's trivial rewritings. sub represents a random formula drawn from the list of input formulas.

The above command shows that each operator has a weight, called priority. When the priority is 0, the operator is never used. When ltlmix generates a syntax tree of size N, it looks among all operators that can be used at the root of such a tree, and performs a weighted random selection. In other words, an operator with priority 2 will be twice more likely to be selected than an operator with priority 1.

Those priorities can be changed with --boolean-priorities as in the following example, which disables xor and makes <-> thrice more likely to appear.

for i in 1 2 3 4 5 6 7 8 9 10 11 12; do
    ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i --boolean-prio='xor=0,equiv=3'
done

Fc
!Xd
1
Ge <-> !Fc
!Xd <-> !Ge
!Xd <-> (Fc | Xd)
Ge
Ge <-> (Gb <-> !Ge)
Ge <-> (!Fc <-> !Xa)
(Ge & !Fc) <-> (!Ge -> !Gb)
(Ge & !Fc) <-> ((Gb | Fc) -> !Gb)
(Ge & (Gb <-> Xd)) <-> ((Gb | Fc) <-> !Fc)

By default, the syntax tree generated on top of the randomly selected input formulas uses only Boolean operators.

Using option -L will use LTL operators instead.

ltlmix -fXa -fGb -fFc --tree-size=10 -L -n10

Gb R (XFc W 0)
!(Gb | !Xa)
1 U !X(0)
(Xa xor Gb) -> (GXa M Fc)
GFc M 1
(Fc U Gb) -> (0 R Xa)
!Gb <-> (Gb | GFc)
1
GFc | (1 U Xa)
!(Xa | GFc)

The following operators are used:

ltlmix -fXa -fGb -fFc -fXd -fGe -L --dump-priorities

Use --ltl-priorities to set the following LTL priorities:
sub	5
false	1
true	1
not	1
F	1
G	1
X	1
equiv	1
implies	1
xor	1
R	1
U	1
W	1
M	1
and	1
or	1

Note that in the LTL case, false and true can be generated by default: when building leave, alse and true have the same probability to be selected as any input formula.

The command genltl --dac-pattern will print a list of 55 LTL formulas representing various specification patterns listed by Dwyer et al. (FMSP'98). Using --stat=%x to count the atomic propositions in each formula, and some standard unix tools, we can compute that they use at most 6 atomic propositions.

genltl --dac-pattern --stat=%x | sort -n | tail -n 1

6

Based on this, we could decide to generate Boolean combination of those formulas while replacing atomic propositions by literals built out of a set of 10 atomic propositions (chosen larger than 6 to ensure that each individual formula will still make sense after the change of atomic propositions).

genltl --dac-pattern | ltlmix -n8 -P10

!G((p8 & F!p7) -> (!p4 U (!p7 | (!p2 & !p4 & X(!p4 U p1))))) xor !G(!p3 -> ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | (!p7 W !p4) | Gp7)))))))))
!G(!p3 -> Gp5) xor !G(!p7 -> G(p9 -> (!p5 & !p8 & X(!p5 U p2))))
G(p6 -> ((!(!p1 & p7 & X(!p1 U (!p1 & !p3))) U (p1 | !p2)) | G!(p7 & XF!p3))) & (G((!p4 & XF!p5) -> XF(!p5 & F!p0)) <-> G((p5 & !p6) -> (p5 W (p5 & p7))))
!G((p0 & p9) -> (!p7 W (!p0 | p4))) & !G((p1 & !p2) -> (!p8 W p2))
((Fp2 -> ((!p1 -> (!p2 U (p0 & !p2))) U p2)) -> G(p1 -> G(p9 -> (!p4 & p8 & X(!p4 U !p7))))) xor G(p1 -> Gp9)
!G((p5 & !p9 & F!p5) -> ((!p8 -> (p5 U (!p0 & p5))) U !p5)) -> !G((p6 & p9) -> (!p7 W !p9))
G((!p1 & !p2) -> (p9 W p1)) <-> (G(p5 -> G(p0 -> F!p4)) -> (Fp6 -> ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | (!p5 U p6)))))))))))
((Fp1 -> ((p6 -> (!p1 U (!p1 & !p2 & X(!p1 U !p9)))) U p1)) <-> (F!p0 -> (p0 U (p0 & !p7 & X(p0 U !p9))))) | (Fp2 -> (p6 U (p2 | (p6 & !p7 & X(p6 U p1)))))

Now we might want to clean this list a bit by relabeling each formula so is uses atomic propositions $\{p_0,p_1,...\}$ starting at 0 and without gap.

genltl --dac-pattern | ltlmix -n8 -P10 | ltlfilt --relabel=pnn

!G((p0 & F!p1) -> (!p2 U (!p1 | (!p2 & !p3 & X(!p2 U p4))))) xor !G(!p5 -> ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | (!p1 W !p2) | Gp1)))))))))
!G(!p0 -> Gp1) xor !G(!p2 -> G(p3 -> (!p1 & !p4 & X(!p1 U p5))))
G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & !p3))) U (p1 | !p4)) | G!(p2 & XF!p3))) & (G((!p5 & XF!p6) -> XF(!p6 & F!p7)) <-> G((!p0 & p6) -> (p6 W (p2 & p6))))
!G((p0 & p1) -> (!p2 W (!p0 | p3))) & !G((p4 & !p5) -> (!p6 W p5))
((Fp0 -> ((!p1 -> (!p0 U (!p0 & p2))) U p0)) -> G(p1 -> G(p3 -> (!p4 & p5 & X(!p4 U !p6))))) xor G(p1 -> Gp3)
!G((p0 & !p1 & F!p0) -> ((!p2 -> (p0 U (p0 & !p3))) U !p0)) -> !G((p1 & p4) -> (!p5 W !p1))
G((!p0 & !p1) -> (p2 W p0)) <-> (G(p3 -> G(p4 -> F!p5)) -> (Fp6 -> ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | (!p3 U p6)))))))))))
((Fp0 -> ((p1 -> (!p0 U (!p0 & !p2 & X(!p0 U !p3)))) U p0)) <-> (F!p4 -> (p4 U (p4 & !p5 & X(p4 U !p3))))) | (Fp2 -> (p1 U (p2 | (p1 & !p5 & X(p1 U p0)))))

Some benchmarks (e.g., for LTL satisfiability) are built as conjunctions of $L$ random formulas picked from a set of basic formulas. Each picked formula has its atomic propositions mapped to random literals built from a subset of $m$ atomic variables.

Given a value for $m$, option -P m will achieve the second part of the above description. To build a conjunction of $L$ formulas, we need to ask for a tree of size $2L-1$ in which only the and operator is allowed.

Here is an example with $L=10$ (hence --tree-size=19) and $m=50$. The example uses a small set of three basic formulas $\{\mathsf{G}a,\mathsf{F}a,\mathsf{X}a\}$ for illustration, but in practice you should replace these -f options by -F FILENAME pointing to a file containing all the input formulas to select from.

ltlmix -fGa -fFa -fXa -n10 -P50 \
       --tree-size=19 --boolean-prio=not=0,or=0,xor=0,equiv=0,implies=0

Xp27 & F!p21 & G!p19 & X!p26 & Fp4 & Gp43 & Fp39 & Fp7
G!p28 & G!p30 & X!p34 & Fp21 & Gp3 & Fp6 & F!p18 & Xp5 & Fp8 & F!p12
X!p32 & Xp9 & Gp4 & Xp48 & F!p48 & X!p6 & Fp5 & Xp20 & Fp28 & Fp26
G!p46 & X!p14 & Fp29 & X!p36 & Fp12 & Xp47 & Fp42 & Gp14 & Fp19
G!p28 & Fp21 & Fp36 & F!p0 & G!p14 & Xp21 & F!p28 & G!p21 & Gp21 & Gp40
Gp3 & F!p48 & F!p28 & Xp7 & Gp8 & Xp42 & Gp0 & Xp36 & F!p2 & G!p0
Xp36 & Xp46 & F!p31 & Xp11 & Xp26 & G!p9 & F!p36 & X!p12 & Fp15 & Xp18
Xp9 & X!p33 & Fp44 & X!p13 & Gp37 & Xp19 & G!p43 & F!p34 & Gp36 & Gp10
Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31

Random conjunctions is common enough to have its own flag. Using -C N will see the tree size to $2N-1$ and disable all operators but and. The above command can therefore be reduced to

ltlmix -fGa -fFa -fXa -n10 -P50 -C10

Xp27 & F!p21 & G!p19 & X!p26 & Fp4 & Gp43 & Fp39 & Fp7
G!p28 & G!p30 & X!p34 & Fp21 & Gp3 & Fp6 & F!p18 & Xp5 & Fp8 & F!p12
X!p32 & Xp9 & Gp4 & Xp48 & F!p48 & X!p6 & Fp5 & Xp20 & Fp28 & Fp26
G!p46 & X!p14 & Fp29 & X!p36 & Fp12 & Xp47 & Fp42 & Gp14 & Fp19
G!p28 & Fp21 & Fp36 & F!p0 & G!p14 & Xp21 & F!p28 & G!p21 & Gp21 & Gp40
Gp3 & F!p48 & F!p28 & Xp7 & Gp8 & Xp42 & Gp0 & Xp36 & F!p2 & G!p0
Xp36 & Xp46 & F!p31 & Xp11 & Xp26 & G!p9 & F!p36 & X!p12 & Fp15 & Xp18
Xp9 & X!p33 & Fp44 & X!p13 & Gp37 & Xp19 & G!p43 & F!p34 & Gp36 & Gp10
Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31

Selecting 10 random conjuncts out of 3×50×2=300 possibilities has a 13.7% chance that at least 2 conjuncts will be identical (see Birthday paradox), so because of Spot's trivial rewritings, some of the above formulas may have fewer than 10 conjuncts.

Generating formulas for LTL synthesis differs from LTL satisfiability because we have to deal with two sets of atomic proposition: one set for input, and one set for output.

Zhu et al. (IJCAI'17) generate their benchmark for LTL synthesis using a setup similar to the above, except that when atomic propositions are randomized, we must make sure not to change their input or output nature.

They use small examples from the Lily distribution as basic formulas to combine. Spot can print those formulas using genltl --lily. There are 23 of them, but we will limit ourselves to four of them for illustrative purpose.

genltl --lily=8..11

GFi0 -> GFo0
GFi0 -> (!o0 & G(!o0 -> ((!o0 U i0) & (i0 -> Fo0))) & GFo0)
(GFi1 | Fi0) -> (GFo1 | Go0)
!(G(i1 -> Fo0) & G(i0 -> Fo1))

Notice how these atomic propositions either start with i (for input) or o for output. This allows Spot to infer their nature. For instance, we could feed those directly to ltlsynt to decide if they are realizable:

genltl --lily=8..11 | ltlsynt --realizability

REALIZABLE
REALIZABLE
REALIZABLE
UNREALIZABLE

When randomizing the atomic propositions in these formulas before combining them, we want to replace each input (resp. output) proposition by a random input (resp. output) proposition. This is achieved by passing two numbers to -A or -P. In the case of Zhu et al., they do not change the polarity of the propositions during their generation, so we would use -A to mimic their setup.

Here are 6 random conjunctions of the above four patterns, in which each input (resp. output) atomic proposition has been replaced by a random input (resp. output) atomic proposition picked randomly in a set of 5 (resp. 4).

genltl --lily=8..11 | ltlmix -A5,4 -C3 -n6

!(G(i3 -> Fo3) & G(i2 -> Fo2)) & (GFi2 -> (!o1 & GFo1 & G(!o1 -> ((!o1 U i2) & (i2 -> Fo1))))) & (GFi4 -> GFo1)
(GFi2 -> (!o1 & GFo1 & G(!o1 -> ((!o1 U i2) & (i2 -> Fo1))))) & !(G(i0 -> Fo1) & G(i4 -> Fo3)) & (GFi4 -> (!o3 & GFo3 & G(!o3 -> ((i4 -> Fo3) & (!o3 U i4)))))
(GFi3 -> (!o3 & GFo3 & G(!o3 -> ((i3 -> Fo3) & (!o3 U i3))))) & ((GFi2 | Fi3) -> (GFo0 | Go2)) & ((Fi0 | GFi2) -> (GFo3 | Go2))
(GFi3 -> GFo2) & (GFi2 -> GFo0) & (GFi3 -> (!o0 & GFo0 & G(!o0 -> ((!o0 U i3) & (i3 -> Fo0)))))
!(G(i3 -> Fo1) & G(i1 -> Fo3)) & !(G(i3 -> Fo0) & G(i0 -> Fo2)) & ((GFi0 | Fi3) -> (GFo0 | Go1))
((Fi1 | GFi4) -> (Go0 | GFo2)) & !(G(i0 -> Fo2) & G(i4 -> Fo1)) & !(G(i3 -> Fo2) & G(i1 -> Fo1))

genltl --lily=8..11 | ltlmix -A5,4 -C3 -n6 | ltlsynt --realizability

UNREALIZABLE
UNREALIZABLE
REALIZABLE
UNREALIZABLE
UNREALIZABLE
UNREALIZABLE

Note that because one of the original pattern is unrealizable, any conjunction involving it will be unrealizable. Even if we had only realizable specifications to combine, the smaller the atomic proposition sets are, the more likely the random conjuncts will be in conflict. Therefore, increasing the number of atomic propositions to chose from may help to get more realizable formulas.

genltl --lily=8..11 | ltlmix -A50,50 -C3 -n6 | ltlsynt --realizability

UNREALIZABLE
UNREALIZABLE
REALIZABLE
REALIZABLE
UNREALIZABLE
UNREALIZABLE

When the original LTL synthesis specification formulas have atomic propositions that do not start with i or o, options --ins, --outs, or --part-file can be used to specify the nature of these atomic propositions. These options work as ltlsynt's input options.