* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument

branching_postponement.
* src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
from ltl_to_tgba_fm().
(ltl_to_tgba_fm): Implement the branching_postponement optimization.
* src/tgbatest/ltl2tgba.cc: Add the -p option.
* src/tgbatest/spotlbtt.test: Exercise branching postponement.
* wrap/python/cgi/ltl2tgba.in: Make it an option.

ChangeLog

@@ -1,3 +1,14 @@
+2004-05-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
+	branching_postponement.
+	* src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
+	from ltl_to_tgba_fm().
+	(ltl_to_tgba_fm): Implement the branching_postponement optimization.
+	* src/tgbatest/ltl2tgba.cc: Add the -p option.
+	* src/tgbatest/spotlbtt.test: Exercise branching postponement.
+	* wrap/python/cgi/ltl2tgba.in: Make it an option.
+
 2004-05-04  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify

src/tgbaalgos/ltl2tgba_fm.cc

@@ -396,9 +396,57 @@ namespace spot
 
   }
 
+  typedef std::map<bdd, bdd, bdd_less_than> prom_map;
+  typedef Sgi::hash_map<const formula*, prom_map, ptr_hash<formula> > dest_map;
+  typedef std::map<bdd, const formula*, bdd_less_than> succ_to_formula;
+
+  static void
+  fill_dests(translate_dict& d, bool symb_merge,
+	     std::set<const formula*>& formulae_seen,
+	     succ_to_formula& canonical_succ, ltl_trad_visitor& v,
+	     dest_map& dests, bdd label, formula* dest)
+  {
+    // If we already know a state with the same successors,
+    // use it in lieu of the current one.  (See the comments
+    // for canonical_succ.)  We need to do this only for new
+    // destinations.
+    if (symb_merge
+	&& formulae_seen.find(dest) == formulae_seen.end())
+      {
+	dest->accept(v);
+	bdd succbdd = v.result();
+	succ_to_formula::iterator cs =
+	  canonical_succ.find(succbdd);
+	if (cs != canonical_succ.end())
+	  {
+	    destroy(dest);
+	    dest = clone(cs->second);
+	  }
+	else
+	  {
+	    canonical_succ[succbdd] = clone(dest);
+	  }
+      }
+
+    bdd promises = bdd_existcomp(label, d.a_set);
+    bdd conds = bdd_existcomp(label, d.var_set);
+
+    dest_map::iterator i = dests.find(dest);
+    if (i == dests.end())
+      {
+	dests[dest][promises] = conds;
+      }
+    else
+      {
+	i->second[promises] |= conds;
+	destroy(dest);
+      }
+  }
+
+
   tgba_explicit*
   ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
-		 bool exprop, bool symb_merge)
+		 bool exprop, bool symb_merge, bool branching_postponement)
   {
     // Normalize the formula.  We want all the negations on
     // the atomic propositions.  We also suppress logic
@@ -414,7 +462,6 @@ namespace spot
     // We do this because many formulae (such as `aR(bRc)' and
     // `aR(bRc).(bRc)') are equivalent, and are trivially identified
     // by looking at the set of successors.
-    typedef std::map<bdd, const formula*, bdd_less_than> succ_to_formula;
     succ_to_formula canonical_succ;
 
     translate_dict d(dict);
@@ -435,8 +482,8 @@ namespace spot
 
 	// Translate it into a BDD to simplify it.
 	// FIXME: Currently the same formula can be converted into a
-	// BDD twice.  Once in the symb_merge block below, and then
+	// BDD twice.  Once in the symb_merge block in fill_dests,
-	// once here.
+	// and then  once here.
 	f->accept(v);
 	bdd res = v.result();
 	succ_to_formula::iterator cs = canonical_succ.find(res);
@@ -474,10 +521,6 @@ namespace spot
 	//
 	// In `exprop' mode, considering all possible combinations of
 	// outgoing propositions generalizes the above trick.
-
-	typedef std::map<bdd, bdd, bdd_less_than> prom_map;
-	typedef Sgi::hash_map<const formula*, prom_map, ptr_hash<formula> >
-	  dest_map;
 	dest_map dests;
 
 	// Compute all outgoing arcs.
@@ -497,50 +540,43 @@ namespace spot
 	    bdd one_prop_set =
 	      exprop ? bdd_satoneset(all_props, var_set, bddtrue) : bddtrue;
 	    all_props -= one_prop_set;
+
+	    typedef std::map<bdd, formula*, bdd_less_than> succ_map;
+	    succ_map succs;
+
 	    minato_isop isop(res & one_prop_set);
 	    bdd cube;
 	    while ((cube = isop.next()) != bddfalse)
 	      {
-		const formula* dest =
+		bdd label = bdd_exist(cube, d.next_set);
+		formula* dest =
 		  d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set));
 
-		// If we already know a state with the same successors,
+		// If we are not postponing the branching, we can
-		// use it in lieu of the current one.  (See the comments
+		// declare the outgoing transitions immediately.
-		// for canonical_succ.)  We need to do this only for new
+		// Otherwise, we merge transitions with identical
-		// destinations.
+		// label, and declare the outgoing transitions in a
-		if (symb_merge
+		// second loop.
-		    && formulae_seen.find(dest) == formulae_seen.end())
+		if (!branching_postponement)
 		  {
-		    dest->accept(v);
+		    fill_dests(d, symb_merge, formulae_seen, canonical_succ,
-		    bdd succbdd = v.result();
+			       v, dests, label, dest);
-		    succ_to_formula::iterator cs =
-		      canonical_succ.find(succbdd);
-		    if (cs != canonical_succ.end())
-		      {
-			destroy(dest);
-			dest = clone(cs->second);
-		      }
-		    else
-		      {
-			canonical_succ[succbdd] = clone(dest);
-		      }
-		  }
-
-		bdd promises = bdd_existcomp(cube, d.a_set);
-		bdd conds =
-		  exprop ? one_prop_set : bdd_existcomp(cube, var_set);
-
-		dest_map::iterator i = dests.find(dest);
-		if (i == dests.end())
-		  {
-		    dests[dest][promises] = conds;
 		  }
 		else
 		  {
-		    i->second[promises] |= conds;
+		    succ_map::iterator si = succs.find(label);
-		    destroy(dest);
+		    if (si == succs.end())
+		      succs[label] = dest;
+		    else
+		      si->second = multop::instance(multop::Or,
+						    si->second, dest);
 		  }
 	      }
+	    if (branching_postponement)
+	      for (succ_map::const_iterator si = succs.begin();
+		   si != succs.end(); ++si)
+		fill_dests (d, symb_merge, formulae_seen, canonical_succ, v,
+			    dests, si->first, si->second);
 	  }
 
 	// Check for an arc going to 1 (True).  Register it first, that

src/tgbaalgos/ltl2tgba_fm.hh

@@ -46,19 +46,43 @@ namespace spot
   ///   month	  = {September},
   ///   isbn      = {3-540-66587-0}
   /// }
+  /// \endverbatim
   ///
   /// If \a exprop is set, the algorithm will consider all properties
   /// combinations possible on each state, in an attempt to reduce
   /// the non-determinism.  The automaton will have the same size as
   /// without this option, but because the transition will be more
-  /// deterministic product automaton will be smaller (or, at worse, equal).
+  /// deterministic, the product automaton will be smaller (or, at worse,
+  /// equal).
   ///
   /// If \a symb_merge is set to false, states with the same symbolic
   /// representation (these are equivalent formulae) will not be
   /// merged.
+  ///
+  /// If \a branching_postponement is set, several transitions leaving
+  /// from the same state with the same label (i.e., condition + acceptance
+  /// conditions) will be merged.  This correspond to an optimization
+  /// described in the following paper.
+  /// \verbatim
+  /// @InProceedings{	  sebastiani.03.charme,
+  ///   author	  = {Roberto Sebastiani and Stefano Tonetta},
+  ///   title	  = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for
+  /// 		     Efficient LTL Model Checking},
+  ///   booktitle = {Proceedings for the 12th Advanced Research Working
+  /// 		     Conference on Correct Hardware Design and Verification
+  /// 		     Methods (CHARME'03)},
+  ///   pages     = {126--140},
+  ///   year      = {2003},
+  ///   editor	  = {G. Goos and J. Hartmanis and J. van Leeuwen},
+  ///   volume	  = {2860},
+  ///   series	  = {Lectures Notes in Computer Science},
+  ///   month     = {October},
+  ///   publisher = {Springer-Verlag}
+  /// }
   /// \endverbatim
   tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
-				bool exprop = false, bool symb_merge = true);
+				bool exprop = false, bool symb_merge = true,
+				bool branching_postponement = false);
 }
 
 #endif // SPOT_TGBA_LTL2TGBA_HH

src/tgbatest/ltl2tgba.cc

@@ -72,6 +72,7 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -N   display the never clain for Spin "
 	    << "(implies -D)" << std::endl
+            << "  -p   branching postponement (implies -f)" << std::endl
 	    << "  -r   display the relation BDD, not the reachability graph"
 	    << std::endl
 	    << "  -R   same as -r, but as a set" << std::endl
@@ -111,6 +112,7 @@ main(int argc, char** argv)
   bool magic_many = false;
   bool expect_counter_example = false;
   bool from_file = false;
+  bool post_branching = false;
 
   for (;;)
     {
@@ -194,6 +196,11 @@ main(int argc, char** argv)
 	  degeneralize_opt = true;
 	  output = 8;
 	}
+      else if (!strcmp(argv[formula_index], "-p"))
+	{
+	  post_branching = true;
+	  fm_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-r"))
 	{
 	  output = 1;
@@ -300,7 +307,8 @@ main(int argc, char** argv)
 	{
 	  if (fm_opt)
 	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
-					       fm_symb_merge_opt);
+					       fm_symb_merge_opt,
+					       post_branching);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	}

src/tgbatest/spotlbtt.test

@@ -119,6 +119,27 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM post_branch + exprop)"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -p -x -t -D'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop + post_branch), fake"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -T'"
+   Enabled = no
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), fake"

wrap/python/cgi/ltl2tgba.in

@@ -211,6 +211,7 @@ options_trans_fm = [
     ('opt_exprop',          'optimize determinism',                        1),
     ('opt_symb_merge',
      'merge states with same symbolic successor representation',           1),
+    ('opt_branch_post',     'branching postponement',                      0),
     ]
 options_trans_lacim = [
     ('show_relation_set',
@@ -407,11 +408,16 @@ if opt_symb_merge:
     symb_merge = 1
 else:
     symb_merge = 0
+if opt_branch_post:
+    branching_postponement = 1
+else:
+    branching_postponement = 0
 
 if trans_lacim:
     automaton = spot.ltl_to_tgba_lacim(f, dict)
 elif trans_fm:
-    automaton = spot.ltl_to_tgba_fm(f, dict, exprop, symb_merge)
+    automaton = spot.ltl_to_tgba_fm(f, dict,
+                                    exprop, symb_merge, branching_postponement)
 
 print 'done.</p>'
 sys.stdout.flush()