diff --git a/NEWS b/NEWS index d4e0ce65e..7c37603eb 100644 --- a/NEWS +++ b/NEWS @@ -38,6 +38,13 @@ New in spot 2.4.1.dev (not yet released) - autcross, ltlcross, and ltldo learned --fail-on-timeout. + - ltlcross learned --reference=COMMANDFMT to specify a translator + that should be trusted. Doing so makes it possible to reduce the + number of tests to be performed, as all other translators will be + compared to the reference's output when available. Multiple + reference can be given; in that case other tools are compared + against the smallest reference automaton. + - The new -x tls-impl=N option allows to fine-tune the implication-based simplification rules of ltl2tgba. See the spot-x man-page for details. diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 20c8ca495..f88118f30 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -81,8 +81,9 @@ static void show_shorthands(shorthands_t* begin, shorthands_t* end) } -tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end) - : spec(spec), cmd(spec), name(spec) +tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, + bool is_ref) + : spec(spec), cmd(spec), name(spec), reference(is_ref) { if (*cmd == '{') { @@ -144,7 +145,8 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end) } tool_spec::tool_spec(const tool_spec& other) - : spec(other.spec), cmd(other.cmd), name(other.name) + : spec(other.spec), cmd(other.cmd), name(other.name), + reference(other.reference) { if (cmd != spec) cmd = strdup(cmd); @@ -174,18 +176,20 @@ tool_spec::~tool_spec() std::vector tools; -void tools_push_trans(const char* trans) +void tools_push_trans(const char* trans, bool is_ref) { tools.emplace_back(trans, std::begin(shorthands_ltl), - std::end(shorthands_ltl)); + std::end(shorthands_ltl), + is_ref); } -void tools_push_autproc(const char* proc) +void tools_push_autproc(const char* proc, bool is_ref) { tools.emplace_back(proc, std::begin(shorthands_autproc), - std::end(shorthands_autproc)); + std::end(shorthands_autproc), + is_ref); } void diff --git a/bin/common_trans.hh b/bin/common_trans.hh index 2811ebc61..37dae4746 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -47,8 +47,11 @@ struct tool_spec const char* cmd; // name of the translator (or spec) const char* name; + // Whether the tool is a reference. + bool reference; - tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end); + tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, + bool is_ref); tool_spec(const tool_spec& other); tool_spec& operator=(const tool_spec& other); ~tool_spec(); @@ -56,8 +59,8 @@ struct tool_spec extern std::vector tools; -void tools_push_trans(const char* trans); -void tools_push_autproc(const char* proc); +void tools_push_trans(const char* trans, bool is_ref = false); +void tools_push_autproc(const char* proc, bool is_ref = false); struct quoted_string final: public spot::printable_value { diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 47cd9e749..1563a28e6 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -95,6 +95,7 @@ enum { OPT_NOCOMP, OPT_OMIT, OPT_PRODUCTS, + OPT_REFERENCE, OPT_SEED, OPT_STATES, OPT_STOP_ERR, @@ -104,6 +105,9 @@ enum { static const argp_option options[] = { + { "reference", OPT_REFERENCE, "COMMANDFMT", 0, + "register one translator and assume it is correct (do not" + "check it for error, but use it to check other translators)", 2 }, /**************************************************/ { nullptr, 0, nullptr, 0, "ltlcross behavior:", 5 }, { "allow-dups", OPT_DUPS, nullptr, 0, @@ -482,6 +486,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_OMIT: opt_omit = true; break; + case OPT_REFERENCE: + tools_push_trans(arg, true); + break; case OPT_SEED: seed = to_pos_int(arg); break; @@ -1092,6 +1099,39 @@ namespace std::cerr << "Performing sanity checks and gathering statistics..." << std::endl; + // If we have reference tools, pick the smallest of their + // automata for positive and negative references. + auto smallest_ref = [&](std::vector& from) + { + typedef std::tuple aut_size; + int smallest_ref = -1; + aut_size smallest_size(true, -1U, -1U, -1U); + for (unsigned i = 0; i < m; ++i) + if (tools[i].reference && from[i]) + { + aut_size pisize(!is_deterministic(from[i]), + from[i]->num_states(), + from[i]->num_edges(), + from[i]->num_sets()); + if (pisize < smallest_size) + { + smallest_ref = i; + smallest_size = pisize; + } + } + return smallest_ref; + }; + + // This are not our definitive choice for reference + // automata, because the sizes might change after we remove + // alternation and Fin acceptance. But we need to know now + // if we will have a pair of reference automata in order to + // skip some of the constructions. + int smallest_pos_ref = smallest_ref(pos); + int smallest_neg_ref = smallest_ref(neg); + if (smallest_pos_ref < 0 || smallest_neg_ref < 0) + smallest_pos_ref = smallest_neg_ref = -1; + bool print_first = verbose; auto unalt = [&](std::vector& x, unsigned i, char prefix) @@ -1126,11 +1166,15 @@ namespace comp[i] = dualize(x[i]); }; - for (unsigned i = 0; i < m; ++i) + for (size_t i = 0; i < m; ++i) { unalt(pos, i, 'P'); - complement(pos, comp_pos, i); unalt(neg, i, 'N'); + // Do not complement reference automata if we have a + // reference pair. + if (smallest_pos_ref >= 0 && tools[i].reference) + continue; + complement(pos, comp_pos, i); complement(neg, comp_neg, i); } @@ -1138,11 +1182,15 @@ namespace { print_first = verbose; auto tmp = [&](std::vector& from, - std::vector& to, unsigned i, + std::vector& to, int i, char prefix) { if (from[i] && !to[i]) { + // Do not complement reference automata if we have a + // reference pair. + if (smallest_pos_ref >= 0 && tools[i].reference) + return; if (print_first) { std::cerr << "info: complementing non-deterministic " @@ -1207,7 +1255,7 @@ namespace cleanup_acceptance_here(x[i]); } }; - for (unsigned i = 0; i < m; ++i) + for (size_t i = 0; i < m; ++i) { tmp(pos, i, " P", " "); tmp(neg, i, " N", " "); @@ -1215,14 +1263,40 @@ namespace tmp(comp_neg, i, "Comp(N", ")"); } + if (smallest_pos_ref >= 0) + { + // Recompute the smallest references now, because removing + // alternation and Fin acceptance might have changed the + // sizes. + smallest_pos_ref = smallest_ref(pos); + smallest_neg_ref = smallest_ref(neg); + + if (verbose) + std::cerr << "info: P" << smallest_pos_ref + << " and N" << smallest_neg_ref << " assumed " + << "correct and used as references\n"; + } + // intersection test for (size_t i = 0; i < m; ++i) if (pos[i]) for (size_t j = 0; j < m; ++j) if (neg[j]) { - problems += - check_empty_prod(pos[i], neg[j], i, j, false, false); + // Do not compare reference translators. + if (tools[i].reference && tools[j].reference) + continue; + // If we have a reference pair, only compare + // against that pair when i != j. + if (i == j || + !((!tools[i].reference && + smallest_neg_ref >= 0 && + (size_t)smallest_neg_ref != j) + || (!tools[j].reference && + smallest_pos_ref >= 0 && + (size_t)smallest_pos_ref != i))) + problems += + check_empty_prod(pos[i], neg[j], i, j, false, false); // Deal with the extra complemented automata if we // have some. @@ -1240,13 +1314,15 @@ namespace // translation was not deterministic. if (i != j && comp_pos[j] && !comp_neg[j]) - problems += - check_empty_prod(pos[i], comp_pos[j], - i, j, false, true); + if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref) + problems += + check_empty_prod(pos[i], comp_pos[j], + i, j, false, true); if (i != j && comp_neg[i] && !comp_pos[i]) - problems += - check_empty_prod(comp_neg[i], neg[j], - i, j, true, false); + if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref) + problems += + 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]))) problems += @@ -1370,7 +1446,7 @@ namespace // consistency check for (size_t i = 0; i < m; ++i) - if (pos_map[i] && neg_map[i]) + if (pos_map[i] && neg_map[i] && !tools[i].reference) { if (verbose) std::cerr << "info: consistency_check (P" << i diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 8a2ef778a..2da4bcdc8 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -53,6 +53,8 @@ and no =-f= or =-F= options are given. * Configuring translators +** Translator specifications + Each translator should be specified as a string that use some of the following character sequences: @@ -65,8 +67,8 @@ following character sequences: : LBT, or Wring's syntax : %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or : Wring's syntax -: %O the automaton is output in HOA, never claim, LBTT, -: or ltl2dstar's format +: %O the automaton output in HOA, never claim, LBTT, or +: 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)=. @@ -207,6 +209,26 @@ Because only the prefix of the actual command is checked, you can still specify some options. For instance =ltlcross 'ltl2tgba -D' ...= is short for =ltlcross 'ltl2tgba -D -H %F>%O' ...= +** Trusted and untrusted translators + +By default, all translators specified are not trusted. This means +that =ltlcross= will cross-compare the output of all translators, +possibly yielding a quadratic number of tests. + +It is possible to declare that certain translators should be trusted +by specifying them with the =--reference=COMMANDFMT= option. This has +a few implications: + - the automata output by reference translators are not tested + - a pair of positive and negative reference automata are selected + from the reference translators (the smallest automata, in case + multiple references are available), and all other translators will + only be compared to these reference automata. + +Consequently, the number of test performed is now linear in the number +of untrusted references. The easiest way to observe the effect of +=--reference= is to run the =ltlcross= with the [[#verbose][=--verbose= option]], +with and without some =--reference= translators. + * Getting statistics Detailed statistics about the result of each translation, and the @@ -969,6 +991,9 @@ be used to gather statistics about a specific set of formulas. # LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq # LocalWords: setenv concat getenv ** =--verbose= + :PROPERTIES: + :CUSTOM_ID: verbose + :END: The verbose option can be useful to troubleshoot problems or simply follow the list of transformations and tests performed by =ltlcross=. @@ -1055,8 +1080,6 @@ that the automaton =N0= is really the complement of =P0=. Similarly =P1=. Finally =P0*N1= and =P1*N0= ensure that =P1= is equivalent to =P0= and =N1= is equivalent to =N0=. - - Note that if we had not used the =--determinize= option, the procedure would look slightly more complex: @@ -1128,3 +1151,60 @@ it with the four automata, and then performs additional checks and =P1= are equivalent, they can catch some problems, and would easily catch the case of an automaton with an empty language by mistake. + +Here is the same example, if we declare that =ltl3ba= is a reference +implementation that should not be checked, and we just want to check +the output of =ltl2tgba= against this reference. See how the number +of tests performed has been reduced. + +#+BEGIN_SRC sh :results verbatim :exports code +ltlcross -f 'FGa' ltl2tgba --reference 'ltl3ba -H1' --verbose +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +SPOT_HOA_TOLERANT=1 ltlcross -f 'FGa' ltl2tgba --reference 'ltl3ba -H1' --verbose 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +F(G(a)) +Running [P0]: ltl3ba -H1 -f '<>([](a))'>'lcr-o0-UanRv9' +Running [P1]: ltl2tgba -H 'F(G(a))'>'lcr-o1-43jbVn' +Running [N0]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o0-TUeymC' +Running [N1]: ltl2tgba -H '!(F(G(a)))'>'lcr-o1-5PYsOQ' +info: collected automata: +info: P0 (2 st.,3 ed.,1 sets) +info: N0 (3 st.,5 ed.,1 sets) univ-edges complete +info: P1 (2 st.,3 ed.,1 sets) +info: N1 (1 st.,2 ed.,1 sets) deterministic complete +Performing sanity checks and gathering statistics... +info: getting rid of universal edges... +info: N0 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets) +info: getting rid of any Fin acceptance... +info: P0 (2 st.,3 ed.,1 sets) -> (2 st.,3 ed.,1 sets) +info: Comp(N1) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets) +info: P0 and N0 assumed correct and used as references +info: check_empty P0*N1 +info: check_empty P1*N0 +info: check_empty Comp(N1)*N0 +info: check_empty P1*N1 +info: building state-space #0/1 of 200 states with seed 0 +info: state-space has 4136 edges +info: building product between state-space and P0 (2 st., 3 ed.) +info: product has 400 st., 8298 ed. +info: 2 SCCs +info: building product between state-space and P1 (2 st., 3 ed.) +info: product has 400 st., 8298 ed. +info: 2 SCCs +info: building product between state-space and N0 (2 st., 4 ed.) +info: product has 400 st., 8272 ed. +info: 1 SCCs +info: building product between state-space and N1 (1 st., 2 ed.) +info: product has 200 st., 4136 ed. +info: 1 SCCs +info: cross_check {P0,P1}, state-space #0/1 +info: cross_check {N0,N1}, state-space #0/1 +info: consistency_check (P1,N1), state-space #0/1 + +No problem detected. +#+end_example diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 625033dbe..d78e6554e 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -36,10 +36,90 @@ ltl2tgba=ltl2tgba # Make sure ltlcross quotes formulas correctly cat >formula <<\EOF G"a'-'>'b" +FGa EOF run 0 ltlcross -F formula --csv=out.csv \ "$ltl2tgba -s %f >%N" \ - "$ltl2tgba --lenient -s %s >%N" + "$ltl2tgba --lenient -s %s >%N" \ + --verbose 2> error +cat >ceplan < ce +diff -u ce ceplan + +ltlcross -F formula --csv=out.csv \ + --ref "$ltl2tgba -s %f >%N" \ + "$ltl2tgba --lenient -s %s >%N" \ + --verbose 2> error +cat >ceplan < ce +diff -u ce ceplan + +ltlcross -F formula --csv=out.csv \ + -D "$ltl2tgba -s %f >%N" \ + "$ltl2tgba --lenient -s %s >%N" \ + --verbose 2> error +cat >ceplan < ce +diff -u ce ceplan + +ltlcross -F formula --csv=out.csv \ + -D --ref "$ltl2tgba -s %f >%N" \ + "$ltl2tgba --lenient -s %s >%N" \ + --verbose 2> error + +cat >ceplan < ce +diff -u ce ceplan + +ltlcross -F formula --csv=out.csv \ + --ref "$ltl2tgba -s %f >%N" \ + --ref "$ltl2tgba --lenient -s %s >%N" \ + --verbose 2> error +grep 'info: check_empty' error && exit 1 run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a grep 'ltlcross.*no input.*in.*foo bar' stderr