diff --git a/NEWS b/NEWS index 854efcb38..dc49dad08 100644 --- a/NEWS +++ b/NEWS @@ -43,6 +43,13 @@ New in spot 1.99.7a (not yet released) * autfilt has a new option, --equivalent-to, to filter automata that are equivalent (language-wise) to a given automaton. + * ltlcross has a new option --determinize to instruct it to + complement non-deterministic automata via determinization. This + option is not enabled by default as it can potentially be slow and + generate large automata. When --determinize is given, option + --product=0 is implied, since the tests based on products with + random state-space are pointless for deterministic automata. + * ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and --bsize-max=N have been reimplemented as --size=RANGE and --bsize=RANGE. The old names are still supported for backward diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index c2759f25d..ba7b34528 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -59,6 +59,7 @@ #include #include #include +#include #include #include #include @@ -107,6 +108,9 @@ static const argp_option options[] = "will not be translated)", 0 }, { "no-complement", OPT_NOCOMP, nullptr, 0, "do not complement deterministic automata to perform extra checks", 0 }, + { "determinize", 'D', nullptr, 0, + "determinize non-deterministic automata so that they" + "can be complemented; also implicitly sets --products=0", 0 }, { "stop-on-error", OPT_STOP_ERR, nullptr, 0, "stop on first execution error or failure to pass" " sanity checks (timeouts are OK)", 0 }, @@ -195,6 +199,7 @@ static bool want_stats = false; static bool allow_dups = false; static bool no_checks = false; static bool no_complement = false; +static bool determinize = false; static bool stop_on_error = false; static int seed = 0; static unsigned products = 1; @@ -398,6 +403,10 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { + case 'D': + determinize = true; + products = 0; + break; case ARGP_KEY_ARG: translators.push_back(arg); break; @@ -812,7 +821,6 @@ namespace typedef std::unordered_set fset_t; - class processor: public job_processor { spot::bdd_dict_ptr dict = spot::make_bdd_dict(); @@ -1059,35 +1067,87 @@ namespace std::cerr << "Performing sanity checks and gathering statistics..." << std::endl; - if (verbose) - std::cerr << "info: getting rid of any Fin acceptance...\n"; + auto printsize = [](const spot::const_twa_graph_ptr& aut) + { + std::cerr << aut->num_states() << " st.," + << aut->num_edges() << " ed.," + << aut->num_sets() << " sets"; + }; + + if (determinize && !no_complement) + { + bool print_first = verbose; + auto tmp = [&](std::vector& from, + std::vector& to, unsigned i, + char prefix) + { + if (!to[i]) + { + if (print_first) + { + std::cerr << "info: complementing non-deterministic " + "automata via determinization...\n"; + print_first = false; + } + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + to[i] = dtwa_complement(p.run(from[i])); + if (verbose) + { + std::cerr << "info: " << prefix << i << "\t("; + printsize(from[i]); + std::cerr << ") -> ("; + printsize(to[i]); + std::cerr << ")\tComp(" << prefix << i << ")\n"; + } + } + }; + for (unsigned i = 0; i < m; ++i) + { + tmp(pos, comp_pos, i, 'P'); + tmp(neg, comp_neg, i, 'N'); + } + } + + bool print_first = verbose; + auto tmp = [&](std::vector& x, unsigned i, + const char* prefix, const char* suffix) + { + if (!x[i]) + return; + cleanup_acceptance_here(x[i]); + if (x[i]->acc().uses_fin_acceptance()) + { + if (verbose) + { + if (print_first) + { + std::cerr << + "info: getting rid of any Fin acceptance...\n"; + print_first = false; + } + std::cerr << "info:\t" << prefix << i + << suffix << "\t("; + printsize(x[i]); + std::cerr << ") ->"; + } + x[i] = remove_fin(x[i]); + if (verbose) + { + std::cerr << " ("; + printsize(x[i]); + std::cerr << ")\n"; + } + } + }; for (unsigned i = 0; i < m; ++i) { -#define DO(x, prefix, suffix) if (x[i]) \ - { \ - cleanup_acceptance_here(x[i]); \ - if (x[i]->acc().uses_fin_acceptance()) \ - { \ - auto st = x[i]->num_states(); \ - auto tr = x[i]->num_edges(); \ - auto ac = x[i]->acc().num_sets(); \ - x[i] = remove_fin(x[i]); \ - if (verbose) \ - std::cerr << "info:\t" prefix << i \ - << suffix << "\t(" \ - << st << " st., " \ - << tr << " ed., " \ - << ac << " sets) -> (" \ - << x[i]->num_states() << " st., " \ - << x[i]->num_edges() << " ed., " \ - << x[i]->acc().num_sets() << " sets)\n"; \ - } \ - } - DO(pos, " P", " "); - DO(neg, " N", " "); - DO(comp_pos, "Comp(P", ")"); - DO(comp_neg, "Comp(N", ")"); -#undef DO + tmp(pos, i, " P", " "); + tmp(neg, i, " N", " "); + tmp(comp_pos, i, "Comp(P", ")"); + tmp(comp_neg, i, "Comp(N", ")"); } // intersection test diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 887b77c47..693a2650c 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -19,8 +19,8 @@ The main differences are: - more precise time measurement (LBTT was only precise to 1/100 of a second, reporting most times as "0.00s"), - support for any type of acceptance condition, - - additional intersection checks with the complement of any - deterministic automaton produced by a translator. + - additional intersection checks with the complement, allowing + to check equivalence of automata more precisely. Although =ltlcross= performs the same sanity checks as LBTT, it does not implement any of the interactive features of LBTT. In our almost @@ -52,7 +52,7 @@ 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' + ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : %% a single % @@ -570,6 +570,9 @@ ltlcross -f a -f Ga '{small} ltl2tgba -s --small %f >%O' '{deter} ltl2tgba -s -- : "(!(G(a)))","deter","ok",0,0.0396312,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2 * Detecting problems + :PROPERTIES: + :CUSTOM_ID: checks + :END: 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 @@ -613,22 +616,29 @@ positive and negative formulas by the ith translator). 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)$ + deterministic, =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 >%O=' will produce - deterministic automata for all obligation properties and many - recurrence properties. Using '=ltl2dstar - --ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will systematically - produce a deterministic Rabin automaton (that =ltlcross= can - complement easily). + By default this check is only done for deterministic automata, + because complementation is relatively cheap is that case (at least + it is cheap for simple acceptance conditions). Using option + =--determinize=, =ltlcross= can be instructed to perform + complementation of non-deterministic automata as well, ensuring + precise equivalence checks between all automata. However be aware + that this determinization + complementation may generate large + automata. + + When validating a translator with =ltlcross= without using the + =--determinize= option we highly recommend to include a translator + with good deterministic output to augment test coverage. Using + '=ltl2tgba -lD %f >%O=' will produce deterministic automata for + all obligation properties and many recurrence properties. Using + '=ltl2dstar --ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will + systematically produce a deterministic Rabin automaton (that + =ltlcross= can complement easily). - Cross-comparison checks: for some state-space $S$, all $P_i\otimes S$ are either all empty, or all non-empty. @@ -643,6 +653,13 @@ positive and negative formulas by the ith translator). itself, except to explain why you may get multiple disagreement between the same sets of automata. + These products tests may sometime catch errors that were not + captured by the first two tests if one non-deterministic automaton + recognize less words than what it should. If the input automata + are deterministic or the =--determinize= option is used, this test + is redundant and can be disabled. (In fact, the =--determinize= + option implies option =--product=0= to do so.) + - Consistency check: For each $i$, the products $P_i\otimes S$ and $N_i\otimes S$ @@ -658,6 +675,13 @@ positive and negative formulas by the ith translator). the state-space in which the inconsistency was detected is also printed. + This test may catch errors that were not captured by the first two + tests if one non-deterministic automaton recognize less words than + what it should. If the input automata are deterministic or the + =--determinize= option is used, this test is redundant and can be + disabled. (In fact, the =--determinize= option implies option + =--product=0= to do so.) + 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=. @@ -909,3 +933,136 @@ be used to gather statistics about a specific set of formulas. # LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic # LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq # LocalWords: setenv concat getenv +** =--verbose= + +The verbose option can be useful to troubleshoot problems or simply +follow the list of transformations and tests performed by =ltlcross=. + +For instance here is what happens if we try to cross check =ltl2tgba= +and =ltl3ba= on the formula =FGa=. + +#+BEGIN_SRC sh :results verbatim :exports code +ltlcross -f 'FGa' ltl2tgba ltl3ba --determinize --verbose +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +ltlcross -f 'FGa' ltl2tgba ltl3ba --determinize --verbose 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +F(G(a)) +Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-vfVUzt' +Running [P1]: ltl3ba -f '<>([](a))'>'lcr-o1-IiXGfZ' +Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-T02eWu' +Running [N1]: ltl3ba -f '!(<>([](a)))'>'lcr-o1-0DpXF0' +Performing sanity checks and gathering statistics... +info: complementing non-deterministic automata via determinization... +info: P0 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P0) +info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P1) +info: getting rid of any Fin acceptance... +info: Comp(P0) (2 st.,4 ed.,2 sets) -> (3 st.,7 ed.,2 sets) +info: Comp(N0) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets) +info: Comp(P1) (2 st.,4 ed.,2 sets) -> (4 st.,9 ed.,2 sets) +info: Comp(N1) (2 st.,4 ed.,1 sets) -> (3 st.,6 ed.,1 sets) +info: check_empty P0*N0 +info: check_empty Comp(N0)*Comp(P0) +info: check_empty P0*N1 +info: check_empty P1*N0 +info: check_empty P1*N1 +info: check_empty Comp(N1)*Comp(P1) + +No problem detected. +#+end_example + +First =FGa= and its negations =!FGa= are translated with the two +tools, resulting in four automata: to positive automata =P0= and =P1= +for =FGa=, and two negative automata =N0= and =N1=. + +=ltlcross= then proceeds to compute the complement of these four +automata. Since =P0= and =P1= are nondeterministic and the +=--determinize= option was given, a first pass determinize and +complete these two automata, creating =Comp(P0)= and =Comp(P1)=. + +Apparently =N0= and =N1= are already deterministic, so their +complement could be obtained by just complementing their acceptance +condition (this is not written -- we only deduce so because they do +not appear in the list of automata that had to be determinized). + +Now that =ltlcross= has four complemented automata, it has to make +sure they use only =Inf= acceptance because that is what our emptiness +check procedure can handle. So there is a new pass over all automata, +rewriting them to get rid of any =Fin= acceptance. + +After this preparatory work, it is time for actually comparing these +automata. Together, the tests =P0*N0= and =Comp(N0)*Comp(P0)= ensure +that the automaton =N0= is really the complement of =P0=. Similarly +=P1*N1= and =Comp(N1)*Comp(P1)= ensure that =N1= is the complement of +=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: + +#+BEGIN_SRC sh :results verbatim :exports code +ltlcross -f 'FGa' ltl2tgba ltl3ba --verbose +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +ltlcross -f 'FGa' ltl2tgba ltl3ba --verbose 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +F(G(a)) +Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-YvMdzU' +Running [P1]: ltl3ba -f '<>([](a))'>'lcr-o1-Ixj7RI' +Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-uBbTbx' +Running [N1]: ltl3ba -f '!(<>([](a)))'>'lcr-o1-eo0fzl' +Performing sanity checks and gathering statistics... +info: getting rid of any Fin acceptance... +info: Comp(N0) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets) +info: Comp(N1) (2 st.,4 ed.,1 sets) -> (3 st.,6 ed.,1 sets) +info: check_empty P0*N0 +info: check_empty P0*N1 +info: check_empty Comp(N0)*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 (1 st., 2 ed.) +info: product has 200 st., 4136 ed. +info: 1 SCCs +info: building product between state-space and N1 (2 st., 4 ed.) +info: product has 400 st., 8272 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 (P0,N0), state-space #0/1 +info: consistency_check (P1,N1), state-space #0/1 + +No problem detected. +#+end_example + +In this case, =ltlcross= does not have any complement automaton for +=P0= and =P1=, so it cannot make sure that =P0= and =P1= are +equivalent. If we imagine for instance that =P0= has an empty +language, we can see that the six =check_empty= tests would still +succeed. + +So =ltlcross= builds a random state-space of 200 states, synchronize +it with the four automata, and then performs additional checks +(=cross_check= and =consistency_check=) on these products as described +[[#checks][earlier]]. While these additional checks do not make a proof that =P0= +and =P1= are equivalent, they can catch some problems, and would +easily catch the case of an automaton with an empty language by +mistake. diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test index ce2564136..cbbe54489 100755 --- a/tests/core/ltlcross.test +++ b/tests/core/ltlcross.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +# Copyright (C) 2012, 2013, 2014, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -38,7 +38,7 @@ EOF # Random formulas randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 ) | -ltlcross --products=2 \ +ltlcross -D \ "$ltl2tgba -t -f %f > %T" \ "$ltl2tgba -t -f -y %f > %T" \ "$ltl2tgba -t -f -fu %f > %T" \ diff --git a/tests/core/ltlcrossce.test b/tests/core/ltlcrossce.test index 01173fad9..0c32a8725 100755 --- a/tests/core/ltlcrossce.test +++ b/tests/core/ltlcrossce.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013 Laboratoire de Recherche et +# Copyright (C) 2013, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,8 +21,6 @@ . ./defs set -e -ltl2tgba=ltl2tgba - # The following "fake" script behaves as # version 1.5.9 of modella, when run as # 'modella -r12 -g -e %L %T' on @@ -86,7 +84,7 @@ EOF chmod +x fake run 1 ltlcross -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ - "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors + "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors cat errors grep 'error: P0\*N1 is nonempty' errors grep 'error: P1\*N0 is nonempty' errors @@ -94,3 +92,12 @@ grep 'error: P1\*N1 is nonempty' errors test `grep cycle errors | wc -l` = 3 test `grep '^error:' errors | wc -l` = 4 +run 1 ltlcross --verbose -D -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ + "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors +cat errors +test `grep 'info: Comp(' errors | wc -l` = 4 +grep 'error: P0\*N1 is nonempty' errors +grep 'error: P1\*N0 is nonempty' errors +grep 'error: P1\*N1 is nonempty' errors +test `grep cycle errors | wc -l` = 3 +test `grep '^error:' errors | wc -l` = 4