Add an is_unambiguous() function, use it in ltlcross and autfilt

* src/twaalgos/isunamb.hh, src/twaalgos/isunamb.cc: New files.
* src/twaalgos/Makefile.am: Add them.
* src/tests/unambig.test: New file.
* src/tests/Makefile.am: Add it.
* src/bin/ltlcross.cc: Record whether each produced automaton is
ambiguous.
* src/bin/autfilt.cc: Add a --is-unambiguous option.
* NEWS: Mention it.

NEWS

@@ -225,7 +225,7 @@ New in spot 1.99b (not yet released)
       new options to produce unambiguous TGBA, i.e., TGBAs in which
       every word is accepted by at most one path.  The ltl2tgba
       command line has a new option, --unambigous (or -U) to produce
-      these automata.
+      these automata, and autfilt has a --is-unambiguous filter.
 
   * Noteworthy code changes
 

src/bin/autfilt.cc

@@ -39,6 +39,7 @@
 #include "twaalgos/product.hh"
 #include "twaalgos/isdet.hh"
 #include "twaalgos/stutter.hh"
+#include "twaalgos/isunamb.hh"
 #include "misc/optionmap.hh"
 #include "misc/timer.hh"
 #include "misc/random.hh"
@@ -80,6 +81,7 @@ enum {
   OPT_IS_COMPLETE,
   OPT_IS_DETERMINISTIC,
   OPT_IS_EMPTY,
+  OPT_IS_UNAMBIGUOUS,
   OPT_KEEP_STATES,
   OPT_MASK_ACC,
   OPT_MERGE,
@@ -179,6 +181,8 @@ static const argp_option options[] =
       "keep deterministic automata", 0 },
     { "is-empty", OPT_IS_EMPTY, 0, 0,
       "keep automata with an empty language", 0 },
+    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, 0, 0,
+      "keep only unambiguous automata", 0 },
     { "intersect", OPT_INTERSECT, "FILENAME", 0,
       "keep automata whose languages have an non-empty intersection with"
       " the automaton from FILENAME", 0 },
@@ -234,6 +238,7 @@ static struct opt_t
 static bool opt_merge = false;
 static bool opt_is_complete = false;
 static bool opt_is_deterministic = false;
+static bool opt_is_unambiguous = false;
 static bool opt_invert = false;
 static range opt_states = { 0, std::numeric_limits<int>::max() };
 static range opt_edges = { 0, std::numeric_limits<int>::max() };
@@ -344,6 +349,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_IS_EMPTY:
       opt_is_empty = true;
       break;
+    case OPT_IS_UNAMBIGUOUS:
+      opt_is_unambiguous = true;
+      break;
     case OPT_MERGE:
       opt_merge = true;
       break;
@@ -522,6 +530,10 @@ namespace
 	matched &= is_complete(aut);
       if (opt_is_deterministic)
 	matched &= is_deterministic(aut);
+      if (opt_is_deterministic)
+	matched &= is_deterministic(aut);
+      else if (opt_is_unambiguous)
+	matched &= is_unambiguous(aut);
       if (opt->are_isomorphic)
         matched &= opt->isomorphism_checker->is_isomorphic(aut);
       if (opt_is_empty)

src/bin/ltlcross.cc

@@ -59,6 +59,7 @@
 #include "misc/formater.hh"
 #include "twaalgos/stats.hh"
 #include "twaalgos/isdet.hh"
+#include "twaalgos/isunamb.hh"
 #include "misc/escape.hh"
 #include "misc/hash.hh"
 #include "misc/random.hh"
@@ -293,6 +294,7 @@ struct statistics
   std::vector<double> product_states;
   std::vector<double> product_transitions;
   std::vector<double> product_scc;
+  bool ambiguous;
 
   static void
   fields(std::ostream& os, bool show_exit, bool show_sr)
@@ -316,7 +318,8 @@ struct statistics
 	   "\"nondet_aut\","
 	   "\"terminal_aut\","
 	   "\"weak_aut\","
-	   "\"strong_aut\"");
+	   "\"strong_aut\","
+	   "\"ambiguous_aut\"");
     size_t m = products_avg ? 1U : products;
     for (size_t i = 0; i < m; ++i)
       os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
@@ -353,7 +356,8 @@ struct statistics
 	   << nondeterministic << ','
 	   << terminal_aut << ','
 	   << weak_aut << ','
-	   << strong_aut;
+	   << strong_aut << ','
+	   << ambiguous;
 	if (!products_avg)
 	  {
 	    for (size_t i = 0; i < products; ++i)
@@ -381,7 +385,7 @@ struct statistics
       {
 	size_t m = products_avg ? 1U : products;
 	m *= 3;
-	m += 13 + show_sr * 6;
+	m += 14 + show_sr * 6;
 	os << na;
 	for (size_t i = 0; i < m; ++i)
 	  os << ',' << na;
@@ -688,6 +692,7 @@ namespace
 		st->weak_aut = true;
 	      else
 		st->terminal_aut = true;
+	      st->ambiguous = !spot::is_unambiguous(res);
 	    }
 	}
       output.cleanup();

src/tests/Makefile.am

@@ -211,6 +211,7 @@ TESTS_twa = \
   babiak.test \
   monitor.test \
   dra2dba.test \
+  unambig.test \
   ltlcross4.test \
   ltl2dstar.test \
   ltl2dstar2.test \

src/tests/unambig.test

@@ -0,0 +1,84 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
+# de l'Epita
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+ltl2tgba=../../bin/ltl2tgba
+autfilt=../../bin/autfilt
+
+for f in 'Ga' \
+         'Ga | Gb' \
+         'Ga | GFb' \
+         'Ga | FGb' \
+         'XFGa | GFb | Gc' \
+         '(Ga -> Gb) W c' \
+	 'F(a & !b & (!c W b))'
+do
+  $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
+  $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous
+done
+
+for f in FGa
+do
+  $ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous
+  $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
+done
+
+# All these should be detected as ambiguous automata
+cat >input<<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 0
+[1] 0
+[0&1] 0 {0}
+--END--
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 2 Inf(0) & Inf(1)
+--BODY--
+State: 0
+[0] 0
+[1] 0 {0}
+[0&1] 0 {0 1}
+--END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 1 {0}
+[1] 1
+State: 1
+[0] 1 {0}
+--END--
+EOF
+
+run 1 $autfilt -q --is-unambiguous input

src/twaalgos/Makefile.am

@@ -46,6 +46,7 @@ twaalgos_HEADERS = \
   gv04.hh \
   hoa.hh \
   isdet.hh \
+  isunamb.hh \
   isweakscc.hh \
   lbtt.hh \
   ltl2taa.hh \
@@ -101,6 +102,7 @@ libtwaalgos_la_SOURCES = \
   gv04.cc \
   hoa.cc \
   isdet.cc \
+  isunamb.cc \
   isweakscc.cc \
   lbtt.cc \
   ltl2taa.cc \

src/twaalgos/isunamb.cc

@@ -0,0 +1,40 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "isunamb.hh"
+#include "twaalgos/product.hh"
+#include "sccfilter.hh"
+#include "stats.hh"
+#include <set>
+#include <list>
+
+namespace spot
+{
+  bool is_unambiguous(const const_twa_graph_ptr& aut)
+  {
+    if (aut->is_deterministic())
+      return true;
+    auto clean_a = scc_filter_states(aut);
+    auto prod = product(clean_a, clean_a);
+    auto clean_p = scc_filter_states(prod);
+    tgba_statistics sa = stats_reachable(clean_a);
+    tgba_statistics sp = stats_reachable(clean_p);
+    return sa.states == sp.states && sa.transitions == sp.transitions;
+  }
+}

src/twaalgos/isunamb.hh

@@ -0,0 +1,44 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include "twa/twagraph.hh"
+
+namespace spot
+{
+  class tgba;
+
+  /// \addtogroup tgba_misc
+  /// @{
+
+  /// \brief Whether the automaton \a aut is unambiguous.
+  ///
+  /// An automaton is unambiguous if each accepted word is
+  /// recognized by only one path.
+  ///
+  /// We check unambiguousity by synchronizing the automaton with
+  /// itself, and then making sure that the co-reachable part of the
+  /// squared automaton has the same size as the co-reachable part of
+  /// the original automaton.
+  SPOT_API bool
+  is_unambiguous(const const_twa_graph_ptr& aut);
+
+  /// @}
+}