2402d721a9
* doc/org/spot2.svg: New file. * doc/Makefile.am: Distribute it. * doc/org/.gitignore: Adjust. * doc/org/setup.org: Display it. * doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org, doc/org/upgrade2.org: Include setup.org instead of declaring it as SETUPFILE. * doc/org/spot.css: Add entries for the logo. * python/ajax/trans.html: Use the new logo. * python/ajax/logos/mail.png, python/ajax/logos/spot64s.png: Delete. * python/ajax/Makefile.am: Adjust.
478 lines
20 KiB
Org Mode
478 lines
20 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: =autcross=
|
|
#+DESCRIPTION: Spot command-line tool for cross-comparing the output of automaton processors.
|
|
#+INCLUDE: 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
|
|
: %M, %[val]M the name of the input automaton, with an optional
|
|
: default value
|
|
: %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 =-= indicates 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 silent :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
|
|
allowed unless =--fail-on-timeout= is also given.
|
|
|
|
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
|
|
are not considered to be errors and therefore not reported in this
|
|
file, unless =--fail-on-timeout= is given.
|
|
|
|
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
|
|
* Use-cases for =%M=
|
|
|
|
If the input automata are named, it is possible to use =%M= in some
|
|
tool specification to pass this name to the tool. In particular, this
|
|
can be used to replace the input automaton by something else.
|
|
|
|
For instance if the name of the automaton is an actual LTL formula
|
|
(automata produced by [[file:ltl2tgba.org][=ltl2tgba=]] follow this convention), you can
|
|
cross-compare some tool that input that formula instead of the
|
|
automaton. For instance consider the following command-line, where we
|
|
compare the determinization of =autfilt -D= (starting from an
|
|
automaton) to the determinization of =ltl2dstar= (starting from the
|
|
LTL formula encoded in the name of the automaton). That LTL formula
|
|
is not in a syntax supported by =ltl2dstar=, so we call =ltl2dstar=
|
|
via [[file:ltldo.org][=ltldo=]] to arrange that.
|
|
|
|
#+BEGIN_SRC sh :results silent :export code
|
|
genltl --eh-patterns=1..3 | ltl2tgba |
|
|
autcross 'autfilt -P -D' 'ltldo ltl2dstar -f %M >%O'
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC sh :results verbatim :export results
|
|
genltl --eh-patterns=1..3 | ltl2tgba |
|
|
autcross 'autfilt -P -D' 'ltldo ltl2dstar -f %M >%O' 2>&1
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
#+begin_example
|
|
-:1.1-16.7 p0 U (p1 & Gp2)
|
|
Running [A0]: autfilt -P -D 'lcr-i0-rBSCo9'>'lcr-o0-xyRJhy'
|
|
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & Gp2)' >'lcr-o1-9uDUjX'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
-:17.1-34.7 p0 U (p1 & X(p2 U p3))
|
|
Running [A0]: autfilt -P -D 'lcr-i1-LFDrvm'>'lcr-o0-6fBZGL'
|
|
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 U p3))' >'lcr-o1-AUXx0a'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
-:35.1-64.7 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
|
|
Running [A0]: autfilt -P -D 'lcr-i2-UaZCtA'>'lcr-o0-hhbJWZ'
|
|
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))' >'lcr-o1-xhS4Ap'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
No problem detected.
|
|
#+end_example
|
|
|
|
This example is a bit contrived, and in this case, an alternative would
|
|
be to use [[file:ltlcross.org][=ltlcross=]], as in:
|
|
|
|
#+BEGIN_SRC sh :results silent :export code
|
|
genltl --eh-patterns=1..3 |
|
|
ltlcross 'ltl2tgba %f | autfilt -P -D > %O' 'ltl2dstar'
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC sh :results verbatim :export results
|
|
genltl --eh-patterns=1..3 |
|
|
ltlcross 'ltl2tgba %f | autfilt -P -D > %O' 'ltl2dstar' 2>&1
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
#+begin_example
|
|
-:1: (p0) U ((p1) & (G(p2)))
|
|
Running [P0]: ltl2tgba '(p0) U ((p1) & (G(p2)))' | autfilt -P -D > 'lcr-o0-DnV1rm'
|
|
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i0-jBLulv' 'lcr-o1-epwYeE'
|
|
Running [N0]: ltl2tgba '!((p0) U ((p1) & (G(p2))))' | autfilt -P -D > 'lcr-o0-8bVQ9M'
|
|
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i0-5oAAdW' 'lcr-o1-W7elh5'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
-:2: (p0) U ((p1) & (X((p2) U (p3))))
|
|
Running [P0]: ltl2tgba '(p0) U ((p1) & (X((p2) U (p3))))' | autfilt -P -D > 'lcr-o0-xMdCve'
|
|
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i1-OJU1Sn' 'lcr-o1-wOCsgx'
|
|
Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) U (p3)))))' | autfilt -P -D > 'lcr-o0-SzgmFG'
|
|
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i1-8iIddQ' 'lcr-o1-zBV5KZ'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
-:3: (p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6))))))))))))))
|
|
Running [P0]: ltl2tgba '(p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6))))))))))))))' | autfilt -P -D > 'lcr-o0-FEA6s9'
|
|
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i2-E0Ikpj' 'lcr-o1-ppDzlt'
|
|
Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6)))))))))))))))' | autfilt -P -D > 'lcr-o0-jqlelD'
|
|
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i2-IwU1uN' 'lcr-o1-6YdQEX'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
No problem detected.
|
|
#+end_example
|
|
|
|
However in practice you could also use the =name:= field of the input
|
|
automaton, combined with =%M= in the tool specification, to designate
|
|
an alternate filename to load, or some key to look up somewhere.
|