From 90a466d6a3f03e59da64542e94dfda1c73e445f5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 11 Sep 2013 10:49:49 +0200
Subject: [PATCH] degen: consider common outgoing acceptance only inside an SCC

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case that is improved
by this.
* src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.test: Adjust.
---
 src/tgbaalgos/degen.cc     | 19 ++++++--
 src/tgbatest/degenid.test  | 88 ++++++++++++++++++++++++++++++++++++++
 src/tgbatest/ltl2ta.test   |  8 ++--
 src/tgbatest/ltl2tgba.test |  7 ++-
 4 files changed, 110 insertions(+), 12 deletions(-)

diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index 4a35721da..b84afdd76 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -106,7 +106,8 @@ namespace spot
       }
     };
 
-    // Acceptance set common to all outgoing transitions of some state.
+    // Acceptance set common to all outgoing transitions (of the same
+    // SCC -- we do not care about the other) of some state.
     class outgoing_acc
     {
       const tgba* a_;
@@ -114,19 +115,28 @@ namespace spot
       typedef Sgi::hash_map<const state*, cache_entry,
                             state_ptr_hash, state_ptr_equal> cache_t;
       cache_t cache_;
+      const scc_map* sm_;
 
     public:
-      outgoing_acc(const tgba* a): a_(a)
+      outgoing_acc(const tgba* a, const scc_map* sm): a_(a), sm_(sm)
       {
       }
 
       cache_t::const_iterator fill_cache(const state* s)
       {
+	unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0;
         bdd common = a_->all_acceptance_conditions();
         bdd union_ = bddfalse;
         tgba_succ_iterator* it = a_->succ_iter(s);
         for (it->first(); !it->done(); it->next())
           {
+	    // Ignore transitions that leave the SCC of s.
+	    const state* d = it->current_state();
+	    unsigned s2 = sm_ ? sm_->scc_of_state(d) : 0;
+	    d->destroy();
+	    if (s2 != s1)
+	      continue;
+
             bdd set = it->current_acceptance_conditions();
             common &= set;
             union_ |= set;
@@ -325,8 +335,6 @@ namespace spot
     // Initialize scc_orders
     scc_orders orders(a->all_acceptance_conditions());
 
-    outgoing_acc outgoing(a);
-
     // Make sure we always use the same pointer for identical states
     // from the input automaton.
     unicity_table uniq;
@@ -355,6 +363,9 @@ namespace spot
     if (use_scc)
       m.build_map();
 
+    // Cache for common outgoing acceptances.
+    outgoing_acc outgoing(a, use_scc ? &m : 0);
+
     queue_t todo;
 
     const state* s0 = uniq(a->get_init_state());
diff --git a/src/tgbatest/degenid.test b/src/tgbatest/degenid.test
index f6be94ef6..b1fb3c00c 100755
--- a/src/tgbatest/degenid.test
+++ b/src/tgbatest/degenid.test
@@ -103,3 +103,91 @@ grep 'states: 8' out
 # easy to obtain a 4-state BA when tweaking the degeneralization
 # to ignore arc entering an SCC.
 test 3 = "`../../bin/ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`"
+
+
+# This 7-state DRA (built with
+#   ltlfilt -f 'F(a & GFb) | (Fc & Fa & F(c & GF!b))' -l  |
+#   ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - -
+# should be converted in into a 6-state DBA.
+cat >in.dra <<EOF
+DRA v2 explicit
+Comment: "Union{Safra[NBA=3],Safra[NBA=5]}"
+States: 7
+Acceptance-Pairs: 2
+Start: 5
+AP: 3 "a" "b" "c"
+---
+State: 0
+Acc-Sig: +0 +1
+1
+1
+2
+2
+1
+1
+2
+2
+State: 1
+Acc-Sig: +1
+1
+1
+2
+2
+1
+1
+2
+2
+State: 2
+Acc-Sig: +0
+1
+1
+2
+2
+1
+1
+2
+2
+State: 3
+Acc-Sig: +0
+6
+6
+3
+3
+1
+1
+0
+0
+State: 4
+Acc-Sig:
+4
+0
+4
+0
+4
+0
+4
+0
+State: 5
+Acc-Sig:
+5
+3
+5
+3
+4
+0
+4
+0
+State: 6
+Acc-Sig:
+6
+6
+3
+3
+1
+1
+0
+0
+EOF
+
+run 0 ../../bin/dstar2tgba in.dra -BD --stats=%s > out.stat
+test 6 = "`cat out.stat`"
diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test
index e5fc0c8cf..7690aeaba 100755
--- a/src/tgbatest/ltl2ta.test
+++ b/src/tgbatest/ltl2ta.test
@@ -85,7 +85,7 @@ done
 
 for opt in -TA; do
   ../ltl2tgba -ks $opt -RT -DS 'Ga U b' > stdout
-  grep 'transitions: 13$' stdout
+  grep 'transitions: 11$' stdout
   grep 'states: 6$' stdout
 done
 
@@ -119,11 +119,11 @@ grep 'states: 290$' stdout
 
 #tests with artificial livelock state:
 run 0 ../ltl2tgba -ks -TA -lv  -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
-grep 'transitions: 790$' stdout
+grep 'transitions: 784$' stdout
 grep 'states: 66$' stdout
 
 run 0 ../ltl2tgba -TA -RT -ks -lv -DS  "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
-grep 'transitions: 390$' stdout
+grep 'transitions: 384$' stdout
 grep 'states: 26$' stdout
 
 run 0 ../ltl2tgba -TGTA -RT -ks  'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout
@@ -138,7 +138,7 @@ grep 'states: 38$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x  -DS  "$f" >stdout
-grep 'transitions: 555$' stdout
+grep 'transitions: 551$' stdout
 grep 'states: 40$' stdout
 
 
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index afbf703d6..f72716bd5 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -150,11 +150,10 @@ for opt in '' -D -DS; do
   ../ltl2tgba -ks -f -R3 $opt "$f" > stdout
   grep 'transitions: 15$' stdout
   grep 'states: 6$' stdout
+  ../ltl2tgba -ks -f -R3f $opt "$f" > stdout
+  grep 'transitions: 15$' stdout
+  grep 'states: 6$' stdout
 done
-# Note: this is worse with -R3f.
-../ltl2tgba -ks -f -R3f -DS "$f" > stdout
-grep 'transitions: 17$' stdout
-grep 'states: 7$' stdout
 
 # Make sure 'GFa & GFb & GFc & GFd & GFe & GFf'
 # has 7 states and 34 transitions after degeneralization.