ltl2tgta.org 9.41 KB
Newer Older
1
#+TITLE: =ltl2tgta=
2 3
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

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]
25
  -1 -> 1 [label="!a & b"]
26
  -2  [label="", style=invis, height=0]
27
  -2 -> 2 [label="a & b"]
28
  -3  [label="", style=invis, height=0]
29 30
  -3 -> 3 [label="a & !b"]
  1 [label="2\n!a & b",shape=box]
31
  1 -> 4 [label="{a}\n"]
32 33 34 35 36 37 38
  2 [label="1\na & b",shape=box]
  2 -> 4 [label="{a}\n"]
  2 -> 1 [label="{a}\n"]
  2 -> 3 [label="{b}\n"]
  3 [label="0\na & !b"]
  3 -> 2 [label="{b}\n"]
  3 -> 1 [label="{a, b}\n"]
39
  4 [label="3",peripheries=2,shape=box]
40
  4 -> 4 [label="{a}\n{0}"]
41 42 43 44 45 46 47 48 49 50 51
}
#+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]
52
  -1 -> 1 [label="!a & b"]
53
  -2  [label="", style=invis, height=0]
54
  -2 -> 2 [label="a & b"]
55
  -3  [label="", style=invis, height=0]
56 57 58 59
  -3 -> 3 [label="a & !b"]
  1 [label="2\\n!a & b",shape=box]
  1 -> 4 [label="{a}\\n"]
  2 [label="1\\na & b",shape=box]
60
  2 -> 4 [label="{a}\\n"]
61 62 63 64 65
  2 -> 1 [label="{a}\\n"]
  2 -> 3 [label="{b}\\n"]
  3 [label="0\\na & !b"]
  3 -> 2 [label="{b}\\n"]
  3 -> 1 [label="{a, b}\\n"]
66
  4 [label="3",peripheries=2,shape=box]
67
  4 -> 4 [label="{a}\\n{0}"]
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
}
#+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]
106
  1 -> 2 [label="!a & b\n"]
107 108 109 110 111 112 113 114 115 116 117 118
  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]
119
  5 -> 5 [label="{a}\n{0}"]
120 121 122 123 124 125 126 127 128 129 130 131 132
}
#+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]
133
  1 -> 2 [label="!a & b\\n"]
134 135 136 137 138
  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]
139
  3 -> 5 [label="{a}\\n"]
140 141 142 143 144 145
  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]
146
  5 -> 5 [label="{a}\\n{0}"]
147 148 149 150 151 152 153 154 155 156 157 158
}
#+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
159
Büchi accepting transitions are marked with the same ={0,1}=
160 161 162 163 164 165 166 167 168 169 170 171
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"]
172
  1 -> 3 [label="!a & b\n"]
173
  1 -> 4 [label="a & !b\n"]
174
  1 -> 5 [label="!a & !b\n"]
175
  2 [label="1",shape=box]
176 177 178 179 180 181 182
  2 -> 3 [label="{a}\n{0,1}"]
  2 -> 4 [label="{b}\n{0,1}"]
  2 -> 5 [label="{a, b}\n{0,1}"]
  3 [label="3"]
  3 -> 2 [label="{a}\n{1}"]
  3 -> 4 [label="{a, b}\n{1}"]
  3 -> 5 [label="{b}\n{1}"]
183
  4 [label="2"]
184 185 186 187
  4 -> 2 [label="{b}\n{0}"]
  4 -> 3 [label="{a, b}\n{0}"]
  4 -> 5 [label="{a}\n{0}"]
  5 [label="4"]
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
  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"]
205
  1 -> 3 [label="!a & b\\n"]
206
  1 -> 4 [label="a & !b\\n"]
207
  1 -> 5 [label="!a & !b\\n"]
208
  2 [label="1",shape=box]
209 210 211 212 213 214 215
  2 -> 3 [label="{a}\\n{0,1}"]
  2 -> 4 [label="{b}\\n{0,1}"]
  2 -> 5 [label="{a, b}\\n{0,1}"]
  3 [label="3"]
  3 -> 2 [label="{a}\\n{1}"]
  3 -> 4 [label="{a, b}\\n{1}"]
  3 -> 5 [label="{b}\\n{1}"]
216
  4 [label="2"]
217 218 219 220
  4 -> 2 [label="{b}\\n{0}"]
  4 -> 3 [label="{a, b}\\n{0}"]
  4 -> 5 [label="{a}\\n{0}"]
  5 [label="4"]
221 222 223 224 225 226 227 228 229 230 231 232 233 234
  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
235
as execution that visit the =0= and =1= acceptance sets
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
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"]
254
  1 -> 3 [label="!a & b\n"]
255
  1 -> 4 [label="a & !b\n"]
256
  1 -> 5 [label="!a & !b\n"]
257
  2 [label="3"]
258 259 260 261 262 263 264 265
  2 -> 3 [label="{a}\n{0,1}"]
  2 -> 4 [label="{b}\n{0,1}"]
  2 -> 5 [label="{a, b}\n{0,1}"]
  2 -> 2 [label="{}\n{0,1}"]
  3 [label="2"]
  3 -> 2 [label="{a}\n{1}"]
  3 -> 4 [label="{a, b}\n{1}"]
  3 -> 5 [label="{b}\n{1}"]
266
  3 -> 3 [label="{}\n"]
267 268 269 270
  4 [label="4"]
  4 -> 2 [label="{b}\n{0}"]
  4 -> 3 [label="{a, b}\n{0}"]
  4 -> 5 [label="{a}\n{0}"]
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
  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"]
291
  1 -> 3 [label="!a & b\\n"]
292
  1 -> 4 [label="a & !b\\n"]
293 294 295 296 297 298 299 300 301 302
  1 -> 5 [label="!a & !b\\n"]
  2 [label="3"]
  2 -> 3 [label="{a}\\n{0,1}"]
  2 -> 4 [label="{b}\\n{0,1}"]
  2 -> 5 [label="{a, b}\\n{0,1}"]
  2 -> 2 [label="{}\\n{0,1}"]
  3 [label="2"]
  3 -> 2 [label="{a}\\n{1}"]
  3 -> 4 [label="{a, b}\\n{1}"]
  3 -> 5 [label="{b}\\n{1}"]
303
  3 -> 3 [label="{}\\n"]
304 305 306 307
  4 [label="4"]
  4 -> 2 [label="{b}\\n{0}"]
  4 -> 3 [label="{a, b}\\n{0}"]
  4 -> 5 [label="{a}\\n{0}"]
308
  4 -> 4 [label="{}\\n"]
309
  5 [label="1"]
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
  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