ltl2tgta.org 9.75 KB
Newer Older
1
#+TITLE: =ltl2tgta=
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
#+EMAIL: spot@lrde.epita.fr
3
#+OPTIONS: H:2 num:nil toc:t
4
#+LINK_UP: tools.html
5
6
7
8
9
10
11
12
13
14
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
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
205
206
207
208
209
210
211
212
213
214
215
216
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
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
329
330
331
332
333
334
335

This tool generates various form of Testing Automata, i.e., automata
that observe the /changes/ of atomic propositions, not their values.

Three types of automata can be output.  The only output format
supported currently is [[http://http://www.graphviz.org/][GraphViz]]'s format, with option =-8= to enable
UTF-8 characters as in other tools.

The =--ta= option will translate a formula into Testing Automaton, as
described by [[http://spinroot.com/spin/Workshops/ws06/039.pdf][Geldenhuys and Hansen (Spin'06)]].

Here is the output on =a U Gb= (we omit the call to =dot=, as shown while
discussing [[file:ltl2tgba.org][=ltl2tgba=]]).

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgta --ta --multiple-init 'a U Gb'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
  -1  [label="", style=invis, height=0]
  -1 -> 1 [label="a & b"]
  -2  [label="", style=invis, height=0]
  -2 -> 2 [label="a & !b"]
  -3  [label="", style=invis, height=0]
  -3 -> 3 [label="b & !a"]
  1 [label="0\na & b",shape=box]
  1 -> 3 [label="{a}\n"]
  1 -> 2 [label="{b}\n"]
  1 -> 4 [label="{a}\n"]
  2 [label="1\na & !b"]
  2 -> 1 [label="{b}\n"]
  2 -> 3 [label="{a, b}\n"]
  3 [label="2\nb & !a",shape=box]
  3 -> 4 [label="{a}\n"]
  4 [label="3",peripheries=2,shape=box]
  4 -> 4 [label="{a}\n{Acc[1]}"]
}
#+end_example

#+NAME: augb-ta
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgta --ta --multiple-init 'a U Gb' | sed 's/\\/\\\\/'
#+END_SRC
#+RESULTS: augb-ta
#+begin_example
digraph G {
  -1  [label="", style=invis, height=0]
  -1 -> 1 [label="a & !b"]
  -2  [label="", style=invis, height=0]
  -2 -> 2 [label="b & !a"]
  -3  [label="", style=invis, height=0]
  -3 -> 3 [label="a & b"]
  1 [label="2\\na & !b"]
  1 -> 3 [label="{b}\\n"]
  1 -> 2 [label="{a, b}\\n"]
  2 [label="0\\nb & !a",shape=box]
  2 -> 4 [label="{a}\\n"]
  3 [label="1\\na & b",shape=box]
  3 -> 2 [label="{a}\\n"]
  3 -> 1 [label="{b}\\n"]
  3 -> 4 [label="{a}\\n"]
  4 [label="3",peripheries=2,shape=box]
  4 -> 4 [label="{a}\\n{Acc[1]}"]
}
#+end_example

#+BEGIN_SRC dot :file augb-ta.png :cmdline -Tpng :var txt=augb-ta :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:augb-ta.png]]

As always, the labels of the states have no influence on the language
recognized by the automaton.  This automaton has three possible
initial states.  The initial state should be chosen depending on the
initial valuation of =a= and =b= in the system to be synchronized with
this testing automaton.  For instance if =a= is true and =b= false in
the initial state, the testing automaton should start in the state
pointed to by the initial arrow labeled =a & !b=.  In the rest of the
testing automaton, the transitions are labeled by the sets of atomic
propositions that should change in the system for the testing
automaton to progress.  States with a double enclosure are Büchi
accepting, meaning that any execution that visits one of these states
is accepting.  All states have an implicit self-loop labeled by ={}=:
if the system progress without changing the value of =a= and =b=, the
testing automaton remains in the same state.  Rectangle states are
livelock-accepting: any execution of the system that get stuck into
one of these state is accepting.

Without the =--multiple-init= option, a fake initial state is added.
This is the default since it often makes the result more readable.

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgta --ta 'a U Gb'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="b & !a\n"]
  1 -> 3 [label="a & b\n"]
  1 -> 4 [label="a & !b\n"]
  2 [label="2",shape=box]
  2 -> 5 [label="{a}\n"]
  3 [label="3",shape=box]
  3 -> 5 [label="{a}\n"]
  3 -> 2 [label="{a}\n"]
  3 -> 4 [label="{b}\n"]
  4 [label="1"]
  4 -> 3 [label="{b}\n"]
  4 -> 2 [label="{a, b}\n"]
  5 [label="4",peripheries=2,shape=box]
  5 -> 5 [label="{a}\n{Acc[1]}"]
}
#+end_example

#+NAME: augb-ta2
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgta --ta 'a U Gb' | sed 's/\\/\\\\/'
#+END_SRC
#+RESULTS: augb-ta2
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="b & !a\\n"]
  1 -> 3 [label="a & b\\n"]
  1 -> 4 [label="a & !b\\n"]
  2 [label="2",shape=box]
  2 -> 5 [label="{a}\\n"]
  3 [label="3",shape=box]
  3 -> 2 [label="{a}\\n"]
  3 -> 4 [label="{b}\\n"]
  3 -> 5 [label="{a}\\n"]
  4 [label="1"]
  4 -> 3 [label="{b}\\n"]
  4 -> 2 [label="{a, b}\\n"]
  5 [label="4",peripheries=2,shape=box]
  5 -> 5 [label="{a}\\n{Acc[1]}"]
}
#+end_example

#+BEGIN_SRC dot :file augb-ta2.png :cmdline -Tpng :var txt=augb-ta2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:augb-ta2.png]]

The =--gba= option can be used to request a Generalized Testing
Automaton, i.e., a Testing Automaton with Generalized Büchi
acceptance.  In that case double-enclosures are not used anymore, and
Büchi accepting transitions are marked with the same ={Acc[x],Acc[y]}=
notation used in TGBA.

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgta --gta 'GFa & GFb'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="a & b\n"]
  1 -> 3 [label="b & !a\n"]
  1 -> 4 [label="a & !b\n"]
  1 -> 5 [label="!b & !a\n"]
  2 [label="1",shape=box]
  2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"]
  2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"]
  2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"]
  3 [label="4"]
  3 -> 2 [label="{a}\n{Acc[b]}"]
  3 -> 4 [label="{a, b}\n{Acc[b]}"]
  3 -> 5 [label="{b}\n{Acc[b]}"]
  4 [label="2"]
  4 -> 2 [label="{b}\n{Acc[a]}"]
  4 -> 3 [label="{a, b}\n{Acc[a]}"]
  4 -> 5 [label="{a}\n{Acc[a]}"]
  5 [label="3"]
  5 -> 2 [label="{a, b}\n"]
  5 -> 3 [label="{b}\n"]
  5 -> 4 [label="{a}\n"]
}
#+end_example

#+NAME: gfagfb-gta
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgta --gta 'GFa & GFb' | sed 's/\\/\\\\/'
#+END_SRC
#+RESULTS: gfagfb-gta
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="a & b\\n"]
  1 -> 3 [label="b & !a\\n"]
  1 -> 4 [label="a & !b\\n"]
  1 -> 5 [label="!b & !a\\n"]
  2 [label="1",shape=box]
  2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"]
  2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"]
  2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"]
  3 [label="4"]
  3 -> 2 [label="{a}\\n{Acc[b]}"]
  3 -> 4 [label="{a, b}\\n{Acc[b]}"]
  3 -> 5 [label="{b}\\n{Acc[b]}"]
  4 [label="2"]
  4 -> 2 [label="{b}\\n{Acc[a]}"]
  4 -> 3 [label="{a, b}\\n{Acc[a]}"]
  4 -> 5 [label="{a}\\n{Acc[a]}"]
  5 [label="3"]
  5 -> 2 [label="{a, b}\\n"]
  5 -> 3 [label="{b}\\n"]
  5 -> 4 [label="{a}\\n"]
}
#+end_example

#+BEGIN_SRC dot :file gfagfb-gta.png :cmdline -Tpng :var txt=gfagfb-gta :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:gfagfb-gta.png]]

The interpretation is similar to that of the TA.  Execution that
stutter in a livelock-accepting (square) state are accepting as well
as execution that visit the =Acc[a]= and =Acc[b]= acceptance sets
infinitely often.  Those acceptance sets are carried by transitions,
as in TGBAs.

Finally, the default is to output a Transition-based Generalized
Testing Automaton [fn:topnoc].  In TGTAs, the stuttering states are
made explicit with ={}= self-loops.  Since these self-loop can be in
acceptance sets, livelock acceptance states are no longer needed.

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgta 'GFa & GFb'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="a & b\n"]
  1 -> 3 [label="b & !a\n"]
  1 -> 4 [label="a & !b\n"]
  1 -> 5 [label="!b & !a\n"]
  2 [label="3"]
  2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"]
  2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"]
  2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"]
  2 -> 2 [label="{}\n{Acc[b], Acc[a]}"]
  3 [label="4"]
  3 -> 2 [label="{a}\n{Acc[b]}"]
  3 -> 4 [label="{a, b}\n{Acc[b]}"]
  3 -> 5 [label="{b}\n{Acc[b]}"]
  3 -> 3 [label="{}\n"]
  4 [label="2"]
  4 -> 2 [label="{b}\n{Acc[a]}"]
  4 -> 3 [label="{a, b}\n{Acc[a]}"]
  4 -> 5 [label="{a}\n{Acc[a]}"]
  4 -> 4 [label="{}\n"]
  5 [label="1"]
  5 -> 2 [label="{a, b}\n"]
  5 -> 3 [label="{b}\n"]
  5 -> 4 [label="{a}\n"]
  5 -> 5 [label="{}\n"]
}
#+end_example

#+NAME: gfagfb-tgta
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgta 'GFa & GFb' | sed 's/\\/\\\\/'
#+END_SRC
#+RESULTS: gfagfb-tgta
#+begin_example
digraph G {
  0 [label="", style=invis, height=0]
  0 -> 1
  1 [label=init]
  1 -> 2 [label="a & b\\n"]
  1 -> 3 [label="b & !a\\n"]
  1 -> 4 [label="a & !b\\n"]
  1 -> 5 [label="!b & !a\\n"]
  2 [label="1"]
  2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"]
  2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"]
  2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"]
  2 -> 2 [label="{}\\n{Acc[b], Acc[a]}"]
  3 [label="4"]
  3 -> 2 [label="{a}\\n{Acc[b]}"]
  3 -> 4 [label="{a, b}\\n{Acc[b]}"]
  3 -> 5 [label="{b}\\n{Acc[b]}"]
  3 -> 3 [label="{}\\n"]
  4 [label="3"]
  4 -> 2 [label="{b}\\n{Acc[a]}"]
  4 -> 3 [label="{a, b}\\n{Acc[a]}"]
  4 -> 5 [label="{a}\\n{Acc[a]}"]
  4 -> 4 [label="{}\\n"]
  5 [label="2"]
  5 -> 2 [label="{a, b}\\n"]
  5 -> 3 [label="{b}\\n"]
  5 -> 4 [label="{a}\\n"]
  5 -> 5 [label="{}\\n"]
}
#+end_example

#+BEGIN_SRC dot :file gfagfb-tgta.png :cmdline -Tpng :var txt=gfagfb-tgta :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:gfagfb-tgta.png]]


[fn:topnoc]: This new class of automaton, as well as the
implementation of the previous testing automata classes, is part of
Ala Eddine BEN SALEM's PhD work, and should appear in a future edition
of ToPNoC (LNCS 7400).


#  LocalWords:  ltl tgta num toc Automata automata GraphViz UTF Gb na
#  LocalWords:  Geldenhuys tgba SRC init invis nb Acc augb sed png fn
#  LocalWords:  cmdline Tpng txt Büchi livelock gba gta GFa GFb TGTAs
#  LocalWords:  gfagfb topnoc Eddine SALEM's ToPNoC LNCS eval setenv
#  LocalWords:  concat getenv setq