* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop

argument.  Consider all possible combinations of propositions when
generating arcs.  Suggested by Jean-Michel Couvreur.
* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust.
* src/tgbatest/ltl2tgba.cc: Honor -fx.
* src/tgbatest/spotlbtt.test: Exercise -fx.
* wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded
properties.

ChangeLog

@@ -1,3 +1,14 @@
+2004-02-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop
+	argument.  Consider all possible combinations of propositions when
+	generating arcs.  Suggested by Jean-Michel Couvreur.
+	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust.
+	* src/tgbatest/ltl2tgba.cc: Honor -fx.
+	* src/tgbatest/spotlbtt.test: Exercise -fx.
+	* wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded
+	properties.
+
 2004-02-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltlparse/ltlparse.yy: Typo.

src/tgbaalgos/ltl2tgba_fm.cc

@@ -438,7 +438,7 @@ namespace spot
   }
 
   tgba_explicit*
-  ltl_to_tgba_fm(const formula* f, bdd_dict* dict)
+  ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop)
   {
     // Normalize the formula.  We want all the negations on
     // the atomic propositions.  We also suppress logic
@@ -506,61 +506,74 @@ namespace spot
 	// to handle this, we take the conditions of any transition
 	// going to true (it's `g' here), and remove it from the other
 	// transitions.
-	// It might be interesting to look at ways to generalize this.
+	//
-	// (Replace `g' by an arbitrary boolean function when thinking
+	// In `exprop' mode, considering all possible combinations of
-	// about it).
+	// 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.
-	minato_isop isop(res);
+	bdd all_props = bddtrue;
-	bdd cube;
+	bdd var_set = bdd_existcomp(bdd_support(res), d.var_set);
-	while ((cube = isop.next()) != bddfalse)
+	while (all_props != bddfalse)
 	  {
-	    const formula* dest =
+	    bdd one_prop_set =
-	      d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set));
+	      exprop ? bdd_satoneset(all_props, var_set, bddtrue) : bddtrue;
-
+	    all_props -= one_prop_set;
-	    // If we already know a state with the same successors,
+	    minato_isop isop(res & one_prop_set);
-	    // use it in lieu of the current one.  (See the comments
+	    bdd cube;
-	    // for canonical_succ.)  We need to do this only for new
+	    while ((cube = isop.next()) != bddfalse)
-	    // destinations.
-	    if (formulae_seen.find(dest) == formulae_seen.end())
 	      {
-		dest->accept(v);
+		const formula* dest =
-		bdd succbdd = v.result();
+		  d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set));
-		succ_to_formula::iterator cs = canonical_succ.find(succbdd);
+
-		if (cs != canonical_succ.end())
+		// 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 (formulae_seen.find(dest) == formulae_seen.end())
 		  {
-		    destroy(dest);
+		    dest->accept(v);
-		    dest = clone(cs->second);
+		    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] = 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
 		  {
-		    canonical_succ[succbdd] = dest;
+		    i->second[promises] |= conds;
+		    destroy(dest);
 		  }
 	      }
-
-	    bdd promises = bdd_existcomp(cube, d.a_set);
-	    bdd conds = bdd_existcomp(cube, 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);
-	      }
 	  }
 
 	// Check for an arc going to True.  Register it first, that
 	// way it will be explored before the other during the model
 	// checking.
 	dest_map::const_iterator i = dests.find(constant::true_instance());
+	// conditions of the True arc, so when can remove them from
+	// all other arcs.  This is not needed when exprop is used,
+	// but it does not hurt.
 	bdd cond_for_true = bddfalse;
 	if (i != dests.end())
 	  {

src/tgbaalgos/ltl2tgba_fm.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -46,8 +46,13 @@ namespace spot
   ///   month	  = {September},
   ///   isbn      = {3-540-66587-0}
   /// }
+  ///
+  /// If \a exprop is set, the algorithm will consider all properties
+  /// combinations possible on each state, in an attempt to reduce
+  /// the non-determinism.
   /// \endverbatim
-  tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict);
+  tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
+				bool exprop = false);
 }
 
 #endif // SPOT_TGBA_LTL2TGBA_HH

src/tgbatest/ltl2tgba.cc

@@ -61,6 +61,8 @@ syntax(char* prog)
 	    << "counter-example " << std::endl
             << "  -f   use Couvreur's FM algorithm for translation"
 	    << std::endl
+            << "  -fx   use Couvreur's FM algorithm, with exploded properties"
+	    << std::endl
             << "  -F   read the formula from the file" << std::endl
 	    << "  -m   magic-search (implies -D), expect a counter-example"
 	    << std::endl
@@ -93,6 +95,7 @@ main(int argc, char** argv)
   bool debug_opt = false;
   bool degeneralize_opt = false;
   bool fm_opt = false;
+  bool fm_exprop_opt = false;
   bool file_opt = false;
   int output = 0;
   int formula_index = 0;
@@ -153,6 +156,11 @@ main(int argc, char** argv)
 	{
 	  fm_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-fx"))
+	{
+	  fm_opt = true;
+	  fm_exprop_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-F"))
 	{
 	  file_opt = true;
@@ -265,7 +273,7 @@ main(int argc, char** argv)
       else
 	{
 	  if (fm_opt)
-	    to_free = a = spot::ltl_to_tgba_fm(f, dict);
+	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	  spot::ltl::destroy(f);

src/tgbatest/spotlbtt.test

@@ -70,6 +70,27 @@ Algorithm
    Enabled = no
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop)"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop), degeneralized"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t -D'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop), fake"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -T'"
+   Enabled = no
+}
+
 GlobalOptions
 {
    Rounds = 100

wrap/python/cgi/ltl2tgba.in

@@ -188,6 +188,7 @@ options = [
 default_translator = 'trans_fm';
 translators = [
     ('trans_fm',        'Convreur/FM'),
+    ('trans_fm_exprop', 'Convreur/FM - exploded properties'),
     ('trans_lacim',     'Convreur/LaCIM'),
     ]
 
@@ -342,6 +343,8 @@ if trans_lacim:
     automaton = spot.ltl_to_tgba_lacim(f, dict)
 elif trans_fm:
     automaton = spot.ltl_to_tgba_fm(f, dict)
+elif trans_fm_exprop:
+    automaton = spot.ltl_to_tgba_fm(f, dict, True)
 
 print 'done.</p>'
 sys.stdout.flush()