diff --git a/NEWS b/NEWS index 0b538d26a..8de6a1918 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,12 @@ New in spot 1.1.4a (not relased) search for bugs in translators to Rabin or Streett automata, but the statistics might not be very relevant. + - When ltlcross obtains a deterministic automaton from a + translator it will now complement this automaton to perform + additional intersection checks. This is complementation is done + only for deterministic automata (because that is cheap) and can + be disabled with --no-complement. + - To help with debugging problems detected by ltlcross, the environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where temporary files are created and if they should be erased. Read diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index af2ef4aa2..e63064b99 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -8,32 +8,38 @@ translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Softw /LTL-to-Büchi Translator Testbench/, that essentially performs the same sanity checks. -The main motivations for rewriting this tool were: +The main differences are: - 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, + - statistics 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"). + 1/100 of a second, reporting most times as "0.00s"), + - support for deterministic Rabin or Streett automata written in + [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]], + - additional intersection checks with the complement of any + deterministic automaton produced by a translator. 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. +problems, maybe with a conterexample, 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=. + will be denoted =P0=, =N0=, =P1=, =N1=, =P2=, =N2=. Optionally + build complemented automata denoted =Comp(P0)=, =Comp(N0)=, etc. + - Perform sanity checks between all these automata to detect any problem. - Build the products of these automata with a random state-space (the same state-space for all translations). (If the =--products=N= option is given, =N= products are performed instead.) - - Perform sanity checks between all these automata to detect any problem. - Gather statistics if requested. * Formula selection @@ -54,8 +60,8 @@ ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' : 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 +: %N,%T,%D the output automaton as a Never claim, in LBTT's +: or in LTL2DSTAR'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)=. @@ -92,17 +98,55 @@ Performing sanity checks and gathering statistics... no problem detected #+end_example -=ltlcross= can only read two kinds of output: +=ltlcross= can only read three 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=. + should be indicated using =%N=. The newer syntax introduced by + Spin 6.24, using =do= instead of =if=, is also supported. - [[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=. + - [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]], which support deterministic Rabin or Streett + automata. After =ltlcross= reads such input, it immediately + convert it into a Büchi automaton. Rabin automata are converted + to (degeneralized) Büchi automata and the conversion will preserve + the determinism anytime a deterministic Büchi automaton exists for + that property (this determinism is good for the complemented + intersection check discussed below). Streett automata are + converted to non-deterministic TGBA, where generalized acceptance + conditions are used to reduce the size of the automaton you would + get by the classical conversion from Streett to Büchi. + This kind of output (Rabin or Streett) should be indicated with =%T=. -Of course all configured tools need not the same =%= sequences. +Of course all configured tools need not use the same =%= sequences. +The following list shows some typical configurations for some existing +tools: + + - '=spin -f %s >%N=' + - '=ltl2ba -f %s >%N=' + - '=ltl3ba -f -S %s >%N=' + - '=ltl3ba -f -S -M %s >%N=' (more deterministic output) + - '=modella -r12 -g -e %L %T=' + - '=/path/to/script4lbtt.py %L %T=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for + its interface with LBTT) + - '=ltl2tgba -s %s >%N=' (smaller output, Büchi automaton) + - '=ltl2tgba -s -D %s >%N=' (more deterministic output, Büchi automaton) + - '=ltl2tgba --lbtt %s >%T=' (smaller output, TGBA) + - '=ltl2tgba --lbtt -D %s >%T=' (more deterministic output, TGBA) + - '=lbt <%L >%T=' + - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L %T=' + (deterministic Rabin output) + - '=ltl2dstar --automata=streett --ltl2nba=spin:path/tp/ltl2tgba@-sD + %L %T=' (deterministic Streett output) + - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L - | dstar2tgba + -s >%N=' (external conversion from Rabin to Büchi done by + =dstar2tgba= for additional reduction of the Büchi automaton than + what =ltlcross= would provide) + - '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer + uses the last =%D= argument as a prefix to which it always append =.dst=, + so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file) * Getting statistics @@ -423,6 +467,24 @@ positive and negative formulas by the ith translator). followed by a cycle that should be repeated infinitely often. The cycle part is denoted by =cycle{...}=. + - Complemented intersection check. If $P_i$ and $P_j$ are + deterministic, we =ltlcross= builds their complements, $Comp(P_i)$ + and $Comp(P_j)$, and then ensures that $Comp(P_i)\otimes + Comp(P_j)$ is empty. If only one of them is deterministic, + for instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all + $j \ne i$; likewise if it's $N_i$ that is deterministic. + + This check is only done for deterministic automata, because + complementation is cheap is that case. When validating a + translator with =ltlcross=, we highly recommend to include a + translator with good deterministic output to augment test + coverage. Using '=ltl2tgba -lD %f >%T=' will produce + deterministic automata for all obligation properties and many + recurrence properties. Using '=ltl2dstar + --ltl2nba=spin:pathto/ltl2tgba@-sD %L %D=' is more expansive, but + it will produce a deterministic Büchi automaton whenever one + exists. + - 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. @@ -451,7 +513,9 @@ positive and negative formulas by the ith translator). the state-space in which the inconsistency was detected is also printed. -The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]]. +The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], +except for the complemented intersection check, which is only done in +=ltlcross=. If any problem was reported during the translation of one of the formulas, =ltlcheck= will exit with an exit status of =1=. Statistics diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index dee18c300..96a2fddea 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -53,6 +53,7 @@ #include "tgbaalgos/isweakscc.hh" #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/word.hh" +#include "tgbaalgos/dbacomp.hh" #include "misc/formater.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/isdet.hh" @@ -91,6 +92,7 @@ Exit status:\n\ #define OPT_SEED 8 #define OPT_PRODUCTS 9 #define OPT_COLOR 10 +#define OPT_NOCOMP 11 static const argp_option options[] = { @@ -122,6 +124,8 @@ static const argp_option options[] = { "no-checks", OPT_NOCHECKS, 0, 0, "do not perform any sanity checks (negated formulas " "will not be translated)", 0 }, + { "no-complement", OPT_NOCOMP, 0, 0, + "do not complement deterministic automata to perform extra checks", 0 }, { "stop-on-error", OPT_STOP_ERR, 0, 0, "stop on first execution error or failure to pass" " sanity checks (timeouts are OK)", 0 }, @@ -190,6 +194,7 @@ const char* csv_output = 0; bool want_stats = false; bool allow_dups = false; bool no_checks = false; +bool no_complement = false; bool stop_on_error = false; int seed = 0; unsigned products = 1; @@ -403,6 +408,10 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_NOCHECKS: no_checks = true; + no_complement = true; + break; + case OPT_NOCOMP: + no_complement = true; break; case OPT_SEED: seed = to_pos_int(arg); @@ -850,7 +859,7 @@ namespace static void check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j, - size_t i, size_t j) + size_t i, size_t j, bool icomp, bool jcomp) { spot::tgba_product* prod = new spot::tgba_product(aut_i, aut_j); spot::emptiness_check* ec = spot::couvreur99(prod); @@ -858,8 +867,17 @@ namespace if (res) { - global_error() << "error: P" << i << "*N" << j - << " is nonempty"; + std::ostream& err = global_error(); + err << "error: "; + if (icomp) + err << "Comp(N" << i << ")"; + else + err << "P" << i; + if (jcomp) + err << "*Comp(P" << j << ")"; + else + err << "*N" << j; + err << " is nonempty"; spot::tgba_run* run = res->accepting_run(); if (run) @@ -1059,9 +1077,16 @@ namespace } } + // These store the result of the translation of the positive and + // negative formulas. size_t m = translators.size(); std::vector pos(m); std::vector neg(m); + // These store the complement of the above results, when we can + // compute it easily. + std::vector comp_pos(m); + std::vector comp_neg(m); + unsigned n = vstats.size(); vstats.resize(n + (no_checks ? 1 : 2)); @@ -1071,7 +1096,17 @@ namespace formulas.push_back(fstr); for (size_t n = 0; n < m; ++n) - pos[n] = runner.translate(n, 'P', pstats); + { + pos[n] = runner.translate(n, 'P', pstats); + // If the automaton is deterministic, compute its complement + // as well. Note that if we have computed statistics + // already, there is no need to call is_deterministic() + // again. + if (!no_complement && pos[n] + && ((want_stats && !(*pstats)[n].nondeterministic) + || (!want_stats && is_deterministic(pos[n])))) + comp_pos[n] = dba_complement(pos[n]); + } // ---------- Negative Formula ---------- @@ -1099,7 +1134,17 @@ namespace formulas.push_back(runner.formula()); for (size_t n = 0; n < m; ++n) - neg[n] = runner.translate(n, 'N', nstats); + { + neg[n] = runner.translate(n, 'N', nstats); + // If the automaton is deterministic, compute its + // complement as well. Note that if we have computed + // statistics already, there is no need to call + // is_deterministic() again. + if (!no_complement && neg[n] + && ((want_stats && !(*nstats)[n].nondeterministic) + || (!want_stats && is_deterministic(neg[n])))) + comp_neg[n] = dba_complement(neg[n]); + } nf->destroy(); } @@ -1116,7 +1161,33 @@ namespace if (pos[i]) for (size_t j = 0; j < m; ++j) if (neg[j]) - check_empty_prod(pos[i], neg[j], i, j); + { + check_empty_prod(pos[i], neg[j], i, j, false, false); + + // Deal with the extra complemented automata if we + // have some. + + // If comp_pos[j] and comp_neg[j] exist for the + // same j, it means pos[j] and neg[j] were both + // deterministic. In that case, we will want to + // make sure that comp_pos[j]*comp_neg[j] is empty + // to assert the complementary of pos[j] and + // neg[j]. However using comp_pos[j] and + // comp_neg[j] against other translator will not + // give us any more insight than pos[j] and + // neg[j]. So we only do intersection checks with + // a complement automata when one of the two + // translation was not deterministic. + + if (i != j && comp_pos[j] && !comp_neg[j]) + check_empty_prod(pos[i], comp_pos[j], i, j, false, true); + if (i != j && comp_neg[i] && !comp_neg[i]) + check_empty_prod(comp_neg[i], neg[j], i, j, true, false); + if (comp_pos[i] && comp_neg[j] && + (i == j || (!comp_neg[i] && !comp_pos[j]))) + check_empty_prod(comp_pos[i], comp_neg[j], + i, j, true, true); + } } else { @@ -1236,7 +1307,11 @@ namespace if (!no_checks) for (size_t i = 0; i < m; ++i) - delete neg[i]; + { + delete neg[i]; + delete comp_neg[i]; + delete comp_pos[i]; + } for (size_t i = 0; i < m; ++i) delete pos[i]; diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 3727521b6..8112862ac 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -81,10 +81,7 @@ Technology. The main motivation for the reimplementation was to support PSL, and output more statistics about the translations. The sanity checks performed on the result of each translator (by -either LBTT or ltlcross) are described in the following paper. Our -implementation will detect and reports problems (like inconsistencies -between two translations) but unlike LBTT it does not offer an -interactive mode to investigate such problems. +either LBTT or ltlcross) are described in the following paper. .TP th02 @@ -92,3 +89,20 @@ H. Tauriainen and K. Heljanko: Testing LTL formula translation into Büchi automata. Int. J. on Software Tools for Technology Transfer. Volume 4, number 1, October 2002. +LBTT did not implement Test 2 described in this paper. ltlcross +implements a slight variation: when an automaton produced by some +translator is deterministic, its complement is built and used for +additional cross-comparisons with other tools. If the translation P1 +of the positive formula and the translation N1 of the negative formula +both yield deterministic automata (this may only happen for obligation +properties) then the emptiness check of Comp(P1)*Comp(N1) is +equivalent to Test 2 of Tauriainen and Heljanko. If only one +automaton is deterministic, say P1, it can still be used to check we +can be used to check the result of another translators, for instance +checking the emptiness of Comp(P1)*P2. + +Our implementation will detect and reports problems (like +inconsistencies between two translations) but unlike LBTT it does not +offer an interactive mode to investigate such problems. + +