tut20.org 7.5 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
2
#+TITLE: Converting a never claim into HOA
3
#+DESCRIPTION: Code example for parsing and printing ω-automata in Spot
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
5
#+HTML_LINK_UP: tut.html
6
7
8
#+PROPERTY: header-args:sh :results verbatim :exports both
#+PROPERTY: header-args:python :results output :exports both
#+PROPERTY: header-args:C+++ :results verbatim :exports both
9
10
11

The goal is to start from a never claim, as produced by Spin, e.g.:

12
13
14
#+BEGIN_SRC sh
  spin -f '[]<>foo U bar' > tut20.never
  cat tut20.never
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#+END_SRC

#+RESULTS:
#+begin_example
never  {    /* []<>foo U bar */
T0_init:
	do
	:: atomic { ((bar)) -> assert(!((bar))) }
	:: (1) -> goto T0_S53
	od;
accept_S42:
	do
	:: (1) -> goto T0_S42
	od;
T0_S42:
	do
	:: ((foo)) -> goto accept_S42
	:: (1) -> goto T0_S42
	od;
T0_S53:
	do
	:: (1) -> goto T0_S53
	:: ((bar) && (foo)) -> goto accept_S42
	:: ((bar)) -> goto T0_S42
	od;
accept_all:
	skip
}
#+end_example

and convert this into an automaton in [[file:hoa.org][the HOA format]].

Note that the automaton parser of Spot can read automata written
48
49
50
either as never claims, in LBTT's format, in ltl2dstar's format or in
the HOA format, and there is no need to specify which format you
expect.  Even if our example uses a never claim as input, the code we
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
51
write will read any of those formats.
52
53
54
55

* Shell

This is very simple: [[file:autfilt.org][=autfilt=]] can read automata in any of the
56
supported formats, and outputs it in the HOA format by default:
57

58
#+BEGIN_SRC sh :wrap SRC hoa
59
autfilt tut20.never
60
61
62
#+END_SRC

#+RESULTS:
63
#+begin_SRC hoa
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
HOA: v1
States: 5
Start: 0
AP: 2 "bar" "foo"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0] 1
[t] 2
State: 1 {0}
[t] 1
State: 2
[t] 2
[0&1] 3
[0] 4
State: 3 {0}
[t] 4
State: 4
[1] 3
[t] 4
--END--
87
#+end_SRC
88
89
90
91
92
93
94

* Python

Another one-liner.  The =spot.automaton()= function reads a single
automaton, and each automaton has a =to_str()= method that can print
in =hoa=, =lbtt=, =spin= (for never claim) or =dot=.

95
#+BEGIN_SRC python :wrap SRC hoa
96
97
98
99
100
import spot
print(spot.automaton('tut20.never').to_str('hoa'))
#+END_SRC

#+RESULTS:
101
#+begin_SRC hoa
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
HOA: v1
States: 5
Start: 0
AP: 2 "bar" "foo"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0] 1
[t] 2
State: 1 {0}
[t] 1
State: 2
[t] 2
[0&1] 3
[0] 4
State: 3 {0}
[t] 4
State: 4
[1] 3
[t] 4
--END--
125
#+end_SRC
126
127
128

* C++

129
Parsing an automaton is similar to [[file:tut01.org][parsing an LTL formula]].  The
130
131
132
=parse_aut()= function takes a filename and a BDD dictionary (to be
discussed later on this page).  It returns a shared pointer to a
structure that has a couple of important fields: =aborted= is a
133
Boolean telling if the input automaton was voluntarily aborted (a
134
135
136
137
138
feature of [[file:hoa.org][the HOA format]]), =errors= is a list of syntax errors that
occurred while parsing the automaton (printing these errors is up to
you), and =aut= is the actual automaton.  The parser usually tries to
recover from errors, so =aut= may not be null even if =errors= is
non-empty.
139

140
#+BEGIN_SRC C++ :wrap SRC hoa
141
142
  #include <string>
  #include <iostream>
143
144
  #include <spot/parseaut/public.hh>
  #include <spot/twaalgos/hoa.hh>
145
146
147
148

  int main()
  {
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
149
    spot::parsed_aut_ptr pa = parse_aut("tut20.never", dict);
150
    if (pa->format_errors(std::cerr))
151
152
153
      return 1;
    // This cannot occur when reading a never claim, but
    // it could while reading a HOA file.
154
    if (pa->aborted)
155
      {
156
        std::cerr << "--ABORT-- read\n";
157
158
        return 1;
      }
159
    spot::print_hoa(std::cout, pa->aut) << '\n';
160
161
162
163
164
    return 0;
  }
#+END_SRC

#+RESULTS:
165
#+begin_SRC hoa
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
HOA: v1
States: 5
Start: 0
AP: 2 "bar" "foo"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0] 1
[t] 2
State: 1 {0}
[t] 1
State: 2
[t] 2
[0&1] 3
[0] 4
State: 3 {0}
[t] 4
State: 4
[1] 3
[t] 4
--END--
189
#+end_SRC
190

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
191
192
193
194
195
196
197
198
199
200
201
202
In the Spot representation of automata, transitions guards are
represented by BDDs.  The role of the =bdd_dict= object is to keep
track of the correspondence between BDD variables and atomic
propositions such as =foo= and =bar= in the above example.  So each
automaton has a shared pointer to some =bdd_dict= (this shared pointer
is what the =bdd_dict_ptr= type is), and operations between automata
(like a product) can only work on automata that share the same
pointer.  Here, when we call the automaton parser, we supply the
=bdd_dict_ptr= that should be used to do the mapping between atomic
propositions and BDD variables.  Atomic propositions that were not
already registered will get a new BDD variable number, and while
existing atomic propositions will reuse the existing variable.
203
204
205
206
207
208
209
210
211
212
213
214
215

In the example for [[file:tut10.org][translating LTL into BA]], we did not specify any
=bdd_dict=, because the =translator= object will create a new one by
default.  However it is possible to supply such a =bdd_dict= to the
translator as well.  Similarly, in the Python bindings, there is a
global =bdd_dict= that is implicitly used for all operations, but it
can be specified if needed.

* Additional comments

There are actually different C++ interfaces to the automaton parser,
depending on your use case.  For instance the parser is able to read a
stream of automata stored in the same file, so that they could be
216
processed in a loop.  For this, you would instantiate a
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
217
218
219
220
221
222
=spot::automaton_stream_parser= object and call its =parse()= method
in a loop.  Each call to this method will either return one
=spot::parsed_aut_ptr=, or =nullptr= if there is no more automaton to
read.  The =parse_aut()= function is actually a simple convenience
wrapper that instantiates an =automaton_stream_parser= and calls its
=parse()= method once.
223
224
225
226
227


In Python, you can easily iterate over a file containing multiple
automata by doing:

228
#+BEGIN_SRC python :wrap SRC hoa
229
230
231
232
233
234
import spot
for aut in spot.automata('tut20.never'):
    print(aut.to_str('hoa'))
#+END_SRC

#+RESULTS:
235
#+begin_SRC hoa
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
HOA: v1
States: 5
Start: 0
AP: 2 "bar" "foo"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0] 1
[t] 2
State: 1 {0}
[t] 1
State: 2
[t] 2
[0&1] 3
[0] 4
State: 3 {0}
[t] 4
State: 4
[1] 3
[t] 4
--END--
259
#+end_SRC
260
261
262
263
264
265
266
267
268
269
270

In fact =spot.automaton()= is just a wrapper around =spot.automata()=
to return only the first automaton.

Still in Python, both =spot.automaton()= and =spot.automata()= can
accept three types of arguments:
- file names (such as in the above examples)
- commands that output automata on their standard output.  Those can
  be any shell expression, and must have '=|=' as their last
  character.  For instance here is how to convert Spin's output into
  LBTT's formula without using temporary files.
271
#+BEGIN_SRC python
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
import spot
print(spot.automaton('spin -f "[]<>p0" |').to_str('lbtt'))
#+END_SRC

#+RESULTS:
: 2 1
: 0 1 -1
: 1 p0
: 0 t
: -1
: 1 0 0 -1
: 0 t
: -1
:

- a string that includes new lines, in which case it is assumed
288
289
  to describe an automaton (or multiple automata) and is
  passed directly to the parser:
290

291
#+BEGIN_SRC python
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
import spot
print(spot.automaton("""
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 1 Inf(0)
--BODY--
State: 0
[0] 1
State: 1 {0}
[t] 1
--END--
""").to_str('spin'))
#+END_SRC

#+RESULTS:
: never {
: T0_init:
:   if
312
:   :: (a) -> goto accept_all
313
314
315
316
317
:   fi;
: accept_all:
:   skip
: }
:
318

319
#+BEGIN_SRC sh :results silent :exports results
320
321
rm -f tut20.never
#+END_SRC
322
323
324

#  LocalWords:  utf html args SRC init od LBTT's dstar's acc Buchi fi
#  LocalWords:  str lbtt aut BDDs bdd ptr nullptr