isdet: simplify is_deterministic(), add is_complete().

* src/tgbaalgos/isdet.cc: Simplify determinism check.
* src/tgbaalgos/isdet.hh, src/tgbaalgos/isdet.cc (is_complete): New
function.
* src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/bin/dstar2tgba.cc
src/bin/ltl2tgba.cc: Add escape sequence %p to the possible statistics
to show whether an automaton is complete.
* src/tgbatest/nondet.test: Add a couple more tests.

NEWS

@@ -53,6 +53,9 @@ New in spot 1.1.4a (not relased)
       This makes it more homogeneous with the --stats option of the
       new dstar2tgba command.
 
+      Additionally, the %p escape can now be used to show whether the
+      output automaton is complete.
+
   * All the parsers implemented in Spot now use the same type
     to store locations.
 

src/bin/dstar2tgba.cc

@@ -100,6 +100,8 @@ static const argp_option options[] =
       "number of nondeterministic states in output", 0 },
     { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "1 if the output is deterministic, 0 otherwise", 0 },
+    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+      "1 if the output is complete, 0 otherwise", 0 },
     { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "a single %", 0 },
     /**************************************************/

src/bin/ltl2tgba.cc

@@ -91,6 +91,8 @@ static const argp_option options[] =
       "number of nondeterministic states", 0 },
     { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "1 if the automaton is deterministic, 0 otherwise", 0 },
+    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+      "1 if the automaton is complete, 0 otherwise", 0 },
     { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "a single %", 0 },
     /**************************************************/

src/tgbaalgos/isdet.cc

 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -30,10 +30,9 @@ namespace spot
     count_nondet_states_aux(const tgba* aut, bool count = true)
     {
       unsigned res = 0;
-      typedef std::set<const state*, state_ptr_less_than> seen_set;
       typedef std::deque<const state*> todo_list;
 
-      seen_set seen;
+      state_set seen;
       todo_list todo;
       {
 	const state* s = aut->get_init_state();
@@ -46,9 +45,8 @@ namespace spot
 	  todo.pop_front();
 
 	  tgba_succ_iterator* i = aut->succ_iter(src);
-	  tgba_succ_iterator* j = aut->succ_iter(src);
-	  unsigned in = 0;
 	  bool nondeterministic = false;
+	  bdd available = bddtrue;
 	  for (i->first(); !i->done(); i->next())
 	    {
 	      // If we know the state is nondeterministic, just skip the
@@ -57,22 +55,11 @@ namespace spot
 	      // destination states.
 	      if (!nondeterministic)
 		{
-		  ++in;
-		  // Move j to the transition that follows i.
-		  j->first();
-		  for (unsigned jn = 0; jn < in; ++jn)
-		    j->next();
-		  // Make sure transitions after i are not conflicting.
-		  while (!j->done())
-		    {
-		      if ((i->current_condition() & j->current_condition())
-			  != bddfalse)
-			{
-			  nondeterministic = true;
-			  break;
-			}
-		      j->next();
-		    }
+		  bdd label = i->current_condition();
+		  if (!bdd_implies(label, available))
+		    nondeterministic = true;
+		  else
+		    available -= label;
 		}
 	      const state* dst = i->current_state();
 	      if (seen.insert(dst).second)
@@ -80,13 +67,12 @@ namespace spot
 	      else
 		dst->destroy();
 	    }
-	  delete j;
 	  delete i;
 	  res += nondeterministic;
 	  if (!count && nondeterministic)
 	    break;
 	}
-      for (seen_set::const_iterator i = seen.begin(); i != seen.end();)
+      for (state_set::const_iterator i = seen.begin(); i != seen.end();)
 	{
 	  const state* s = *i++;
 	  s->destroy();
@@ -106,4 +92,47 @@ namespace spot
   {
     return !count_nondet_states_aux(aut, false);
   }
+
+  bool
+  is_complete(const tgba* aut)
+  {
+    state_set seen;
+    typedef std::deque<const state*> todo_list;
+    todo_list todo;
+    bool complete = true;
+    {
+      const state* s = aut->get_init_state();
+      seen.insert(s);
+      todo.push_back(s);
+    }
+    while (!todo.empty())
+      {
+	const state* src = todo.front();
+	todo.pop_front();
+
+	tgba_succ_iterator* i = aut->succ_iter(src);
+	bdd available = bddtrue;
+	for (i->first(); !i->done(); i->next())
+	  {
+	    available -= i->current_condition();
+	    const state* dst = i->current_state();
+	    if (seen.insert(dst).second)
+	      todo.push_back(dst);
+	    else
+	      dst->destroy();
+	  }
+	delete i;
+	if (available != bddfalse)
+	  {
+	    complete = false;
+	    break;
+	  }
+      }
+    for (state_set::const_iterator i = seen.begin(); i != seen.end();)
+      {
+	const state* s = *i++;
+	s->destroy();
+      }
+    return complete;
+  }
 }

src/tgbaalgos/isdet.hh

@@ -43,6 +43,13 @@ namespace spot
   SPOT_API bool
   is_deterministic(const tgba* aut);
 
+  /// \Brief Return true iff \a aut is complete.
+  ///
+  /// An automaton is complete if its translation relation is total,
+  /// i.e., each state as a successor for any possible configuration.
+  SPOT_API bool
+  is_complete(const tgba* aut);
+
   /// @}
 }
 

src/tgbaalgos/stats.cc

@@ -147,6 +147,7 @@ namespace spot
     declare('e', &edges_);
     declare('f', &form_);
     declare('n', &nondetstates_);
+    declare('p', &complete_);
     declare('s', &states_);
     declare('S', &scc_);	// Historical.  Deprecated.  Use %c instead.
     declare('t', &trans_);
@@ -195,6 +196,11 @@ namespace spot
 	deterministic_ = is_deterministic(aut);
       }
 
+    if (has('p'))
+      {
+	complete_ = is_complete(aut);
+      }
+
     return format(format_);
   }
 

src/tgbaalgos/stats.hh

@@ -98,6 +98,7 @@ namespace spot
     printable_value<unsigned> scc_;
     printable_value<unsigned> nondetstates_;
     printable_value<unsigned> deterministic_;
+    printable_value<unsigned> complete_;
   };
 
   /// @}

src/tgbatest/nondet.test

 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -21,13 +21,17 @@
 . ./defs
 set -e
 
-../../bin/ltl2tgba FGa GFa --stats='%f %d' >out.1
 cat >expected.1<<EOF
-FGa 0
-GFa 1
+FGa, 0 0
+GFa, 1 1
+a U b, 1 0
+G(Fa | !r) | Fx, 0 1
 EOF
 
-cmp out.1 expected.1
+cut -d, -f1 expected.1 |
+../../bin/ltl2tgba -F- --stats='%f, %d %p' >out.1
+
+diff out.1 expected.1
 
 ../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s' >out.2
 cat >expected.2<<EOF
@@ -35,4 +39,4 @@ FGa 0 1 2
 GFa 1 0 1
 EOF
 
-cmp out.2 expected.2
+diff out.2 expected.2