From d07c66944e61150ab6739b124b8fc0f5cf652bb3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 3 Dec 2003 13:29:11 +0000
Subject: [PATCH] * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh
 (tgba_explicit::merge_transitions): New method. *
 src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Factorize all variables (not
 just Next and A) when computing prime implicants, and then call
 merge_transitions().

---
 ChangeLog                    |  8 ++++++++
 src/tgba/tgbaexplicit.cc     | 31 +++++++++++++++++++++++++++++++
 src/tgba/tgbaexplicit.hh     |  1 +
 src/tgbaalgos/ltl2tgba_fm.cc | 29 ++++++++++++++++++++++++++++-
 4 files changed, 68 insertions(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index 1591574be..cefbca50b 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2003-12-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh
+	(tgba_explicit::merge_transitions): New method.
+	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Factorize all
+	variables (not just Next and A) when computing prime implicants,
+	and then call merge_transitions().
+
 2003-12-01  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* configure.ac: Bump version to 0.0m.
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index 40a2f5a24..03e78404a 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -220,6 +220,37 @@ namespace spot
       }
   }
 
+  void
+  tgba_explicit::merge_transitions()
+  {
+    ns_map::iterator i;
+    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+      {
+	state::iterator t1;
+	for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
+	  {
+	    bdd acc = (*t1)->acceptance_conditions;
+	    state* dest = (*t1)->dest;
+
+	    // Find another transition with the same destination and
+	    // acceptance conditions.
+	    state::iterator t2 = t1;
+	    ++t2;
+	    while (t2 != i->second->end())
+	      {
+		state::iterator t2copy = t2++;
+		if ((*t2copy)->acceptance_conditions == acc
+		    && (*t2copy)->dest == dest)
+		  {
+		    (*t1)->condition |= (*t2copy)->condition;
+		    delete *t2copy;
+		    i->second->erase(t2copy);
+		  }
+	      }
+	  }
+      }
+  }
+
   bool
   tgba_explicit::has_acceptance_condition(const ltl::formula* f) const
   {
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 28232c216..d6a513b5d 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -64,6 +64,7 @@ namespace spot
     /// This assumes that all acceptance conditions in \a f are known from dict.
     void add_acceptance_conditions(transition* t, bdd f);
     void complement_all_acceptance_conditions();
+    void merge_transitions();
 
     // tgba interface
     virtual ~tgba_explicit();
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index ada20bbab..8bf9bede0 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -469,7 +469,32 @@ namespace spot
 
 	std::string now = to_string(f);
 
-	minato_isop isop(res, d.next_set & d.a_set);
+	// We used to factor only Next and A variables while computing
+	// prime implicants, with
+	//    minato_isop isop(res, d.next_set & d.a_set);
+	// in order to obtain transitions with formulae of atomic
+	// proposition directly, but unfortunately this led to strange
+	// factorizations.  For instance f U g was translated as
+	//     r(f U g) = g + a(g).r(X(f U g)).(f + g)
+	// instead of just
+	//     r(f U g) = g + a(g).r(X(f U g)).f
+	// Of course both formulae are logically equivalent, but the
+	// latter is "more deterministic" than the former, so it should
+	// be preferred.
+	//
+	// Therefore we now factor all variables.  This may lead to more
+	// transitions than necessary (e.g.,  r(f + g) = f + g  will be
+	// coded as two transitions), but we later call merge_transitions()
+	// to gather transitions with same source/destination and acceptance
+	// conditions.
+	//
+	// Note that this is still not optimal.  For instance it would
+	// be better to encode `f U g' as
+	//     r(f U g) = g + a(g).r(X(f U g)).f.!g
+	// because that leads to a deterministic automaton.  However it
+	// is not clear how to formalize this generally (replace `g'
+	// by an arbitrary boolean function when thinking about it).
+	minato_isop isop(res);
 	bdd cube;
 	while ((cube = isop.next()) != bddfalse)
 	  {
@@ -501,6 +526,8 @@ namespace spot
 	 i != formulae_seen.end(); ++i)
       destroy(*i);
 
+    // Merge transitions if we can.
+    a->merge_transitions();
     // Turn all promises into real acceptance conditions.
     a->complement_all_acceptance_conditions();
     return a;