autcross.org 16.3 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1 2 3 4 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
# -*- coding: utf-8 -*-
#+TITLE: =autcross=
#+DESCRIPTION: Spot command-line tool for cross-comparing the output of automaton processors.
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html

=autcross= is a tool for cross-comparing the output of tools that
transform automata.   It works similarly to [[file:ltlcross.org][=ltlcross=]] except that
inputs are automata.

The core of =autcross= is a loop that does the following steps:
  - Input an automaton
  - Process that input automaton with all the configured tools.
    If there are 3 translators, the automata produced by those tools
    will be named =A0=, =A1=, and =A2=.
  - Ensure that all produced automata are equivalent.

Statistics about the results of each tools can optionally be saved in
a CSV file.  And in case only those statistics matters, it is also
possible to disable the equivalence checks.

* Input automata

The input automata can be supplied either on standard input, or in
files specified with option =-F=.

If an input automaton is expressed in the HOA format and has a name,
that name will be displayed by =autcross= when processing the automaton,
and will appear in the CSV file if such a file is output.

* Specifying the tools to test

Each tool should be specified as a string that uses some of the
following character sequences:

#+BEGIN_SRC sh :results verbatim :exports results
  autcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
:   %%                         a single %
:   %H,%S,%L                   filename for the input automaton in (H) HOA, (S)
:                              Spin's neverclaim, or (L) LBTT's format
:   %O                         filename for the automaton output in HOA, never
:                              claim, LBTT, or ltl2dstar's format

For instance we can use =autfilt --complement %H >%O= to indicate that
=autfilt= reads one file (=%H=) in the HOA format, and to redirect the
output in file so that =autcross= can find it.  The output format is
automatically detected, so a generic =%O= is used for the output file
regardless of its format.

Another tool that can complement automata is =ltl2dstar=, using
the syntax =ltl2dstar -B --complement-input=yes %H %O=.  So to
compare the results of these two tools we could use:

#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b |
autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O'
#+END_SRC

#+BEGIN_SRC sh :results verbatim :exports output
randaut -B -n 3 a b |
autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O' 2>&1
#+END_SRC

#+RESULTS:
#+begin_example
-:1.1-45.7
Running [A0]: autfilt --complement 'lcr-i0-Nr1xZO' >'lcr-o0-urHakt'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i0-mmkgH7' 'lcr-o1-ABdm4L'
Performing sanity checks and gathering statistics...

-:46.1-92.7
Running [A0]: autfilt --complement 'lcr-i1-5kMYrq' >'lcr-o0-9kvBP4'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i1-lVlGfJ' 'lcr-o1-BexLFn'
Performing sanity checks and gathering statistics...

-:93.1-137.7
Running [A0]: autfilt --complement 'lcr-i2-rjvy61' >'lcr-o0-rKKlxG'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i2-Musr0k' 'lcr-o1-LyAxtZ'
Performing sanity checks and gathering statistics...

No problem detected.
#+end_example

In this example, we generate 3 random Büchi automata (because
=ltl2dstar= expects Büchi automata as input) using [[file:randaut.org][=randaut=]], and pipe
them to =autcross=.  For each of those automata, =autcross= display
the source location of that automaton (here =-= indicate that the
automaton is read from standard input, and this is followed by
=beginline.column-endline.colum= specifying the position of that
automaton in the input.   If the automata had names, they would
be displayed as well.

Then, each tool is called using temporary files to exchange the
automata, and the resulting automata are then compared.  The last line
specifies that no problem was detected.


To simplify the use of some known tools, a set of predefined
shorthands are available.  Those can be listed with the
=--list-shorthands= option.

#+BEGIN_SRC sh :results verbatim :exports both
autcross --list-shorthands
#+END_SRC
#+RESULTS:
#+begin_example
If a COMMANDFMT does not use any %-sequence, and starts with one of
the following words, then the string on the right is appended.

  autfilt      %H>%O
  seminator    %H>%O
  ltl2dstar    -B %H %O
  nba2ldpa     <%H>%O

Any {name} and directory component is skipped for the purpose of
matching those prefixes.  So for instance
  '{AF} ~/mytools/autfilt-2.4 --remove-fin'
will be changed into
  '{AF} ~/mytools/autfilt-2.4 --remove-fin %H>%O'
#+end_example

What this implies is our previous example could be shortened to:

#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes'
#+END_SRC

* Getting statistics

Detailed statistics about the result of each translation, and the
product of that resulting automaton with the random state-space, can
be obtained using the =--csv=FILE= option.

** CSV output

Let's take our example and modify it in two ways.  First we pass a
=--name= option to =randaut= to give each automaton a name (in
=randaut=, =%L= denotes the serial number of the automaton); this is
mostly a cosmetic change, so that =autcross= will display names.
Second, we pass a =--csv= option to =autcross= to save statistics in a
file.


#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv
#+END_SRC

#+BEGIN_SRC sh :results verbatim :exports results
randaut -B -n 3 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv 2>&1
#+END_SRC

#+RESULTS:
#+begin_example
-:1.1-46.7	automaton 0
Running [A0]: autfilt --complement 'lcr-i0-QHReWu'>'lcr-o0-0eTOmZ'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-jsoPPt' 'lcr-o1-66bQiY'
Performing sanity checks and gathering statistics...

-:47.1-94.7	automaton 1
Running [A0]: autfilt --complement 'lcr-i1-IubpMs'>'lcr-o0-dfmYfX'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i1-13NXLr' 'lcr-o1-zSwXhW'
Performing sanity checks and gathering statistics...

-:95.1-140.7	automaton 2
Running [A0]: autfilt --complement 'lcr-i2-g5bDOq'>'lcr-o0-X71ilV'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i2-og1mUp' 'lcr-o1-QVurtU'
Performing sanity checks and gathering statistics...

No problem detected.
#+end_example

After this execution, the file =autcross.csv= contains the following:

#+BEGIN_SRC sh :results verbatim :exports results
cat autcross.csv
#+END_SRC
#+RESULTS:
: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating"
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"autfilt --complement","ok",0,0.0129685,2,27,95,108,3,2,0,0,0
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00202496,2,34,121,136,6,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"autfilt --complement","ok",0,0.0128458,2,58,216,232,3,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"ltl2dstar --complement-input=yes","ok",0,0.0026184,2,74,268,296,6,2,0,8,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"autfilt --complement","ok",0,0.0127144,2,21,69,84,2,4,0,20,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00180888,2,24,74,96,2,4,0,35,0

This file can then be loaded in any spreadsheet or statistical application.

When computing such statistics, you should be aware that inputs for
which a tool failed to generate an automaton (e.g. it crashed, or it
was killed if you used =autcross='s =--timeout= option to limit run
time) will appear with empty columns at the end of the CSV line.
Those lines with missing data can be omitted with the =--omit-missing=
option.

However data for bogus automata are still included: as shown below
=autcross= will report inconsistencies between automata as errors, but
it does not try to guess who is incorrect.

The column names should be almost self-explanatory.  See the [[./man/autcross.1.html][man page]]
for a description of the columns.

** Changing the name of the translators

By default, the names used in the CSV output to designate the
tools are the command specified on the command line.  Like with
=ltlcross=, this can be adjusted by using a command specification of
the form ={short name}actual command=.

For instance

#+BEGIN_SRC sh :results verbatim :exports both
randaut -B -n 3 a b --name="automaton %L" |
autcross '{AF}autfilt --complement' '{L2D}ltl2dstar --complement-input=yes' --csv
#+END_SRC

#+RESULTS:
: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating"
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"AF","ok",0,0.039722,2,27,95,108,3,2,0,0,0
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"L2D","ok",0,0.00640371,2,34,121,136,6,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"AF","ok",0,0.0400776,2,58,216,232,3,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"L2D","ok",0,0.00489558,2,74,268,296,6,2,0,20,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"AF","ok",0,0.0220585,2,21,69,84,2,4,0,7,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"L2D","ok",0,0.00329786,2,24,74,96,2,4,0,23,0

* Language preserving transformation

By default =autcross= assumes that for a given input the automata
produced by all tools should be equivalent.  However it does not
assume that those language should be equivalent to the input (it is
clearly not the case in our complementation test above).

If the transformation being tested does preserve the language of an
automaton, it is worth to pass the =--language-preserved= option to
=autfilt=.  Doing so a bit like adding =cat %H>%O= as another tool: it
will also ensure that the output is equivalent to the input.

* Detecting problems
   :PROPERTIES:
   :CUSTOM_ID: checks
   :END:

If a translator exits with a non-zero status code, or fails to output
an automaton =autcross= can read, and error will be displayed and the
result of the tool will be discarded.

Otherwise =autcross= performs equivalence checks between each pair of
automata.   This is done in two steps.  First, all produced automata
=A0=, =A1=, etc. are complemented: the complement automata are
named =Comp(A0)=, =Comp(A1)= etc.  Second, =autcross= ensures
that =Ai*Comp(Aj)= is empty for all =i= and =j=.

If the =--language-preserved= option is passed, the =input= automaton
also participate to these equivalence checks.


To simulate a problem, let's compare pretend we want verify that
=autfilt --complement= preserves the input language (clearly it does
not, since it actually complement the language of the automaton).

#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b --name="automaton %L" |
autcross --language-preserved 'autfilt --complement'
#+END_SRC

#+BEGIN_SRC sh :results verbatim :exports output
randaut -B -n 3 a b --name="automaton %L" |
autcross --language-preserved 'autfilt --complement' 2>&1
#+END_SRC

#+RESULTS:
#+begin_example
-:1.1-46.7	automaton 0
Running [A0]: autfilt --complement 'lcr-i0-3gRqrd'>'lcr-o0-ubUpHb'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
       !a & !b; a & !b; cycle{!a & !b; a & !b; !a & b; !a & b; !a & !b; !a & b; !a & b; !a & !b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
       !a & !b; !a & !b; cycle{!a & !b; !a & b; a & b}

-:47.1-94.7	automaton 1
Running [A0]: autfilt --complement 'lcr-i1-JxFi09'>'lcr-o0-oQGbj8'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
       !a & b; cycle{a & !b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
       !a & b; a & !b; cycle{!a & b; a & b}

-:95.1-140.7	automaton 2
Running [A0]: autfilt --complement 'lcr-i2-SQT7E6'>'lcr-o0-kWt404'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
       a & !b; !a & !b; cycle{a & !b; !a & b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
       cycle{!a & b; !a & b; !a & !b; a & !b; a & !b; !a & !b}

error: some error was detected during the above runs,
       please search for 'error:' messages in the above trace.
#+end_example

Here, for each automaton, we get an example of word that is accepted
by the automaton and rejected by the input (i.e., accepted by
=Comp(input)=), as well as an example of word accepted by the input
but rejected by the automaton (i.e. accepted by =Comp(A0)=).  Those
examples would not exit if the language was really preserved by the
tool.

Incoherence between the output of several tools (even with
=--language-preserved=) are reported in a similar way.

* Miscellaneous options

** =--stop-on-error=

The =--stop-on-error= option will cause =autcross= to abort on the
first detected error.  This include failure to start some tool,
read its output, or failure to passe the sanity checks.  Timeouts are
322
allowed unless =--fail-on-timeout= is also given.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
323 324 325 326 327 328 329 330 331

One use for this option is when =autcross= is used in combination with
=randaut= to check tools on an infinite stream of formulas.

** =--save-bogus=FILENAME=

The =--save-bogus=FILENAME= will save any automaton for which an error
was detected (either some tool failed, or some problem was
detected using the resulting automata) in =FILENAME=.  Again, timeouts
332 333
are not considered to be errors and therefore not reported in this
file, unless =--fail-on-timeout= is given.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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

The main use for this feature is in conjunction with =randaut='s
generation of random formulas.  For instance the following command
will run the translators on an infinite number of formulas, saving
any problematic formula in =bugs.ltl=.

** =--no-check=

The =--no-check= option disables all sanity checks.  This
makes sense if you only care about the output of =--csv=.

** =--verbose=

The verbose option can be useful to troubleshoot problems or simply
follow the list of transformations and tests performed by =autcross=.

#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 1 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose
#+END_SRC

#+BEGIN_SRC sh :results verbatim :exports results
randaut -B -n 1 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose 2>&1
#+END_SRC

#+RESULTS:
#+begin_example
-:1.1-46.7	automaton 0
info: input	(10 st.,26 ed.,1 sets)
Running [A0]: autfilt --complement 'lcr-i0-oZm5P2'>'lcr-o0-O4P0IB'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-gEwlJa' 'lcr-o1-wSaHJJ'
info: collected automata:
info:   A0	(27 st.,95 ed.,3 sets) deterministic complete
info:   A1	(34 st.,121 ed.,6 sets) deterministic complete
Performing sanity checks and gathering statistics...
info: getting rid of any Fin acceptance...
info:         A0	(27 st.,95 ed.,3 sets) -> (58 st.,203 ed.,2 sets)
info:   Comp(A0)	(27 st.,95 ed.,3 sets) -> (51 st.,188 ed.,1 sets)
info:         A1	(34 st.,121 ed.,6 sets) -> (64 st.,228 ed.,3 sets)
info:   Comp(A1)	(34 st.,121 ed.,6 sets) -> (34 st.,121 ed.,1 sets)
info: check_empty A0*Comp(A1)
info: check_empty A1*Comp(A0)

No problem detected.
#+end_example

#  LocalWords:  utf autcross SETUPFILE html HOA neverclaim dstar's Nr
#  LocalWords:  autfilt dstar randaut lcr xZO urHakt mmkgH ABdm kMYrq
#  LocalWords:  kvBP lVlGfJ BexLFn rjvy rKKlxG Musr LyAxtZ shorthands
#  LocalWords:  COMMANDFMT seminator nba ldpa QHReWu eTOmZ jsoPPt ilV
#  LocalWords:  bQiY IubpMs dfmYfX NXLr zSwXhW bDOq og mUp QVurtU ap
#  LocalWords:  ok complementation Ai Aj gRqrd ubUpHb JxFi oQGbj SQT
#  LocalWords:  kWt Eo Xsc WXgCB vLwKMQ tI SXF qqlE KXplk ZFTCz PNY
#  LocalWords:  hUAK IjnFhD cWys ZqjdQh