ltlcross: add option --determinize

* bin/ltlcross.cc: Implement it.
* doc/org/ltlcross.org, NEWS: Document it.
* tests/core/ltlcross.test, tests/core/ltlcrossce.test: Test it.

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

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 <spot/twaalgos/stats.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/isunamb.hh>
+#include <spot/twaalgos/postproc.hh>
 #include <spot/misc/escape.hh>
 #include <spot/misc/hash.hh>
 #include <spot/misc/random.hh>
@@ -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<spot::formula> 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)
+	  auto printsize = [](const spot::const_twa_graph_ptr& aut)
-	    std::cerr << "info: getting rid of any Fin acceptance...\n";
+	    {
+	      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<spot::twa_graph_ptr>& from,
+			     std::vector<spot::twa_graph_ptr>& 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<spot::twa_graph_ptr>& 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])					\
+	      tmp(pos, i, "     P", " ");
-		{							\
+	      tmp(neg, i, "     N", " ");
-		  cleanup_acceptance_here(x[i]);			\
+	      tmp(comp_pos, i, "Comp(P", ")");
-		  if (x[i]->acc().uses_fin_acceptance())		\
+	      tmp(comp_neg, i, "Comp(N", ")");
-		    {							\
-	              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
 	    }
 
 	  // intersection test

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
+  - additional intersection checks with the complement, allowing
-    deterministic automaton produced by a translator.
+    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
+    By default this check is only done for deterministic automata,
-    complementation is cheap is that case.  When validating a
+    because complementation is relatively cheap is that case (at least
-    translator with =ltlcross=, we highly recommend to include a
+    it is cheap for simple acceptance conditions).  Using option
-    translator with good deterministic output to augment test
+    =--determinize=, =ltlcross= can be instructed to perform
-    coverage.  Using '=ltl2tgba -lD %f >%O=' will produce
+    complementation of non-deterministic automata as well, ensuring
-    deterministic automata for all obligation properties and many
+    precise equivalence checks between all automata.  However be aware
-    recurrence properties.  Using '=ltl2dstar
+    that this determinization + complementation may generate large
-    --ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will systematically
+    automata.
-    produce a deterministic Rabin automaton (that =ltlcross= can
+
-    complement easily).
+    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.

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" \

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