From fafb135c87fbbd6ec64d54402efd39b304eea092 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 13 Jul 2016 15:09:32 +0200
Subject: [PATCH] isdet: update prop_deterministic in count_nondet_states()

* spot/twaalgos/isdet.cc: Here.
* bin/ltlcross.cc: Simplify.
* NEWS: Update.
---
 NEWS                   |  5 +++--
 bin/ltlcross.cc        | 16 ++++------------
 spot/twaalgos/isdet.cc |  8 +++++---
 3 files changed, 12 insertions(+), 17 deletions(-)

diff --git a/NEWS b/NEWS
index af80b72c3..d476b16ac 100644
--- a/NEWS
+++ b/NEWS
@@ -55,8 +55,9 @@ New in spot 2.0.3a (not yet released)
     future.
 
   * is_deterministic(), is_terminal(), is_weak(), and
-    is_inherently_weak() will update the corresponding properties of
-    the automaton as a side-effect of their check.
+    is_inherently_weak(), count_nondet_states() will update the
+    corresponding properties of the automaton as a side-effect of
+    their check.
 
   * language_containment_checker now has default values for all
     parameters of its constructor.
diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index e44fbef89..c1160fe0c 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -1008,12 +1008,8 @@ namespace
           problems += prob;
 
           // If the automaton is deterministic, compute its complement
-          // as well.  Note that if we have computed statistics
-          // already, there is no need to call is_deterministic()
-          // again.
-          if (!no_complement && pos[n]
-              && ((want_stats && !(*pstats)[n].nondeterministic)
-                  || (!want_stats && is_deterministic(pos[n]))))
+          // as well.
+          if (!no_complement && pos[n] && is_deterministic(pos[n]))
             comp_pos[n] = dtwa_complement(pos[n]);
         }
 
@@ -1048,12 +1044,8 @@ namespace
               problems += prob;
 
               // If the automaton is deterministic, compute its
-              // complement as well.  Note that if we have computed
-              // statistics already, there is no need to call
-              // is_deterministic() again.
-              if (!no_complement && neg[n]
-                  && ((want_stats && !(*nstats)[n].nondeterministic)
-                      || (!want_stats && is_deterministic(neg[n]))))
+              // complement as well.
+              if (!no_complement && neg[n] && is_deterministic(neg[n]))
                 comp_neg[n] = dtwa_complement(neg[n]);
             }
         }
diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc
index afae5348b..72897cff0 100644
--- a/spot/twaalgos/isdet.cc
+++ b/spot/twaalgos/isdet.cc
@@ -50,6 +50,8 @@ namespace spot
           if (!count && nondet_states)
             break;
         }
+      std::const_pointer_cast<twa_graph>(aut)
+        ->prop_deterministic(!nondet_states);
       return nondet_states;
     }
   }
@@ -57,6 +59,8 @@ namespace spot
   unsigned
   count_nondet_states(const const_twa_graph_ptr& aut)
   {
+    if (aut->prop_deterministic())
+      return 0;
     return count_nondet_states_aux<true>(aut);
   }
 
@@ -66,9 +70,7 @@ namespace spot
     trival d = aut->prop_deterministic();
     if (d.is_known())
       return d.is_true();
-    bool res = !count_nondet_states_aux<false>(aut);
-    std::const_pointer_cast<twa_graph>(aut)->prop_deterministic(res);
-    return res;
+    return !count_nondet_states_aux<false>(aut);
   }
 
   bool