From 4f0a630dbc8fde63232c551111be20b1db9f47bf Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 17 Aug 2016 14:17:37 +0200
Subject: [PATCH] stats: preparatory change of the implementation of %c

This now holds the scc_info while processing the %c sequence, so that
using options we will soon be able to specify which SCC to count.

* spot/twaalgos/stats.hh, spot/twaalgos/stats.cc (printable_scc_info):
New class.
(state_printer): Use it for %c.
* spot/misc/formater.hh: Add move assignment.
* bin/common_aoutput.hh, bin/common_aoutput.cc: Use printable_scc_info
for %C.
* tests/core/format.test: Add a quick test case to make sure nothing
changed.
---
 bin/common_aoutput.cc  |  3 ++-
 bin/common_aoutput.hh  |  2 +-
 spot/misc/formater.hh  |  7 +++++++
 spot/twaalgos/stats.cc | 16 ++++++++++++++--
 spot/twaalgos/stats.hh | 21 ++++++++++++++++++++-
 tests/core/format.test |  3 +++
 6 files changed, 47 insertions(+), 5 deletions(-)

diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 0031af1ea..46b6ad6fd 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -406,7 +406,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
         haut_acc_ = haut->aut->acc().num_sets();
 
       if (has('C'))
-        haut_scc_ = spot::scc_info(haut->aut).scc_count();
+        haut_scc_.automaton(haut->aut);
 
       if (has('N'))
         {
@@ -471,6 +471,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
   // automata are built.
   output_aut_ = nullptr;
   input_aut_ = nullptr;
+  haut_scc_.reset();
   return res;
 }
 
diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh
index b07e064e7..008fc9c09 100644
--- a/bin/common_aoutput.hh
+++ b/bin/common_aoutput.hh
@@ -111,7 +111,7 @@ private:
   spot::printable_value<unsigned> haut_edges_;
   spot::printable_value<unsigned> haut_trans_;
   spot::printable_value<unsigned> haut_acc_;
-  spot::printable_value<unsigned> haut_scc_;
+  spot::printable_scc_info haut_scc_;
   spot::printable_value<unsigned> haut_deterministic_;
   spot::printable_value<unsigned> haut_nondetstates_;
   spot::printable_value<unsigned> haut_complete_;
diff --git a/spot/misc/formater.hh b/spot/misc/formater.hh
index e20ebd318..d1edc985a 100644
--- a/spot/misc/formater.hh
+++ b/spot/misc/formater.hh
@@ -71,6 +71,13 @@ namespace spot
       return *this;
     }
 
+    printable_value&
+    operator=(T&& new_val)
+    {
+      val_ = std::move(new_val);
+      return *this;
+    }
+
     virtual void
     print(std::ostream& os, const char*) const override
     {
diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc
index e661e9252..64cffef3b 100644
--- a/spot/twaalgos/stats.cc
+++ b/spot/twaalgos/stats.cc
@@ -123,6 +123,12 @@ namespace spot
     print_psl(os, val_);
   };
 
+  void printable_scc_info::print(std::ostream& os, const char*) const
+  {
+    os << val_->scc_count();
+  };
+
+
   stat_printer::stat_printer(std::ostream& os, const char* format)
     : format_(format)
   {
@@ -167,8 +173,12 @@ namespace spot
     if (has('a'))
       acc_ = aut->num_sets();
 
+    // %S was renamed to %c in Spot 1.2, so that autfilt could use %S
+    // and %s to designate the state numbers in input and output
+    // automate.  We still recognize %S an obsolete and undocumented
+    // alias for %c, if it is not overridden by a subclass.
     if (has('c') || has('S'))
-      scc_ = scc_info(aut).scc_count();
+      scc_.automaton(aut);
 
     if (has('n'))
       {
@@ -193,7 +203,9 @@ namespace spot
         gen_acc_ = os.str();
       }
 
-    return format(format_);
+    auto& os = format(format_);
+    scc_.reset(); // Make sure we do not hold a pointer to the automaton
+    return os;
   }
 
 }
diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh
index 688d5c3b7..5373a404a 100644
--- a/spot/twaalgos/stats.hh
+++ b/spot/twaalgos/stats.hh
@@ -23,6 +23,7 @@
 #pragma once
 
 #include <spot/twa/twa.hh>
+#include <spot/twaalgos/sccinfo.hh>
 #include <iosfwd>
 #include <spot/misc/formater.hh>
 
@@ -69,6 +70,24 @@ namespace spot
     print(std::ostream& os, const char*) const override;
   };
 
+  class SPOT_API printable_scc_info final:
+    public spot::printable
+  {
+    std::unique_ptr<scc_info> val_;
+  public:
+    void automaton(const const_twa_graph_ptr& aut)
+    {
+      val_ = std::unique_ptr<scc_info>(new scc_info(aut));
+    }
+
+    void reset()
+    {
+      val_ = nullptr;
+    }
+
+    void print(std::ostream& os, const char* pos) const override;
+  };
+
   /// \brief prints various statistics about a TGBA
   ///
   /// This object can be configured to display various statistics
@@ -95,7 +114,7 @@ namespace spot
     printable_value<unsigned> edges_;
     printable_value<unsigned> trans_;
     printable_value<unsigned> acc_;
-    printable_value<unsigned> scc_;
+    printable_scc_info scc_;
     printable_value<unsigned> nondetstates_;
     printable_value<unsigned> deterministic_;
     printable_value<unsigned> complete_;
diff --git a/tests/core/format.test b/tests/core/format.test
index 9463a425d..ce56666ab 100644
--- a/tests/core/format.test
+++ b/tests/core/format.test
@@ -56,3 +56,6 @@ test "$out" = "cycle{a},cycle{!a}"
 test "0,1,0,1" = "`ltl2tgba FGa | autfilt -D --stats='%D,%d,%P,%p'`"
 test "0,0,0,1" = "`ltl2tgba FGa | autfilt -C --stats='%D,%d,%P,%p'`"
 test "1,0" = "`ltl2tgba FGa | autfilt -D --stats='%N,%n'`"
+
+test "4" = "`ltl2tgba '(Ga -> Gb)W c' --stats=%c`"
+test "4,5" = "`ltl2tgba '(Ga -> Gb)W c' | autfilt -C --stats=%C,%c`"