tut01.org 11.9 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#+TITLE: Parsing and Printing LTL Formulas
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html

Our first task is to read formulas and print them in another syntax.

* Shell command

Using =ltlfilt=, you can easily read an LTL formula in one syntax, and
output it in another syntax.  By default the parser will accept a
formula in [[file:ioltl.org][any infix syntax]], but if the input is in the prefix syntax
of LBT, you should use [[file:ioltl.org][=--lbt-input=]].  The output syntax is controlled
using different options such as (=--spin=, =--lbt=, =--latex=, etc.).
Full parentheses can also be requested using =-p=.

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
18
19
20
21
ltlfilt -f '[]<>p0 || <>[]p1' --latex
formula='& & G p0 p1 p2'
ltlfilt --lbt-input -f "$formula" --lbt
ltlfilt --lbt-input -f "$formula" --spin -p
22
23
24
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
26
27
: \G \F p_{0} \lor \F \G p_{1}
: & & p1 p2 G p0
: (p1) && (p2) && ([](p0))
28
29
30

The reason the LBT parser has to be explicitly enabled is because of
some corner cases that have different meanings in the two syntaxes.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
31
32
(For instance =t= and =f= are the true constant in LBT's syntax, but
they are considered as atomic propositions in all the other syntaxes.)
33
34
35
36
37
38
39
40

* Python bindings

Here are the same operation in Python

#+BEGIN_SRC python :results output :exports both
import spot
f = spot.formula('[]<>p0 || <>[]p1')
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
41
42
print(f.to_str('latex'))
f = spot.formula('& & G p0 p1 p2')
43
44
45
46
47
print(f.to_str('lbt'))
print(f.to_str('spin', parenth=True))
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
49
50
: \G \F p_{0} \lor \F \G p_{1}
: & & p1 p2 G p0
: (p1) && (p2) && ([](p0))
51
52
53
54

The =spot.formula= function wraps the calls to the two formula parsers
of Spot.  It first tries to parse the formula using infix syntaxes,
and if it fails, it tries to parse it with the prefix parser.  (So
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55
this might fail to correctly interpret =t= or =f= if you are
56
57
58
59
60
61
62
63
64
65
66
67
68
69
processing a list of LBT formulas.)  Using =spot.formula=, parse
errors are returned as an exception.

* C++

** Simple wrapper for the two parsers

We first start with the easy parser interface, similar to the one used
above in the python bindings.  Here parse errors would be returned as
exceptions.

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <iostream>
  #include "ltlparse/public.hh"
70
  #include "ltlvisit/print.hh"
71
72
73

  int main()
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
75
    print_latex_psl(std::cout, spot::ltl::parse_formula("[]<>p0 || <>[]p1")) << '\n';
    const spot::ltl::formula* f = spot::ltl::parse_formula("& & G p0 p1 p2");
76
77
78
    print_lbt_ltl(std::cout, f) << '\n';
    print_spin_ltl(std::cout, f, true) << '\n';
    f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
79
    return 0;
80
81
82
83
  }
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84
85
86
: \G \F p_{0} \lor \F \G p_{1}
: & & p1 p2 G p0
: (p1) && (p2) && ([](p0))
87

88
Notice that the different output routines specify in their name the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
89
90
91
syntax the output, and the type of formula they can output.  Here we
are only using LTL formulas for demonstration, so those three
functions are OK with that.
92
93
94
95
96
97

Did you notice the calls to =f->destroy()= at the end?  The LTL
formula objects are implemented as DAG with sharing of subformulas.
Each (sub)formula is therefore reference counted, and currently this
is done manually by calling =f->clone()= and =f->destroy()= (do not
ever =delete= a formula, always call =f->destroy()=).
98
99
100
101
102
103
104
105
106
107
108

We do not recommend using this =parse_formula()= interface because of
the potential formulas (like =f= or =t=) that have different meanings
in the two parsers that are tried.

Instead, depending on whether you want to parse formulas with infix
syntax, or formulas with prefix syntax, you should call the specific
parser.  Additionally, this give you control over how to print errors.

** Calling the infix parser explicitly

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
110
Here is how to call the infix parser explicitly,:

111
112
113
114
#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
115
  #include "ltlvisit/print.hh"
116
117
118
119
120

  int main()
  {
    std::string input = "[]<>p0 || <>[]p1";
    spot::ltl::parse_error_list pel;
121
    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
122
123
124
125
126
127
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
      {
        if (f)
          f->destroy();
        return 1;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
    print_latex_psl(std::cout, f) << '\n';
129
    f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
130
    return 0;
131
132
133
134
  }
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
135
: \G \F p_{0} \lor \F \G p_{1}
136

137
138
139
140
141
142
143
So =parse_infix_psl()= processes =input=, and stores any diagnostic in
=pel=, which is a list of pairs associating each error to a location.
You could iterate over that list to print it by yourself as you wish,
or you can call =format_parse_errors()= to do that for you.  Note that
as its name implies, this parser can read more than LTL formulas (the
fragment of PSL we support is basically LTL extended with regular
expressions).
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

If =pel= is empty, =format_parse_errors()= will do nothing and return
false.

If =pel= is non empty, =format_parse_errors()= will display the errors
messages and return true.  In the above code, we have decided to
aborts the execution in this case.

However the parser usually tries to do some error recovery.  For
instance if you have input =(a U b))= the parser will complain about
the extra parenthesis (=pel= not empty), but it will still return an
=f= that is equivalent to =a U b=.  So you could decide to continue
with the "fixed" formula if you wish.  Here is an example:

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
162
  #include "ltlvisit/print.hh"
163
164
165
166
167

  int main()
  {
    std::string input = "(a U b))";
    spot::ltl::parse_error_list pel;
168
    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
169
170
171
172
173
    // Use std::cout instead of std::cerr because we can only
    // show the output of std::cout in this documentation.
    (void) spot::ltl::format_parse_errors(std::cout, input, pel);
    if (f == nullptr)
      return 1;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
174
    print_latex_psl(std::cout, f) << '\n';
175
    f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
176
    return 0;
177
178
179
180
  }
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
181
182
183
184
185
186
187
188
189
: >>> (a U b))
:            ^
: syntax error, unexpected closing parenthesis
:
: >>> (a U b))
:            ^
: ignoring trailing garbage
:
: a \U b
190
191
192
193
194
195
196


The formula =f= is only returned as null when the parser really cannot
recover anything.

** Calling the prefix parser explicitly

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
197
198
The only difference here is the call to =parse_prefix_ltl()= instead
of =parse_infix_psl()=.
199
200
201
202
203

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
204
  #include "ltlvisit/print.hh"
205
206
207
208
209

  int main()
  {
    std::string input = "& & G p0 p1 p2";
    spot::ltl::parse_error_list pel;
210
    const spot::ltl::formula* f = spot::ltl::parse_prefix_ltl(input, pel);
211
212
213
214
215
216
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
      {
        if (f)
          f->destroy();
        return 1;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
    print_lbt_ltl(std::cout, f) << '\n';
    print_spin_ltl(std::cout, f, true) << '\n';
    f->destroy();
    return 0;
  }
#+END_SRC

#+RESULTS:
: & & p1 p2 G p0
: (p1) && (p2) && ([](p0))


* Additional Comments

** PSL vs LTL

LTL is a subset of PSL as far as Spot is concerned, so you can parse
an LTL formula with =parse_infix_psl()=, and later print it with for
instance =print_spin_ltl()= (which, as its name implies, can only
print LTL formulas).  There is no =parse_infix_ltl()= function because
you can simply use =parse_infix_psl()= to parse LTL formulas.

There is a potential problem if you design a tool that only works with
LTL formulas, but call =parse_infix_psl()= to parse user input.  In
that case, the user might well input a PSL formula and cause problem
down the line.

For instance, let's see what happens if a PSL formulas is passed to
=print_spin_ltl=:

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
  #include "ltlvisit/print.hh"

  int main()
  {
    std::string input = "{a*;b}<>->(a U (b & GF c))";
    spot::ltl::parse_error_list pel;
    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
      {
        if (f)
          f->destroy();
        return 1;
      }
    print_spin_ltl(std::cout, f) << '\n';
265
    f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
266
    return 0;
267
268
269
270
  }
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
: {a[*];b}<>-> (a U (b && []<>c))

The output is a 'best effort' output.  The LTL subformulas have been
rewritten, but the PSL-specific part (the SERE and =<>->= operator)
are output in the only syntax Spot knows, definitively not
Spin-compatible.

If that is unwanted, here are two possible solutions.

The first is to simply diagnose non-LTL formulas.

#+BEGIN_SRC C++ :results verbatim :exports code
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
  #include "ltlvisit/print.hh"

  int main()
  {
    std::string input = "{a*;b}<>->(a U (b & GF c))";
    spot::ltl::parse_error_list pel;
    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
      {
        if (f)
          f->destroy();
        return 1;
      }
    if (!f->is_ltl_formula())
      {
        f->destroy();
        std::cerr << "Only LTL formulas are supported.\n";
        return 1;
      }
    print_spin_ltl(std::cout, f) << '\n';
    f->destroy();
    return 0;
  }
#+END_SRC

A second (but slightly weird) idea would be to try to simplify the PSL
formula, and hope that the PSL simplify is able to come up with an
equivalent LTL formula.  This does not always work, so you need to be
prepared to reject the formula any way.  In our example, we are lucky
(maybe because it was carefully chosen...):

#+BEGIN_SRC C++ :results verbatim :exports code
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
  #include "ltlvisit/print.hh"
  #include "ltlvisit/simplify.hh"

  int main()
  {
    std::string input = "{a*;b}<>->(a U (b & GF c))";
    spot::ltl::parse_error_list pel;
    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
      {
        if (f)
          f->destroy();
        return 1;
      }
    if (!f->is_ltl_formula())
      {
        spot::ltl::ltl_simplifier simp;
        const formula* g = simp.simplify(f);
        f->destroy();
        f = g;
      }
    if (!f->is_ltl_formula())
      {
        f->destroy();
        std::cerr << "Only LTL formulas are supported.\n";
        return 1;
      }
    print_spin_ltl(std::cout, f) << '\n';
    f->destroy();
    return 0;
  }
#+END_SRC

#+RESULTS:
: a U (b && (a U (b && []<>c)))

** Lenient parsing

In version 6, Spin extended its command-line LTL parser to accept
arbitrary atomic propositions to be specified.  For instance =(a > 4)
U (b < 5)= would be correct input, with =a > 4= and =b < 5= considered
as two atomic propositions.  Of course the atomic proposition could be
arbitrarily complex, and there is no way we can teach Spot about the
syntax for atomic propositions supported by any tool.  The usual
workaround in Spot is to double-quote any arbitrary atomic
proposition:

#+BEGIN_SRC sh :results verbatim :exports both
echo compare
ltlfilt -f '"a > 4" U "b < 5"'
echo and
ltlfilt -f '"a > 4" U "b < 5"' --spin
#+END_SRC

#+RESULTS:
: compare
: "a > 4" U "b < 5"
: and
: (a > 4) U (b < 5)

When the Spin output is requested, these atomic propositions are
atomically output in a way that Spin can parse.

This Spin syntax is not accepted by default by the infix parser, but
it has an option for that.  This is called /lenient parsing/: when the
parser finds a parenthetical block it does not understand, it simply
assume that this block represents an atomic proposition.

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --lenient -f '(a > 4) U (b < 5)'
#+END_SRC

#+RESULTS:
: "a > 4" U "b < 5"

Lenient parsing is risky, because any parenthesized sub-formula that
is a syntax-error will be treated as an atomic proposition:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --lenient -f '(a U ) U c'
#+END_SRC

#+RESULTS:
: "a U" U c

In C++ you can enable lenient using one of the Boolean arguments of
=parse_infix_psl()=.