Merge branch 'master' into next

* configure.ac, NEWS: Bump version to 1.99a at the same time.

NEWS

@@ -1,4 +1,4 @@
-New in spot 1.2.5a (not yet released)
+New in spot 1.99a (not yet released)
 
   * Major changes (including backward incompatible changes):
 
@@ -87,6 +87,25 @@ New in spot 1.2.5a (not yet released)
       automata (when viewed explictely), using the above and non
       longuer supported tgba_bdd_concrete class.
 
+New in spot 1.2.5a (not yet released)
+
+  * New features:
+
+    - ltlcross --verbose is a new option to see what is being done
+
+  * Bug fixes:
+
+    - When the automaton resulting from the translation of a positive
+      formula is deterministic, ltlcross will compute its complement
+      to perform additional checks against other translations of the
+      positive formula.  The same procedure should be performed with
+      automata obtained from negated formulas, but because of a typo
+      this was not the case.
+    - the neverclaim parser will now diagnose redefinitions of
+      state labels.
+    - the acceptance specification in the HOA format output have been
+      adjusted to match recent changes in the format specifications.
+
 New in spot 1.2.5 (2014-08-21)
 
   * New features:

configure.ac

@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.61])
-AC_INIT([spot], [1.2.5a], [spot@lrde.epita.fr])
+AC_INIT([spot], [1.99a], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])

doc/org/ltlcross.org

@@ -136,11 +136,11 @@ tools:
   - '=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 %D='
+  - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D='
     (deterministic Rabin output)
-  - '=ltl2dstar --automata=streett --ltl2nba=spin:path/tp/ltl2tgba@-sD
+  - '=ltl2dstar --automata=streett --ltl2nba=spin:path/to/ltl2tgba@-sD
     %L %D=' (deterministic Streett output)
-  - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L - | dstar2tgba
+  - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba
     -s >%N=' (external conversion from Rabin to Büchi done by
     =dstar2tgba= for more reduction of the Büchi automaton than
     what =ltlcross= would provide)

src/bin/ltlcross.cc

@@ -96,6 +96,7 @@ Exit status:\n\
 #define OPT_NOCOMP 11
 #define OPT_OMIT 12
 #define OPT_BOGUS 13
+#define OPT_VERBOSE 14
 
 static const argp_option options[] =
   {
@@ -163,6 +164,8 @@ static const argp_option options[] =
       "'auto' (the default if --color is not used)", 0 },
     { "save-bogus", OPT_BOGUS, "FILENAME", 0,
       "save formulas for which problems were detected in FILENAME", 0 },
+    { "verbose", OPT_VERBOSE, 0, 0,
+      "print what is being done, for debugging", 0 },
     { 0, 0, 0, 0, 0, 0 }
   };
 
@@ -212,6 +215,7 @@ bool opt_omit = false;
 bool has_sr = false; // Has Streett or Rabin automata to process.
 const char* bogus_output_filename = 0;
 std::ofstream* bogus_output = 0;
+bool verbose = false;
 
 struct translator_spec
 {
@@ -572,6 +576,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_STOP_ERR:
       stop_on_error = true;
       break;
+    case OPT_VERBOSE:
+      verbose = true;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }
@@ -983,22 +990,24 @@ namespace
 		  }
 		else
 		  {
+		    const char* type = 0;
+		    switch (aut->type)
+		      {
+		      case spot::Rabin:
+			type = "DRA";
+			break;
+		      case spot::Streett:
+			type = "DSA";
+			break;
+		      }
+		    assert(type);
+
 		    // Gather statistics about the input automaton
 		    if (want_stats)
 		      {
 			statistics* st = &(*fstats)[translator_num];
 			st->has_in = true;
-
-			switch (aut->type)
-			  {
-			  case spot::Rabin:
-			    st->in_type = "DRA";
-			    break;
-			  case spot::Streett:
-			    st->in_type = "DSA";
-			    break;
-			  }
-
+			st->in_type = type;
 			spot::tgba_sub_statistics s =
 			  sub_stats_reachable(aut->aut);
 			st->in_states= s.states;
@@ -1009,6 +1018,8 @@ namespace
 			st->in_scc = spot::scc_info(aut->aut).scc_count();
 		      }
 		    // convert it into TGBA for further processing
+		    if (verbose)
+		      std::cerr << "info: converting " << type << " to TGBA\n";
 		    res = dstar_to_tgba(aut);
 		  }
 		break;
@@ -1029,6 +1040,8 @@ namespace
 	  // Compute statistics.
 	  if (res)
 	    {
+	      if (verbose)
+		std::cerr << "info: getting statistics\n";
 	      st->ok = true;
 	      spot::tgba_sub_statistics s = sub_stats_reachable(res);
 	      st->states = s.states;
@@ -1072,6 +1085,21 @@ namespace
   {
     auto prod = spot::product(aut_i, aut_j);
     auto res = spot::couvreur99(prod)->check();
+
+    if (verbose)
+      {
+	std::cerr << "info: check_empty ";
+	if (icomp)
+	  std::cerr << "Comp(N" << i << ')';
+	else
+	  std::cerr << 'P' << i;
+	if (jcomp)
+	  std::cerr << "*Comp(P" << j << ')';
+	else
+	  std::cerr << "*N" << j;
+	std::cerr << '\n';
+      }
+
     if (res)
       {
 	std::ostream& err = global_error();
@@ -1109,6 +1137,20 @@ namespace
   cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
   {
     size_t m = maps.size();
+    if (verbose)
+      {
+	std::cerr << "info: cross_check {";
+	bool first = true;
+	for (size_t i = 0; i < m; ++i)
+	  {
+	    if (first)
+	      first = false;
+	    else
+	      std::cerr << ',';
+	    std::cerr << l << i;
+	  }
+	std::cerr << "}, state-space #" << p << '/' << products << '\n';
+      }
 
     std::vector<bool> res(m);
     unsigned verified = 0;
@@ -1418,7 +1460,7 @@ namespace
 		      problems +=
 			check_empty_prod(pos[i], comp_pos[j],
 					 i, j, false, true);
-		    if (i != j && comp_neg[i] && !comp_neg[i])
+		    if (i != j && comp_neg[i] && !comp_pos[i])
 		      problems +=
 			check_empty_prod(comp_neg[i], neg[j],
 					 i, j, true, false);
@@ -1454,6 +1496,11 @@ namespace
 	{
 	  // build a random state-space.
 	  spot::srand(seed);
+
+	  if (verbose)
+	    std::cerr << "info: building state-space #" << p << '/' << products
+		      << " with seed " << seed << '\n';
+
 	  auto statespace = spot::random_graph(states, density, ap, dict);
 
 	  // Products of the state space with the positive automata.
@@ -1510,8 +1557,14 @@ namespace
 
 	      // consistency check
 	      for (size_t i = 0; i < m; ++i)
-		if (pos_map[i] && neg_map[i] &&
-		    !(consistency_check(pos_map[i], neg_map[i], statespace)))
+		if (pos_map[i] && neg_map[i])
+		  {
+		    if (verbose)
+		      std::cerr << "info: consistency_check (P" << i
+				<< ",N" << i << "), state-space #"
+				<< p << '/' << products << '\n';
+		    if (!(consistency_check(pos_map[i], neg_map[i],
+					    statespace)))
 		      {
 			++problems;
 
@@ -1526,6 +1579,7 @@ namespace
 			end_error();
 		      }
 		  }
+	    }
 
 	  // Cleanup.
 	  if (!no_checks)
@@ -1549,6 +1603,9 @@ namespace
 static void
 print_stats_csv(const char* filename)
 {
+  if (verbose)
+    std::cerr << "info: writing CSV to " << filename << '\n';
+
   std::ofstream* outfile = 0;
   std::ostream* out;
   if (!strncmp(filename, "-", 2))
@@ -1587,6 +1644,9 @@ print_stats_csv(const char* filename)
 static void
 print_stats_json(const char* filename)
 {
+  if (verbose)
+    std::cerr << "info: writing JSON to " << filename << '\n';
+
   std::ofstream* outfile = 0;
   std::ostream* out;
   if (!strncmp(filename, "-", 2))

src/neverparse/neverclaimparse.yy

@@ -69,6 +69,7 @@
 using namespace spot::ltl;
 static bool accept_all_needed = false;
 static bool accept_all_seen = false;
+static std::map<std::string, spot::location> labels;
 }
 
 %token NEVER "never"
@@ -88,7 +89,7 @@ static bool accept_all_seen = false;
 %type <str> opt_dest formula_or_ident
 %type <p> transition src_dest
 %type <list> transitions transition_block
-%type <str> ident_list
+%type <str> one_ident ident_list
 
 
 %destructor { delete $$; } <str>
@@ -118,13 +119,22 @@ states:
   | states ';' state
   | states ';'
 
-ident_list:
-    IDENT ':'
+one_ident: IDENT ':'
     {
       namer->new_state(*$1);
+      std::pair<std::map<std::string, spot::location>::const_iterator, bool>
+	res = labels.insert(std::make_pair(*$1, @1));
+      if (!res.second)
+	{
+	  error(@1, std::string("redefinition of ") + *$1 + "...");
+	  error(res.first->second, std::string("... ")  + *$1 + " previously defined here");
+	}
       $$ = $1;
     }
-  | ident_list IDENT ':'
+
+
+ident_list: one_ident
+  | ident_list one_ident
     {
       namer->alias_state(namer->get_state(*$1), *$2);
       // Keep any identifier that starts with accept.
@@ -319,6 +329,7 @@ namespace spot
       }
     accept_all_needed = false;
     accept_all_seen = false;
+    labels.clear();
 
     delete namer;
     return result;

src/tgbaalgos/hoaf.cc

@@ -276,9 +276,9 @@ namespace spot
     os << "Acceptance: " << num_acc;
     if (num_acc > 0)
       {
-	os << " I(0";
+	os << " Inf(0";
 	for (unsigned i = 1; i < num_acc; ++i)
-	  os << ")&I(" << i;
+	  os << ")&Inf(" << i;
 	os << ')';
       }
     else

src/tgbatest/ltl2dstar.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -61,3 +61,17 @@ grep '"in_type"' out.csv
 grep '"DSA"' out.csv
 grep '"DRA"' out.csv
 grep ',,,,' out.csv
+
+
+# A bug in ltlcross <=1.2.5 caused it to not use the complement of the
+# negative automaton.  So running ltlcross with GFa would check one
+# complement (the positive one), but running with FGa would ignore
+# the negative complement.
+$ltlcross -f 'GFa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+test `grep -c 'info: check_empty.*Comp' err` = 1
+$ltlcross -f 'FGa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+test `grep -c 'info: check_empty.*Comp' err` = 1

src/tgbatest/neverclaimread.test

@@ -169,7 +169,7 @@ run 2 ../ltl2tgba -XN input > stdout 2>stderr
 cat >expected <<\EOF
 input:9.16: syntax error, unexpected $undefined, expecting fi or ':'
 EOF
-grep input: stderr >> stderrfilt
+grep input: stderr > stderrfilt
 diff stderrfilt expected
 
 
@@ -206,6 +206,87 @@ run 0 ../ltl2tgba -ks -XN input > output
 diff output expected
 
 
+# Test duplicated labels.  The following neverclaim was produced by
+# ltl2ba 1.1 for '[](<>[]p1 U X[]<>Xp0)', but is rejected by Spin
+# because of a duplicate label (accept_S10).  We should
+# complain as well.  This was reported by Joachim Klein.
+
+cat >input <<\EOF
+never { /* [](<>[]p1 U X[]<>Xp0) */
+T0_init:
+	if
+	:: (1) -> goto accept_S2
+	:: (1) -> goto T1_S3
+	:: (p1) -> goto T2_S4
+	fi;
+accept_S2:
+	if
+	:: (1) -> goto accept_S39
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto accept_S10
+	fi;
+accept_S39:
+	if
+	:: (p0) -> goto accept_S39
+	:: (1) -> goto T0_S39
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S39:
+	if
+	:: (p0) -> goto accept_S39
+	:: (1) -> goto T0_S39
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S24:
+	if
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S10:
+	if
+	:: (p0 && p1) -> goto accept_S10
+	:: (p1) -> goto T0_S10
+	fi;
+accept_S10:
+	if
+	:: (p0 && p1) -> goto accept_S10
+	:: (p1) -> goto T0_S10
+	fi;
+T1_S24:
+	if
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto accept_S10
+	fi;
+accept_S10:
+	if
+	:: (p1) -> goto accept_S10
+	fi;
+T1_S3:
+	if
+	:: (1) -> goto T1_S3
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto T2_S4
+	:: (p1) -> goto accept_S10
+	fi;
+T2_S4:
+	if
+	:: (p1) -> goto T2_S4
+	:: (p1) -> goto accept_S10
+	fi;
+}
+EOF
+
+run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
+cat stderr
+cat >expected-err <<\EOF
+input:48.1-10: redefinition of accept_S10...
+input:38.1-10: ... accept_S10 previously defined here
+EOF
+grep input: stderr > stderrfilt
+diff stderrfilt expected-err
+
 cat >formulae<<EOF
 a
 FG a