autcross

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.

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

%%                         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:

randaut -B -n 3 a b |
autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O'

-:1.1-45.7
Running [A0]: autfilt --complement 'lcr-i0-30Pwre' >'lcr-o0-J4iXOS'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-btz3Tp' 'lcr-o1-zqMBx5'
Performing sanity checks and gathering statistics...

-:46.1-92.7
Running [A0]: autfilt --complement 'lcr-i1-3gpn9x' >'lcr-o0-TV6UUa'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i1-2BnXDU' 'lcr-o1-wfvZrE'
Performing sanity checks and gathering statistics...

-:93.1-137.7
Running [A0]: autfilt --complement 'lcr-i2-nx6UKh' >'lcr-o0-zrjvgP'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i2-LpRslA' 'lcr-o1-qrbcXJ'
Performing sanity checks and gathering statistics...

No problem detected.

In this example, we generate 3 random Büchi automata (because ltl2dstar expects Büchi automata as input) using randaut, and pipe them to autcross. For each of those automata, autcross displays 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.

autcross --list-shorthands

If a COMMANDFMT does not use any %-sequence, and starts with one of
the following regexes, then the string on the right is appended.

  autfilt                                  %H>%O
  dra2dpa                                  <%H>%O
  dstar2tgba                               %H>%O
  ltl2dstar                                -B %H %O
  nba2l?dpa                                <%H>%O
  seminator                                %H>%O
  owl.* (ngba2ldba|nba(2dpa|2det|sim)|aut2parity|gfg-minimization)\b <%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'

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

randaut -B -n 3 a b |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes'

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.

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 languages 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.

Similarly, if the tools being tested implement complementation algorithm, adding the --language-complemented will additionally compare the outputs using this own complementation algorithm. Using this option is more efficient than passing autfilt --complement as a tool, since autcross can save on complementation by using the input automaton.

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 participates to these equivalence checks.

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

randaut -B -n 3 a b --name="automaton %L" |
autcross --language-preserved 'autfilt --complement'

-:1.1-46.7	automaton 0
Running [A0]: autfilt --complement 'lcr-i0-zp0sqw'>'lcr-o0-RDpnZH'
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}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
       !a & !b; cycle{!a & !b; !a & !b; !a & b; a & !b}

-:47.1-94.7	automaton 1
Running [A0]: autfilt --complement 'lcr-i1-sZbXFh'>'lcr-o0-wLdK4i'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
       cycle{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}

-:95.1-140.7	automaton 2
Running [A0]: autfilt --complement 'lcr-i2-agwhTv'>'lcr-o0-b2AmZl'
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:
       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.

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 similarly.

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 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 ltldo to arrange that.

genltl --eh-patterns=1..3 | ltl2tgba |
  autcross 'autfilt -P -D' 'ltldo ltl2dstar -f %M >%O'

-:1.1-16.7	p0 U (p1 & Gp2)
Running [A0]: autfilt -P -D 'lcr-i0-AXZqTx'>'lcr-o0-mkFfLg'
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & Gp2)' >'lcr-o1-S4ywC1'
Performing sanity checks and gathering statistics...

-:17.1-34.7	p0 U (p1 & X(p2 U p3))
Running [A0]: autfilt -P -D 'lcr-i1-xL60h1'>'lcr-o0-wQKVX8'
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 U p3))' >'lcr-o1-TnZN7b'
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-zYGBjs'>'lcr-o0-X3tfSE'
Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))' >'lcr-o1-HCB0YH'
Performing sanity checks and gathering statistics...

No problem detected.

The previous example was a bit contrived, and in this case, a saner alternative would be to use ltlcross, as in:

genltl --eh-patterns=1..3 |
  ltlcross 'ltl2tgba %f | autfilt -P -D > %O' 'ltl2dstar'

-:1: (p0) U ((p1) & (G(p2)))
Running [P0]: ltl2tgba '(p0) U ((p1) & (G(p2)))' | autfilt -P -D > 'lcr-o0-Lqys0w'
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i0-8kEuVf' 'lcr-o1-NX7oNK'
Running [N0]: ltl2tgba '!((p0) U ((p1) & (G(p2))))' | autfilt -P -D > 'lcr-o0-cutYWe'
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i0-PtnwmG' 'lcr-o1-o24HFW'
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-QGjeJt'
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i1-GkMuFm' 'lcr-o1-O0ROHU'
Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) U (p3)))))' | autfilt -P -D > 'lcr-o0-yH8XO0'
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i1-NWKuRh' 'lcr-o1-aXL6q0'
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-IKhElH'
Running [P1]: ltl2dstar --output-format=hoa 'lcr-i2-HUAzAF' 'lcr-o1-kVN0cq'
Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6)))))))))))))))' | autfilt -P -D > 'lcr-o0-xCR7E7'
Running [N1]: ltl2dstar --output-format=hoa 'lcr-i2-9BDW3i' 'lcr-o1-XZ64Kz'
Performing sanity checks and gathering statistics...

No problem detected.

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.

While the autcross command itself has no built-in support for parallelization (patches welcome), its interface allows easy parallelization with third party tools such as: xargs -P (GNU findutils), parallel (GNU parallel or moreutils), or even make. See running ltlcross in parallel for inspiration.