randltl.org 10.3 KB
Newer Older
1
#+TITLE: =randltl=
2
3
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
4
5
6
7
8
9

This tool generates random formulas.  By default, it will generate one
random LTL formula using atomic propositions supplied on the
command-line.  It can be instructed to generate random Boolean or PSL
formulas instead, but let us first focus on LTL generation.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
10
For instance to obtain fave random LTL formula over the propositions
11
12
13
=a=, =b=, or =c=, use:

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14
randltl -n5 a b c
15
16
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
17
18
19
20
21
: 1
: !(!((a U Gb) U b) U GFa)
: GF((b R !a) U (Xc M 1))
: (b <-> Xc) xor Fb
: FXb R (a R (1 U b))
22
23
24

Note that the result does not always use all atomic propositions.

25
26
27
28
If you do not care about how the atomic propositions are named,
you can give a nonnegative number instead:

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29
randltl -n5 3
30
31
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
33
34
35
36
: 1
: !(!((p0 U Gp1) U p1) U GFp0)
: GF((p1 R !p0) U (Xp2 M 1))
: (p1 <-> Xp2) xor Fp1
: FXp1 R (p0 R (1 U p1))
37

38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
The syntax of the formula output can be changed using the
[[file:ioltl.org][common output options]]:

#+BEGIN_SRC sh :results verbatim :exports results
randltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
:   -8, --utf8                 output using UTF-8 characters
:   -l, --lbt                  output in LBT's syntax
:   -p, --full-parentheses     output fully-parenthesized formulas
:   -s, --spin                 output in Spin's syntax
:       --spot                 output in Spot's syntax (default)
:       --wring                output in Wring's syntax

When you select Spin's or Wring's syntax, operators =W= and =M= are
automatically rewritten using =U= and =R= (written =V= for Spin).
When you select LBT's syntax, you should name you atomic propositions
like =p0=, =p1=, etc... (Atomic proposition named differently will be
output by Spot in double-quotes, but this is not supported by LBT.)

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
60
61
62
randltl -l 12
randltl -8 12
randltl -s 12
randltl --wring 12
63
#+END_SRC
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
64

65
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
67
68
69
: V ! X ^ G p4 M p10 F ! p11 V G p3 p5
: ¬○(□p4⊕(p10 M ◇¬p11)) R (□p3 R p5)
: !X(([]p4 && !(<>!p11 U (p10 && <>!p11))) || (![]p4 && (<>!p11 U (p10 && <>!p11)))) V ([]p3 V p5)
: (!(X((G(p4=1)) ^ ((F(p11=0)) U ((p10=1) * (F(p11=0))))))) R ((G(p3=1)) R (p5=1))
70
71
72
73

As you might guess from the above result, for a given set of atomic
propositions (and on the same computer) the generated formula will
always be the same.  This is because each time =randltl= starts, it
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
initializes the seed of the random number generator to =0=.  This seed
75
76
77
can be changed using the =--seed= option.  For instance the following
three commands:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
78
#+NAME: result-seed
79
80
81
82
83
84
85
86
#+BEGIN_SRC sh :results verbatim :exports both
randltl a b c
randltl --seed=123 a b c
randltl --seed=0 a b c
#+END_SRC

Will give three formulas in which the first and last are identical:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
88
89
90
#+RESULTS: result-seed
: 1
: b W 0
: 1
91
92
93
94

When generating random formulas, we usually want large quantity of
them.  Rather than running =randltl= several times with different
seeds, we can use the =-n= option to specify a number of formulas to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
95
produce as seen in the very first example of this page.
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123

By default =randltl= will never output the same formula twice (this
can be changed with the =--allow-dups= option), so it may generate
more formulas internally than it eventually prints.  To ensure
termination, for each output formula the number of ignored (because
duplicated) random formulas that are generated is limited to 100000.
Therefore in some situations, most likely when generating small
formulas, with few atomic proposition, you may see =randltl= stop
before the requested number of formulas has been output with an error
message.

If the integer passed to =-n= is negative, =randltl= will attempt to
generate as many formulas as it can.  This is most useful when
=randltl= is piped to =ltlfilt= to select random formulas matching a
certain criterion, as we shall see later.

Besides the list of atomic propositions (=a b c= in our example) and
the seed, several other parameters control the generation of the
random formulas.

Initially, the random generator selects a tree size for the formula.
The default size is =15=, but it can be changed using the =--tree-size=
option.  For instance in the following, for each formula the tree size
will be chosen randomly in the range =22..30=.
#+BEGIN_SRC sh :results verbatim :exports both
randltl -n 5 a b c --tree-size=22..30
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124
: (((b xor c) xor (a U (Gc M c))) | (!b xor (a M b))) W (b & Fc)
125
: 0
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
127
128
: !((c xor Gb) -> !Fb) xor !(Gc M 1)
: 1
: (a | ((c | G(!a W (!a W b))) W (b & (c M b)))) <-> (b R c)
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149

The tree size is just the number of nodes in the syntax tree of the
formula during its construction.  However because Spot automatically
applies some /trivial simplifications/ during the construction of its
formulas (e.g., =F(F(a)= is reduced to =F(a)=, =a&0= to =0=, etc.),
the actual size of the formula output may be smaller than the
tree size specified.

It is pretty common to obtain the formulas =0= or =1= among the first
formulas output, since many random formulas trivially simplify to
these.  However because duplicate formulas are suppressed by default,
they shall only occur once.

Stronger simplifications may be requested using the =-r= option, that
implements many rewritings that helps Spot translators algorithms (so
beware that using =-r= reduces the randomness of the output).

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n 5 a b c --tree-size=22..30 -r
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
150
: 1
151
: 0
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
153
154
: ((G!b | (!c & F!b) | (c & Gb)) & GF!c) | (Fb & ((!c & Gb) | (c & F!b)) & FGc)
: (b R c) | (!a & ((!c & F(a & !b)) M (!c W !b)))
: XGa
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204

The generator build the syntax tree recursively from its root, by
considering all operators that could be used for a given tree size (for
example a tree-size of 2 disables binary operators).  A /priority/ is
associated to each operator, and the probability of this operator
being selected is this priority over the sum of the priorities of all
considered operators.  The default priorities for each operator can
be seen with =--dump-priorities=:

#+BEGIN_SRC sh :results verbatim :exports both
randltl a b c --dump-priorities
#+END_SRC
#+RESULTS:
#+begin_example
Use --ltl-priorities to set the following LTL priorities:
ap	3
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
#+end_example

Where =ap= stands for /atomic propositions/ (=a=, =b=, =c=).  In this
example, when the generator builds a leaf of the syntax tree (i.e., a
subformula of tree-size 1), it must ignore all operators, and chose
between =ap=, =false=, or =true=, and the odds of choosing =ap= is
3/(3+1+1).

As indicated at the top of the output, these priorities can be changed
using the =--ltl-priorities= options.  The most common scenario is to
disable some of the operators by giving them a null priority.  The
following example disables 6 operators, and augments the priority of
=U= to 3 to favor its occurrence.

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n 5 a b c --ltl-priorities 'xor=0,implies=0,equiv=0,W=0,M=0,X=0,U=3'
#+END_SRC
#+RESULTS:
: 1
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
205
206
207
208
: 1 U b
: 0
: F!((b U !a) U Gc)
: !b U G(b R c)
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225

When using =-r= to simplify generated formulas, beware that these
rewritings may use operators that you disabled during the initial
random generation: you may obtain a formula that uses =W= even if =W=
has a null priority.  (You can use =ltlfilt= to rewrite these
operators if that is a problem.)

If the =--weak-fairness= option is used, for each random formula
generated, a weak-fairness formula of the form =GF(a) & GF(b) & GF(c)=
is generated for a subset of the atomic propositions and "ANDed" to
the random formula.  The =--tree-size= option has no influence on the
weak-fairness formula appended.

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n 5 a b c --weak-fairness
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
226
227
228
229
230
: GFb
: ((b | XXa) M Ga) & GFa & GFc
: GFb & GFc & !(!((a U Gb) U b) U GFa)
: GFb & GFa & GFc & F(!X!b U (!c M 1))
: GFb & GFa & GFc & Xc
231
232
233
234
235
236
237
238


Boolean formulas may be output with the =-B= option:
#+BEGIN_SRC sh :results verbatim :exports both
randltl -B -n 5 a b c
#+END_SRC
#+RESULTS:
: !b
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
239
240
241
242
: b & !b
: b
: !c xor (!a xor b)
: !a -> (!c <-> (b xor !(a xor !b)))
243
244
245
246
247
248
249
250
251
252
253
254
255
256

In that case, priorities should be set with =--boolean-priorities=.

Finally, PSL formulas may be output using the =-P= option.  However
keep in mind that since LTL formulas are PSL formulas, generating
random PSL formula may produce many LTL formulas that do not use any
PSL operator (this is even more so the case when simplifications are
enabled with =-r=).

#+BEGIN_SRC sh :results verbatim :exports both
randltl -P -n 5 a b c
#+END_SRC
#+RESULTS:
: 1
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
257
258
259
260
: a R c
: F({[*0] | {{[*0] | a[*]}}[*]}[]-> 0)
: (a | ((a U c) M a)) M 1
: 0
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328

As shown with the =--dump-priorities= output below, tweaking the
priorities used to generated PSL formulas requires three different
options:

#+BEGIN_SRC sh :results verbatim :exports both
randltl -P a b c --dump-priorities
#+END_SRC
#+RESULTS:
#+begin_example
Use --ltl-priorities 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 --sere-priorities to set the following SERE priorities:
eword	1
boolform	1
star	1
star_b	1
and	1
andNLM	1
or	1
concat	1
fusion	1
Use --boolean-priorities 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
#+end_example

The =--ltl-priorities= option we have seen previously now recognize
some new PSL-specific operators: =Closure= is the ={sere}= operator,
=EConcat= is the ={sere}<>->f= operator, and =UConcat= is the
={sere}[]->f= operator.  When these operator are selected, they
require a SERE argument which is generated according to the priorities
set by =--sere-priorities=: =eword= is the empty word, =boolform= is a
Boolean formula (generated using the priorities set by
=--boolean-priorities=), =star= is the unbounded Kleen star, while
=star_b= is the bounded version, and =andNLM= is the
non-length-matching variant of the =and= operator.

#  LocalWords:  randltl num toc LTL PSL SRC Gb sed utf UTF lbt LBT's
#  LocalWords:  Xc GFb Gc Xb Fb XFb Xa dups ltlfilt Fc XXc GX GFc XG
#  LocalWords:  rewritings ltl ap GF ANDed GFa boolean EConcat eword
#  LocalWords:  UConcat boolform andNLM concat Kleen eval setenv setq
#  LocalWords:  getenv