Add an algorithm (from Couvreur) working on BDDs to reduce the

size of TGBAs represented as BDDs by deleting unaccepting SCCs.

* src/eltlparse/eltlparse.yy: Remove a warning.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
new function delete_unaccepting_scc in both classes.
* src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
new function in LaCIM for ELTL and bench it.
* src/tgbatest/defs.in: Fix it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
ELTL in benchs.

ChangeLog

@@ -1,3 +1,18 @@
+2009-09-04  Damien Lefortier <dam@lrde.epita.fr>
+
+	Add an algorithm (from Couvreur) working on BDDs to reduce the
+	size of TGBAs represented as BDDs by deleting unaccepting SCCs.
+
+	* src/eltlparse/eltlparse.yy: Remove a warning.
+	* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
+	src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
+	new function delete_unaccepting_scc in both classes.
+	* src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
+	new function in LaCIM for ELTL and bench it.
+	* src/tgbatest/defs.in: Fix it.
+	* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
+	ELTL in benchs.
+
 2009-09-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix path to libtool in test suites.

bench/ltl2tgba/algorithms

@@ -31,6 +31,22 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "LACIM, eltl"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$ELTL2TGBA -LW'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "LACIM, eltl, +delete_unaccepting_scc"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$ELTL2TGBA -L'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "FM, degen, +symb_merge, +exprop, LTLopt"

bench/ltl2tgba/defs.in

@@ -40,6 +40,7 @@ LBTT_TRANSLATE="@LBTT_TRANSLATE@"
 LTL2BA='@LTL2BA@'
 LTL2NBA='@LTL2NBA@'
 LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@'
+ELTL2TGBA='@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@'
 MODELLA='@MODELLA@'
 SPIN='@SPIN@'
 WRING2LBTT='@WRING2LBTT@'

src/eltlparse/eltlparse.yy

@@ -368,7 +368,7 @@ nfa_arg: ARG
 	  aliasmap::const_iterator i = amap.find(*$1);
 	  if (i != amap.end())
 	  {
-            int arity = formula_tree::arity(i->second);
+            unsigned arity = formula_tree::arity(i->second);
 	    CHECK_ARITY(@1, $1, $3->children.size(), arity);
 
 	    // Hack to return the right type without screwing with the

src/tgba/tgbabddconcrete.cc

@@ -164,4 +164,11 @@ namespace spot
     return data_;
   }
 
+  void
+  tgba_bdd_concrete::delete_unaccepting_scc()
+  {
+    data_.delete_unaccepting_scc(init_);
+    set_init_state(init_);
+  }
+
 }

src/tgba/tgbabddconcrete.hh

@@ -79,6 +79,10 @@ namespace spot
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
 
+    /// \brief Delete SCCs (Strongly Connected Components) from the
+    /// TGBA which cannot be accepting.
+    void delete_unaccepting_scc();
+
   protected:
     virtual bdd compute_support_conditions(const state* state) const;
     virtual bdd compute_support_variables(const state* state) const;

src/tgba/tgbabddcoredata.cc

@@ -130,4 +130,67 @@ namespace spot
     acc_set &= acc;
     negacc_set &= !acc;
   }
+
+  void
+  tgba_bdd_core_data::delete_unaccepting_scc(bdd init)
+  {
+    bdd er = bdd_exist(relation, var_set); /// existsRelation
+    bdd s0 = bddfalse;
+    bdd s1 = bdd_exist(bdd_exist(init & relation, var_set), now_set);
+    s1 = bdd_replace(s1, dict->next_to_now);
+
+    /// Find all reachable states
+    while (s0 != s1)
+    {
+      s0 = s1;
+      /// Compute s1 = succ(s0) | s
+      s1 = bdd_replace(bdd_exist(s0 & er, now_set), dict->next_to_now) | s0;
+    }
+
+    /// Find states which can be visited infinitely often while seeing
+    /// all acceptance conditions
+    s0 = bddfalse;
+    while (s0 != s1)
+    {
+      s0 = s1;
+      bdd all = all_acceptance_conditions;
+      while (all != bddfalse)
+      {
+	bdd next = bdd_satone(all);
+	all -= next;
+	s1 = infinitely_often(s1, next, er);
+      }
+    }
+
+    relation = s0 & (relation & bdd_replace(s0, dict->now_to_next));
+  }
+
+  bdd
+  tgba_bdd_core_data::infinitely_often(bdd s, bdd acc, bdd er)
+  {
+    bdd ar = acc & (relation & acceptance_conditions); /// accRelation
+    bdd s0 = bddfalse;
+    bdd s1 = s;
+
+    while (s0 != s1)
+    {
+      s0 = s1;
+      bdd as = bdd_replace(s0, dict->now_to_next) & ar;
+      as = bdd_exist(bdd_exist(as, next_set), var_set) & s0;
+
+      /// Do predStar
+      bdd s0_ = bddfalse;
+      bdd s1_ = bdd_exist(as, acc_set);
+      while (s0_ != s1_)
+      {
+	s0_ = s1_;
+	/// Compute s1_ = pred(s0_) | s0_
+	s1_ = bdd_exist(er & bdd_replace(s0_, dict->now_to_next), next_set);
+	s1_ = (s1_ & s0) | s0_;
+      }
+      s1 = s0_;
+    }
+
+    return s0;
+  }
 }

src/tgba/tgbabddcoredata.hh

@@ -142,6 +142,13 @@ namespace spot
     /// \brief Update the variable sets to take a new acceptance condition
     /// into account.
     void declare_acceptance_condition(bdd prom);
+
+    /// \brief Delete SCCs (Strongly Connected Components) from the
+    /// relation which cannot be accepting.
+    void delete_unaccepting_scc(bdd init);
+
+  private:
+    bdd infinitely_often(bdd s, bdd acc, bdd er);
   };
 }
 

src/tgbatest/defs.in

@@ -50,7 +50,7 @@ mkdir $testSubDir
 cd $testSubDir
 
 DOT='@DOT@'
-top_builddir='@top_builddir@'
+top_builddir='../@top_builddir@'
 LBTT="@LBTT@"
 LBTT_TRANSLATE="@LBTT_TRANSLATE@"
 VALGRIND='@VALGRIND@'

src/tgbatest/eltl2tgba.cc

@@ -36,14 +36,18 @@
 void
 syntax(char* prog)
 {
-  std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl
+  std::cerr << "Usage: " << prog << " [OPTIONS...]  formula [file]" << std::endl
-	    << "       " << prog << " -F [OPTIONS...] file [file]" << std::endl
+	    << "       " << prog << " -F  [OPTIONS...] file [file]" << std::endl
-	    << "       " << prog << " -L [OPTIONS...] file [file]" << std::endl
+	    << "       " << prog << " -L  [OPTIONS...] file [file]" << std::endl
+	    << "       " << prog << " -LW [OPTIONS...] file [file]" << std::endl
 	    << std::endl
 	    << "Options:" << std::endl
 	    << "  -F    read the formula from the file (extended input format)"
 	    << std::endl
 	    << "  -L    read the formula from an LBTT-compatible file"
+	    << std::endl
+	    << "  -LW   read the formula from an LBTT-compatible file"
+	    << " (with no reduction)"
 	    << std::endl;
 }
 
@@ -76,14 +80,16 @@ main(int argc, char** argv)
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::formula* f = 0;
   int formula_index = 0;
+  int reduce = 1;
 
   if (strcmp(argv[1], "-F") == 0)
   {
     f = spot::eltl::parse_file(argv[2], p, env, false);
     formula_index = 2;
   }
-  if (strcmp(argv[1], "-L") == 0)
+  if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0)
   {
+    reduce = strcmp(argv[1], "-LW") == 0 ? 0 : 1;
     std::string input;
     std::ifstream ifs(argv[2]);
     std::getline(ifs, input, '\0');
@@ -118,8 +124,10 @@ main(int argc, char** argv)
 
   spot::bdd_dict* dict = new spot::bdd_dict();
   spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict);
+  if (reduce == 1)
+    concrete->delete_unaccepting_scc();
 
-  if (strcmp(argv[1], "-L") == 0)
+  if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0)
     spot::lbtt_reachable(std::cout, concrete);
   else
   {

src/tgbatest/spotlbtt.test

@@ -64,6 +64,14 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), eltl"
    Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../eltl2tgba -LW'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc"
+   Path = "${LBTT_TRANSLATE}"
    Parameters = "--spot '../eltl2tgba -L'"
    Enabled = yes
 }