From 1cf5778faaad9a3669a6b2e1ff9f6f80381f0a40 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 4 Aug 2017 15:14:35 +0200
Subject: [PATCH] stats: allow counting complete SCCs

* bin/common_aoutput.cc, NEWS: Update documentation.
* spot/twaalgos/stats.cc: Honor c and C.
* tests/core/alternating.test: Test it.
---
 NEWS                        |  3 +++
 bin/common_aoutput.cc       |  4 +--
 spot/twaalgos/stats.cc      | 20 +++++++++++---
 tests/core/alternating.test | 53 +++++++++++++++++++++++++++++++++++++
 4 files changed, 74 insertions(+), 6 deletions(-)

diff --git a/NEWS b/NEWS
index f04b027bb..44b4d9d93 100644
--- a/NEWS
+++ b/NEWS
@@ -30,6 +30,9 @@ New in spot 2.3.5.dev (not yet released)
     because it can now extract the subautomaton leading to an SCC
     specified by number.  (The old name is still kept as an alias.)
 
+  - The --stats=%c option of tools producing automata can now be
+    restricted to count complete SCCs, using %[c]c.
+
   Library:
 
   - A new library, libspotgen, gathers all functions used to generate
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 40f4be299..925a54f1c 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -184,7 +184,7 @@ static const argp_option io_options[] =
       OPTION_DOC | OPTION_NO_USAGE,
       "number of SCCs; you may filter the SCCs to count "
       "using the following LETTERS, possibly concatenated: (a) accepting, "
-      "(r) rejecting, (v) trivial, (t) terminal, (w) weak, "
+      "(r) rejecting, (c) complete, (v) trivial, (t) terminal, (w) weak, "
       "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
     { "%R, %[LETTERS]R", 0, nullptr,
       OPTION_DOC | OPTION_NO_USAGE,
@@ -244,7 +244,7 @@ static const argp_option o_options[] =
     { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "number of SCCs; you may filter the SCCs to count "
       "using the following LETTERS, possibly concatenated: (a) accepting, "
-      "(r) rejecting, (v) trivial, (t) terminal, (w) weak, "
+      "(r) rejecting, (c) complete, (v) trivial, (t) terminal, (w) weak, "
       "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
     { "%R, %[LETTERS]R", 0, nullptr,
       OPTION_DOC | OPTION_NO_USAGE,
diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc
index b4b151f5f..0988b42d1 100644
--- a/spot/twaalgos/stats.cc
+++ b/spot/twaalgos/stats.cc
@@ -212,6 +212,8 @@ namespace spot
     bool non_weak = false;
     bool inherently_weak = false;
     bool non_inherently_weak = false;
+    bool complete = false;
+    bool non_complete = false;
 
     const char* beg = pos;
     auto error = [&](std::string str)
@@ -236,11 +238,11 @@ namespace spot
         case 'r':
           rejecting = true;
           break;
-        case 'v':
-          trivial = true;
+        case 'c':
+          complete = true;
           break;
-        case 'V':
-          non_trivial = true;
+        case 'C':
+          non_complete = true;
           break;
         case 't':
           terminal = true;
@@ -248,6 +250,12 @@ namespace spot
         case 'T':
           non_terminal = true;
           break;
+        case 'v':
+          trivial = true;
+          break;
+        case 'V':
+          non_trivial = true;
+          break;
         case 'w':
           weak = true;
           break;
@@ -301,6 +309,10 @@ namespace spot
           continue;
         if (non_trivial && val_->is_trivial(i))
           continue;
+        if (complete && !is_complete_scc(*val_, i))
+          continue;
+        if (non_complete && is_complete_scc(*val_, i))
+          continue;
         if (terminal && !is_terminal_scc(*val_, i))
           continue;
         if (non_terminal && is_terminal_scc(*val_, i))
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 1686f774f..50c8814aa 100755
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -1862,3 +1862,56 @@ EOF
 autfilt --tgba in 2>out && exit 1
 grep 'autfilt.*weak.*alternating' out
 test '2 0 2 2'  = "`autfilt --stats='%[Wiw]c %[w]c %[iw]c %[W]c' in`"
+
+
+cat >in <<EOF
+HOA: v1
+States: 2
+AP: 1 "a"
+Start: 0
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 1&0 {0}
+[!0] 0
+State: 1
+[t] 0&1
+--END--
+EOF
+test '0 1 1 0 0'  = "`autfilt --stats='%[iw]c %[W]c %[c]c %[C]c %[t]c' in`"
+
+cat >in <<EOF
+HOA: v1
+States: 3
+AP: 1 "a"
+Start: 0
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[t] 0&1
+State: 1
+[0] 1&2 {0}
+[!0] 1
+State: 2
+[t] 2&1
+--END--
+EOF
+test '1 1 1 1 0'  = "`autfilt --stats='%[iw]c %[W]c %[c]c %[C]c %[t]c' in`"
+
+cat >in <<EOF
+HOA: v1
+States: 3
+AP: 1 "a"
+Start: 0
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[t] 0&1
+State: 1 {0}
+[0] 1&2
+[!0] 1
+State: 2 {0}
+[t] 2&1
+--END--
+EOF
+test '2 0 1 1 1'  = "`autfilt --stats='%[iw]c %[W]c %[c]c %[C]c %[t]c' in`"