fec939c1a6
* src/bin/ltlcross.cc: Implement the counters. * doc/org/ltlcross.org: Update the documentation. * bench/ltl2tgba/sum.py: Do not assume a fixed column for the time. * NEWS: Update.
376 lines
19 KiB
Org Mode
376 lines
19 KiB
Org Mode
#+TITLE: =ltlcross=
|
|
#+EMAIL spot@lrde.epita.fr
|
|
#+OPTIONS: H:2 num:nil toc:t
|
|
#+LINK_UP: file:tools.html
|
|
|
|
=ltlcross= is a tool for cross-comparing the output of LTL-to-Büchi
|
|
translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], the
|
|
/LTL-to-Büchi Translator Testbench/, that essentially performs the
|
|
same sanity checks.
|
|
|
|
The main motivations for rewriting this tool were:
|
|
- support for PSL formulas in addition to LTL
|
|
- more statistics, especially:
|
|
- the number of logical transitions represented by each physical edge,
|
|
- the number of deterministic states and automata
|
|
- the number of SCCs with their various strengths (nonaccepting, terminal, weak, strong)
|
|
- the number of terminal, weak, and strong automata
|
|
- output in a format that can be more easily be post-processed,
|
|
- more precise time measurement (LBTT was only precise to
|
|
1/100 of a second, reporting most times as "0.00s").
|
|
|
|
Although =ltlcross= performs the same sanity checks as LBTT, it does
|
|
not implement any of the interactive features of LBTT. In our almost
|
|
10-year usage of LBTT, we never had to use its interactive features to
|
|
understand bugs in our translation. Therefore =ltlcross= will report
|
|
problems, but you will be on your own to investigate and fix them.
|
|
|
|
The core of =ltlcross= is a loop that does the following steps:
|
|
- Input a formula
|
|
- Translate the formula and its negation using each configured translator.
|
|
If there are 3 translators, the positive and negative translations
|
|
will be denoted =P0=, =N0=, =P1=, =N1=, =P2=, =N2=.
|
|
- Build the products of these automata with a random state-space (the same
|
|
state-space for all translations).
|
|
- Perform sanity checks between all these automata to detect any problem.
|
|
- Gather statistics if requested.
|
|
|
|
* Formula selection
|
|
|
|
Formulas to translate should be specified using the [[file:ioltl.org][common input options]].
|
|
Standard input is read if no =-f= or =-F= option is given.
|
|
|
|
* Configuring translators
|
|
|
|
Each translator should be specified as a string that use some of the
|
|
following character sequences:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin,
|
|
: LBT, or Wring's syntax
|
|
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
|
|
: Wring's syntax
|
|
: %N,%T the output automaton as a Never claim, or in
|
|
: LBTT's format
|
|
|
|
For instance here is how we could cross-compare the never claims
|
|
output by =spin= and =ltl2tgba= for the formulas =GFa= and =X(a U b)=.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
|
|
When =ltlcross= executes these commands, =%s= will be replaced
|
|
by the formula in Spin's syntax, and =%N= will be replaced by a
|
|
temporary file into which the output of the translator is redirected
|
|
before it is read back by =ltlcross=.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N' 2>&1
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
([](<>(a)))
|
|
Running [P0]: ltl2tgba -s '([](<>(a)))' >'lck-o0-iDGV6y'
|
|
Running [P1]: spin -f '([](<>(a)))' >'lck-o1-sA3FYp'
|
|
Running [N0]: ltl2tgba -s '(!([](<>(a))))' >'lck-o0-1ClVQg'
|
|
Running [N1]: spin -f '(!([](<>(a))))' >'lck-o1-wyErP7'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
(X((a) U (b)))
|
|
Running [P0]: ltl2tgba -s '(X((a) U (b)))' >'lck-o0-ex1BYY'
|
|
Running [P1]: spin -f '(X((a) U (b)))' >'lck-o1-UNE8dQ'
|
|
Running [N0]: ltl2tgba -s '(!(X((a) U (b))))' >'lck-o0-coM8tH'
|
|
Running [N1]: spin -f '(!(X((a) U (b))))' >'lck-o1-eHPoQy'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
no problem detected
|
|
#+end_example
|
|
|
|
=ltlcross= can only read two kinds of output:
|
|
- Never claims (only if they are restricted to representing an
|
|
automaton using =if=, =goto=, and =skip= statements) such as those
|
|
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. These
|
|
should be indicated using =%N=.
|
|
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with
|
|
either state-based acceptance or transition-based acceptance.
|
|
This output is used for instance by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][=lbt=]], [[http://web.archive.org/web/20080607170403/http://www.science.unitn.it/~stonetta/modella.html][=modella=]], or =ltl2tgba
|
|
--lbtt=. These should be indicated using =%T=.
|
|
|
|
Of course all configured tools need not the same =%= sequences.
|
|
|
|
* 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= or =--json=FILE= option.
|
|
|
|
The following compare =ltl2tgba=, =spin=, and =lbt= on three random
|
|
formula (where =W= and =M= operators have been rewritten away because
|
|
they are not supported by =spin= and =lbt=).
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
randltl -n 2 a b |
|
|
ltlfilt --remove-wm |
|
|
ltlcross --csv=results.csv \
|
|
'ltl2tgba -s %f >%N' \
|
|
'spin -f %s >%N' \
|
|
'lbt < %L >%T'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
randltl -n 2 a b c | ltlfilt --remove-wm |
|
|
ltlcross --csv=results.csv --json=results.json \
|
|
'ltl2tgba -s %f >%N' \
|
|
'spin -f %s >%N' \
|
|
'lbt < %L >%T' --csv=results.csv 2>&1
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
-:1: (G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))
|
|
Running [P0]: ltl2tgba -s '(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))' >'lck-o0-HcRzrd'
|
|
Running [P1]: spin -f '([]((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) V ((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) || (X(p1)))))' >'lck-o1-Sir9YC'
|
|
Running [P2]: lbt < 'lck-i0-W7LdjO' >'lck-o2-ZACV3b'
|
|
Running [N0]: ltl2tgba -s '(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))' >'lck-o0-KoveKk'
|
|
Running [N1]: spin -f '(!([]((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) V ((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) || (X(p1))))))' >'lck-o1-xxXdfU'
|
|
Running [N2]: lbt < 'lck-i0-tcO4oL' >'lck-o2-QQUs0t'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
-:2: (!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))
|
|
Running [P0]: ltl2tgba -s '(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))' >'lck-o0-qlcvic'
|
|
Running [P1]: spin -f '(!((!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))))' >'lck-o1-fEBqz3'
|
|
Running [P2]: lbt < 'lck-i1-sint9k' >'lck-o2-6oY4RU'
|
|
Running [N0]: ltl2tgba -s '((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))' >'lck-o0-6PQGuD'
|
|
Running [N1]: spin -f '(!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))' >'lck-o1-1l4NVu'
|
|
Running [N2]: lbt < 'lck-i1-iEEnbM' >'lck-o2-a2Toum'
|
|
Performing sanity checks and gathering statistics...
|
|
|
|
No problem detected.
|
|
#+end_example
|
|
|
|
After this execution, the file =results.csv= contains the following:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
cat results.csv
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
"formula", "tool", "states", "edges", "transitions", "acc", "scc", "nonacc_scc", "terminal_scc", "weak_scc", "strong_scc", "nondetstates", "nondeterministic", "terminal_aut", "weak_aut", "strong_aut", "time", "product_states", "product_transitions", "product_scc"
|
|
"(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "ltl2tgba -s %f >%N", 7, 27, 42, 1, 1, 0, 0, 0, 1, 5, 1, 0, 0, 1, 0.162927, 1333, 20565, 3
|
|
"(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "spin -f %s >%N", 55, 957, 1723, 1, 1, 0, 0, 0, 1, 55, 1, 0, 0, 1, 3.83261, 10791, 866615, 37
|
|
"(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "lbt < %L >%T", 167, 5656, 10744, 3, 2, 1, 0, 0, 1, 167, 1, 0, 0, 1, 0.0365079, 32258, 5318535, 96
|
|
"(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "ltl2tgba -s %f >%N", 11, 28, 72, 1, 10, 6, 1, 2, 1, 1, 1, 0, 0, 1, 0.0628941, 2163, 36722, 594
|
|
"(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "spin -f %s >%N", 23, 113, 331, 1, 14, 9, 1, 1, 3, 20, 1, 0, 0, 1, 0.101343, 4567, 171114, 1193
|
|
"(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "lbt < %L >%T", 157, 2414, 5957, 3, 109, 103, 1, 1, 4, 133, 1, 0, 0, 1, 0.0197828, 30811, 3020266, 19147
|
|
"(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "ltl2tgba -s %f >%N", 6, 12, 21, 1, 5, 3, 0, 1, 1, 1, 1, 0, 0, 1, 0.0509422, 806, 15638, 9
|
|
"(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "spin -f %s >%N", 11, 21, 47, 1, 8, 6, 0, 1, 1, 7, 1, 0, 0, 1, 0.0102468, 1217, 36416, 20
|
|
"(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "lbt < %L >%T", 17, 45, 100, 2, 13, 11, 0, 1, 1, 14, 1, 0, 0, 1, 0.00346881, 1744, 57783, 347
|
|
"((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "ltl2tgba -s %f >%N", 7, 14, 28, 1, 6, 3, 1, 1, 1, 2, 1, 0, 0, 1, 0.0503676, 1006, 19822, 10
|
|
"((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "spin -f %s >%N", 17, 43, 102, 1, 13, 10, 1, 1, 1, 12, 1, 0, 0, 1, 0.0474604, 2449, 70190, 256
|
|
"((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "lbt < %L >%T", 23, 68, 154, 2, 19, 16, 1, 1, 1, 18, 1, 0, 0, 1, 0.0037305, 2236, 73111, 640
|
|
#+end_example
|
|
|
|
This can be loaded in any spreadsheet application. Although we only
|
|
supplied 2 random generated formulas, the output contains 4 formulas because
|
|
=ltlcross= had to translate the positive and negative version of each.
|
|
|
|
If we had used the option =--json=results.json= instead of
|
|
=--cvs=results.csv=, the file =results.json= would have contained the
|
|
following [[http://www.json.org/][JSON]] output.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
cat results.json
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
{
|
|
"tool": [
|
|
"ltl2tgba -s %f >%N",
|
|
"spin -f %s >%N",
|
|
"lbt < %L >%T"
|
|
],
|
|
"formula": [
|
|
"(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))",
|
|
"(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))",
|
|
"(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))",
|
|
"((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))"
|
|
],
|
|
"fields": [
|
|
"formula", "tool", "states", "edges", "transitions", "acc", "scc", "nonacc_scc", "terminal_scc", "weak_scc", "strong_scc", "nondetstates", "nondeterministic", "terminal_aut", "weak_aut", "strong_aut", "time", "product_states", "product_transitions", "product_scc"
|
|
],
|
|
"inputs": [ 0, 1 ],
|
|
"results": [
|
|
[ 0, 0, 7, 27, 42, 1, 1, 0, 0, 0, 1, 5, 1, 0, 0, 1, 0.162927, 1333, 20565, 3 ],
|
|
[ 0, 1, 55, 957, 1723, 1, 1, 0, 0, 0, 1, 55, 1, 0, 0, 1, 3.83261, 10791, 866615, 37 ],
|
|
[ 0, 2, 167, 5656, 10744, 3, 2, 1, 0, 0, 1, 167, 1, 0, 0, 1, 0.0365079, 32258, 5318535, 96 ],
|
|
[ 1, 0, 11, 28, 72, 1, 10, 6, 1, 2, 1, 1, 1, 0, 0, 1, 0.0628941, 2163, 36722, 594 ],
|
|
[ 1, 1, 23, 113, 331, 1, 14, 9, 1, 1, 3, 20, 1, 0, 0, 1, 0.101343, 4567, 171114, 1193 ],
|
|
[ 1, 2, 157, 2414, 5957, 3, 109, 103, 1, 1, 4, 133, 1, 0, 0, 1, 0.0197828, 30811, 3020266, 19147 ],
|
|
[ 2, 0, 6, 12, 21, 1, 5, 3, 0, 1, 1, 1, 1, 0, 0, 1, 0.0509422, 806, 15638, 9 ],
|
|
[ 2, 1, 11, 21, 47, 1, 8, 6, 0, 1, 1, 7, 1, 0, 0, 1, 0.0102468, 1217, 36416, 20 ],
|
|
[ 2, 2, 17, 45, 100, 2, 13, 11, 0, 1, 1, 14, 1, 0, 0, 1, 0.00346881, 1744, 57783, 347 ],
|
|
[ 3, 0, 7, 14, 28, 1, 6, 3, 1, 1, 1, 2, 1, 0, 0, 1, 0.0503676, 1006, 19822, 10 ],
|
|
[ 3, 1, 17, 43, 102, 1, 13, 10, 1, 1, 1, 12, 1, 0, 0, 1, 0.0474604, 2449, 70190, 256 ],
|
|
[ 3, 2, 23, 68, 154, 2, 19, 16, 1, 1, 1, 18, 1, 0, 0, 1, 0.0037305, 2236, 73111, 640 ]
|
|
]
|
|
}
|
|
#+end_example
|
|
|
|
Here the =fields= table describes the columns of the =results= table.
|
|
The =inputs= tables lists the columns that are considered as inputs
|
|
for the experiments. The values in the columns corresponding to the
|
|
fields =formula= and =tool= contains indices relative to the =formula=
|
|
and =tool= tables. This format is more compact when dealing with lots
|
|
of translators and formulas, because they don't have to be repeated on
|
|
each line as in the CSV version.
|
|
|
|
JSON data can be easily processed in any language. For instance the
|
|
following Python3 script averages each column for each tool, and
|
|
presents the results in a form that can almost be copied into a LaTeX
|
|
table (the =%= in the tool names have to be taken care of). Note that
|
|
for simplicity we assume that the first two columns are inputs,
|
|
instead of reading the =inputs= field.
|
|
|
|
#+BEGIN_SRC python :results output :exports both
|
|
#!/usr/bin/python3
|
|
import json
|
|
data = json.load(open('results.json'))
|
|
datacols = range(2, len(data["fields"]))
|
|
# Index results by tool
|
|
results = { t:[] for t in range(0, len(data["tool"])) }
|
|
for l in data["results"]:
|
|
results[l[1]].append(l)
|
|
# Average columns for each tool, and display them as a table
|
|
print("%-18s & count & %s \\\\" % ("tool", " & ".join(data["fields"][2:])))
|
|
for i in range(0, len(data["tool"])):
|
|
c = len(results[i])
|
|
sums = ["%6.1f" % (sum([x[j] for x in results[i]])/c)
|
|
for j in datacols]
|
|
print("%-18s & %3d & %s \\\\" % (data["tool"][i], c,
|
|
" & ".join(sums)))
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: tool & count & states & edges & transitions & acc & scc & nonacc_scc & terminal_scc & weak_scc & strong_scc & nondetstates & nondeterministic & terminal_aut & weak_aut & strong_aut & time & product_states & product_transitions & product_scc \\
|
|
: ltl2tgba -s %f >%N & 4 & 7.0 & 20.0 & 40.0 & 1.0 & 5.0 & 3.0 & 0.0 & 1.0 & 1.0 & 2.0 & 1.0 & 0.0 & 0.0 & 1.0 & 0.1 & 1327.0 & 23186.0 & 154.0 \\
|
|
: spin -f %s >%N & 4 & 26.0 & 283.0 & 550.0 & 1.0 & 9.0 & 6.0 & 0.0 & 0.0 & 1.0 & 23.0 & 1.0 & 0.0 & 0.0 & 1.0 & 1.0 & 4756.0 & 286083.0 & 376.0 \\
|
|
: lbt < %L >%T & 4 & 91.0 & 2045.0 & 4238.0 & 2.0 & 35.0 & 32.0 & 0.0 & 0.0 & 1.0 & 83.0 & 1.0 & 0.0 & 0.0 & 1.0 & 0.0 & 16762.0 & 2117423.0 & 5057.0 \\
|
|
|
|
The script =bench/ltl2tgba/sum.py= is a more evolved version of the
|
|
above script that generates two kinds of LaTeX tables.
|
|
|
|
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 =ltlcross='s =--timeout= option to limit run
|
|
time) are not represented in the CSV or JSON files. However data for
|
|
bogus automata are still included: as shown below =ltlcross= will
|
|
report inconsistencies between automata as errors, but it does not try
|
|
to guess who is incorrect.
|
|
|
|
* Detecting problems
|
|
|
|
If a translator exits with a non-zero status code, or fails to output
|
|
an automaton =ltlcross= can read, and error will be displayed and the
|
|
result of the translation will be discarded.
|
|
|
|
Otherwise =ltlcross= performs the following checks on all translated
|
|
formulas ($P_i$ and $N_i$ designate respectively the translation of
|
|
positive and negative formulas by the ith translator).
|
|
|
|
- Intersection check: $P_i\otimes N_j$ must be empty for all
|
|
pairs of $(i,j)$.
|
|
|
|
A single failing translator might generate a lot of lines of
|
|
the form:
|
|
|
|
: error: P0*N1 is nonempty
|
|
: error: P1*N0 is nonempty
|
|
: error: P1*N1 is nonempty
|
|
: error: P1*N2 is nonempty
|
|
: error: P1*N3 is nonempty
|
|
: error: P1*N4 is nonempty
|
|
: error: P1*N5 is nonempty
|
|
: error: P1*N6 is nonempty
|
|
: error: P1*N7 is nonempty
|
|
: error: P1*N8 is nonempty
|
|
: error: P1*N9 is nonempty
|
|
: error: P2*N1 is nonempty
|
|
: error: P3*N1 is nonempty
|
|
: error: P4*N1 is nonempty
|
|
: error: P5*N1 is nonempty
|
|
: error: P6*N1 is nonempty
|
|
: error: P7*N1 is nonempty
|
|
: error: P8*N1 is nonempty
|
|
: error: P9*N1 is nonempty
|
|
|
|
In this example, translator number =1= looks clearly faulty
|
|
(at least the other 9 translators do not contradict each other).
|
|
|
|
- Cross-comparison checks: for some state-space $S$,
|
|
all $P_i\otimes S$ are either all empty, or all non-empty.
|
|
Similarly all $N_i\otimes S$ are either all empty, or all non-empty.
|
|
|
|
A cross-comparison failure could be displayed as:
|
|
|
|
: error: {P0,P2,P3,P4,P5,P6,P7,P8,P9} disagree with {P1} when evaluating the state-space
|
|
|
|
- Consistency check:
|
|
|
|
For each $i$, the products $P_i\otimes S$ and $N_i\otimes S$
|
|
actually cover all states of $S$. Because $S$ does not have any
|
|
deadlock, any of its infinite path must be accepted by $P_i$ or
|
|
$N_i$ (or both).
|
|
|
|
An error in that case is displayed as
|
|
|
|
: error: inconsistency between P1 and N1
|
|
|
|
The above checks are the same that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]].
|
|
|
|
If any problem was reported during the translation of one of the
|
|
formulas, =ltlcheck= will exit with an exit status of =1=. Statistics
|
|
(if requested) are output nonetheless, and include any faulty
|
|
automaton as well.
|
|
|
|
* Miscellaneous options
|
|
|
|
** =--stop-on-error=
|
|
|
|
The =--stop-on-error= will cause =ltlcross= to abort on the first
|
|
detected error. This include failure to start some translator, read
|
|
its output, or failure to passe the sanity checks. Timeouts are
|
|
allowed.
|
|
|
|
One use for this option is when =ltlcross= is used in combination with
|
|
=randltl= to check translators on an infinite stream of formulas.
|
|
|
|
For instance the following will cross-compare =ltl2tgba= against
|
|
=ltl3ba= until it finds an error, or your interrupt the command, or it
|
|
runs out of memory (the hash tables used by =randltl= and =ltlcross=
|
|
to remove duplicate formulas will keep growing).
|
|
|
|
#+BEGIN_SRC sh :export code :eval no
|
|
randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N'
|
|
#+END_SRC
|
|
|
|
** =--no-check=
|
|
|
|
The =--no-check= option disables all sanity checks, and only use the supplied
|
|
formulas in their positive form.
|
|
|
|
When checks are enabled, the negated formulas are intermixed with the
|
|
positives ones in the results. Therefore the =--no-check= option can
|
|
be used to gather statistics about a specific set of formulas.
|
|
|
|
# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed
|
|
# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY
|
|
# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella
|
|
# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ
|
|
# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO
|
|
# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic
|
|
# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq
|
|
# LocalWords: setenv concat getenv
|