* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc

(ltl_to_tgba_fm): Add a new option "containment_checks" to enable
some language containment checks (via emptiness checks) during the
translation.  This first attempt currently only use containment
checks to merge states bisimulating each other.
* src/tgbatest/ltl2tgba.cc: Bind this to option "-c".
* src/tgbatest/spotlbtt.test: Check it.

ChangeLog

@@ -1,5 +1,13 @@
 2006-07-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc
+	(ltl_to_tgba_fm): Add a new option "containment_checks" to enable
+	some language containment checks (via emptiness checks) during the
+	translation.  This first attempt currently only use containment
+	checks to merge states bisimulating each other.
+	* src/tgbatest/ltl2tgba.cc: Bind this to option "-c".
+	* src/tgbatest/spotlbtt.test: Check it.
+
 	* src/tgba/bdddict.cc (bdd_dict::unregister_variable): Correctly
 	call release_n(), not remove() to repopulated the freelist of
 	anonymous BDD variables.  New code I'm working on triggered an

src/tgbaalgos/ltl2tgba_fm.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -33,8 +33,9 @@
 #include "ltlvisit/apcollect.hh"
 #include <cassert>
 #include <memory>
-#include "tgba/tgbabddconcretefactory.hh"
 #include "ltl2tgba_fm.hh"
+#include "tgba/tgbaproduct.hh"
+#include "tgbaalgos/gtec/gtec.hh"
 
 namespace spot
 {
@@ -537,14 +538,118 @@ namespace spot
       pfl_map pfl_;
     };
 
+    // Keep a map of the TGBA translation of all subformulae and their
+    // negations, for easy language containment check.
+    class language_containment_checker
+    {
+      struct record_
+      {
+	const tgba* translation;
+	typedef std::set<const record_*> incomp_map;
+	incomp_map incompatible;
+      };
+      typedef Sgi::hash_map<const formula*,
+			    record_, formula_ptr_hash> trans_map;
+    public:
+      language_containment_checker(bdd_dict* dict, bool exprop,
+				   bool symb_merge,
+				   bool branching_postponement,
+				   bool fair_loop_approx)
+	: dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
+	  branching_postponement_(branching_postponement),
+	  fair_loop_approx_(fair_loop_approx)
+      {
+      }
+
+      ~language_containment_checker()
+      {
+
+	while (!translated_.empty())
+	  {
+	    trans_map::iterator i = translated_.begin();
+	    delete i->second.translation;
+	    const formula* f = i->first;
+	    translated_.erase(i);
+	    destroy(f);
+	  }
+      }
+
+      // Check whether L(l) is a subset of L(g).
+      bool
+      contained(const formula* l, const formula* g)
+      {
+	const record_* rl = register_formula_(l);
+	const formula* ng = unop::instance(unop::Not, clone(g));
+	const record_* rng = register_formula_(ng);
+	destroy(ng);
+	bool res = rl->incompatible.find(rng) != rl->incompatible.end();
+	return res;
+      }
+
+      // Check whether L(l) = L(g).
+      bool
+      equal(const formula* l, const formula* g)
+      {
+	return contained(l,g) && contained(g,l);
+      }
+
+    protected:
+      const record_*
+      register_formula_(const formula* f)
+      {
+	trans_map::iterator i = translated_.find(f);
+	if (i != translated_.end())
+	  return &i->second;
+
+	const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_,
+						branching_postponement_,
+						fair_loop_approx_);
+	record_& r = translated_[clone(f)];
+	r.translation = e;
+
+	// Check the emptiness of the product of this formula with any
+	// other registered formula.
+	for (i = translated_.begin(); i != translated_.end(); ++i)
+	  {
+	    if (f == i->first)
+	      continue;
+	    const tgba* p = new tgba_product(e, i->second.translation);
+	    emptiness_check* ec = couvreur99(p);
+	    emptiness_check_result* ecr = ec->check();
+	    if (!ecr)
+	      {
+		r.incompatible.insert(&i->second);
+		i->second.incompatible.insert(&r);
+	      }
+	    else
+	      delete ecr;
+	    delete ec;
+	    delete p;
+	  }
+	return &r;
+      }
+
+    private:
+      /* Translation options */
+      bdd_dict* dict_;
+      bool exprop_;
+      bool symb_merge_;
+      bool branching_postponement_;
+      bool fair_loop_approx_;
+      /* Translation Maps */
+      trans_map translated_;
+    };
+
     class formula_canonizer
     {
     public:
       formula_canonizer(translate_dict& d,
-			bool fair_loop_approx, bdd all_promises)
+			bool fair_loop_approx, bdd all_promises,
+			language_containment_checker* lcc)
 	: v_(d),
 	  fair_loop_approx_(fair_loop_approx),
-	  all_promises_(all_promises)
+	  all_promises_(all_promises),
+	  lcc_(lcc)
       {
 	// For cosmetics, register 1 initially, so the algorithm will
 	// not register an equivalent formula first.
@@ -563,13 +668,16 @@ namespace spot
       }
 
       bdd
-      translate(const formula* f)
+      translate(const formula* f, bool* new_flag = 0)
       {
 	// Use the cached result if available.
 	formula_to_bdd_map::const_iterator i = f2b_.find(f);
 	if (i != f2b_.end())
 	  return i->second;
 
+	if (new_flag)
+	  *new_flag = true;
+
 	// Perform the actual translation.
 	f->accept(v_);
 	bdd res = v_.result();
@@ -596,17 +704,36 @@ namespace spot
       const formula*
       canonize(const formula* f)
       {
-	bdd b = translate(f);
+	bool new_variable = false;
+	bdd b = translate(f, &new_variable);
 
 	bdd_to_formula_map::iterator i = b2f_.find(b);
-	// Since we have just translated the formula, it is necessary in b2f_.
+	// Since we have just translated the formula, it is
+	// necessarily in b2f_.
 	assert(i != b2f_.end());
 
 	if (i->second != f)
 	  {
+	    // The translated bdd maps to an already seen formula.
 	    destroy(f);
 	    f = clone(i->second);
 	  }
+	else if (new_variable && lcc_)
+	  {
+	    // It's a new bdd for a new formula.  Let's see if we can
+	    // find an equivalent formula with language containment
+	    // checks.
+	    for (formula_to_bdd_map::const_iterator j = f2b_.begin();
+		 j != f2b_.end(); ++j)
+	      if (f != j->first && lcc_->equal(f, j->first))
+		{
+		  f2b_[f] = j->second;
+		  i->second = j->first;
+		  destroy(f);
+		  f = clone(i->second);
+		  break;
+		}
+	  }
 	return f;
       }
 
@@ -627,6 +754,7 @@ namespace spot
       possible_fair_loop_checker pflc_;
       bool fair_loop_approx_;
       bdd all_promises_;
+      language_containment_checker* lcc_;
     };
 
   }
@@ -657,8 +785,10 @@ namespace spot
   ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
 		 bool exprop, bool symb_merge, bool branching_postponement,
 		 bool fair_loop_approx, const atomic_prop_set* unobs,
-		 int reduce_ltl)
+		 int reduce_ltl, bool containment_checks)
   {
+    symb_merge |= containment_checks;
+
     // Normalize the formula.  We want all the negations on
     // the atomic propositions.  We also suppress logic
     // abbreviations such as <=>, =>, or XOR, since they
@@ -691,7 +821,12 @@ namespace spot
 	all_promises = pv.result();
       }
 
-    formula_canonizer fc(d, fair_loop_approx, all_promises);
+    language_containment_checker lcc(dict, exprop, symb_merge,
+				     branching_postponement,
+				     fair_loop_approx);
+
+    formula_canonizer fc(d, fair_loop_approx, all_promises,
+			 containment_checks ? &lcc : 0);
 
     // These are used when atomic propositions are interpreted as
     // events.  There are two kinds of events: observable events are

src/tgbaalgos/ltl2tgba_fm.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -125,7 +125,8 @@ namespace spot
 				bool branching_postponement = false,
 				bool fair_loop_approx = false,
 				const ltl::atomic_prop_set* unobs = 0,
-				int reduce_ltl = ltl::Reduce_None);
+				int reduce_ltl = ltl::Reduce_None,
+				bool containment_checks = false);
 }
 
 #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH

src/tgbatest/ltl2tgba.cc

@@ -65,6 +65,8 @@ syntax(char* prog)
 	    << "  -A    same as -a, but as a set" << std::endl
 	    << "  -b    display the automaton in the format of spot"
             << std::endl
+	    << "  -c    enable language containment checks (implies -f)"
+	    << std::endl
 	    << "  -d    turn on traces during parsing" << std::endl
 	    << "  -D    degeneralize the automaton as a TBA" << std::endl
 	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
@@ -169,6 +171,7 @@ main(int argc, char** argv)
   bool graph_run_opt = false;
   bool graph_run_tgba_opt = false;
   bool opt_reduce = false;
+  bool containment = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
   spot::tgba_explicit* system = 0;
@@ -199,6 +202,11 @@ main(int argc, char** argv)
 	{
 	  output = 7;
 	}
+      else if (!strcmp(argv[formula_index], "-c"))
+	{
+	  containment = true;
+	  fm_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-d"))
 	{
 	  debug_opt = true;
@@ -499,7 +507,7 @@ main(int argc, char** argv)
 					       fm_symb_merge_opt,
 					       post_branching,
 					       fair_loop_approx, unobservables,
-					       fm_red);
+					       fm_red, containment);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	}

src/tgbatest/spotlbtt.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -68,6 +68,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM) containments"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot './ltl2tgba -F -f -c -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), basic reduction of formula"
@@ -100,6 +108,15 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM) containments + reduction of formula (pre reduction)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot './ltl2tgba -r4 -F -f -c -t'"
+   Enabled = yes
+}
+
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula in FM"