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

symb_merge argument.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise.
* src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y
to unset symb_merge.
* wrap/python/cgi/ltl2tgba.in: Remove the exprop version
of the FM translator, make exprop and symb_merge options.

ChangeLog

@@ -1,5 +1,13 @@
 2004-02-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the
+	symb_merge argument.
+	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise.
+	* src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y
+	to unset symb_merge.
+	* wrap/python/cgi/ltl2tgba.in: Remove the exprop version
+	of the FM translator, make exprop and symb_merge options.
+
 	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>:
 	suppress the GFy optimisation introduced on 2003-11-26, it is
 	generalized by the identification of states with same symbolic

src/tgbaalgos/ltl2tgba_fm.cc

@@ -435,7 +435,8 @@ namespace spot
   }
 
   tgba_explicit*
-  ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop)
+  ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
+		 bool exprop, bool symb_merge)
   {
     // Normalize the formula.  We want all the negations on
     // the atomic propositions.  We also suppress logic
@@ -530,7 +531,8 @@ namespace spot
 		// 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())
+		if (symb_merge
+		    && formulae_seen.find(dest) == formulae_seen.end())
 		  {
 		    dest->accept(v);
 		    bdd succbdd = v.result();

src/tgbaalgos/ltl2tgba_fm.hh

@@ -49,10 +49,16 @@ namespace spot
   ///
   /// 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 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).
+  ///
+  /// If \a symb_merge is set to false, states with the same symbolic
+  /// representation (these are equivalent formulae) will not be
+  /// merged.
   /// \endverbatim
   tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
-				bool exprop = false);
+				bool exprop = false, bool symb_merge = true);
 }
 
 #endif // SPOT_TGBA_LTL2TGBA_HH

src/tgbatest/ltl2tgba.cc

@@ -61,8 +61,6 @@ 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
@@ -82,8 +80,12 @@ syntax(char* prog)
 	    << "acceptance conditions" << std::endl
 	    << "  -v   display the BDD variables used by the automaton"
 	    << std::endl
+            << "  -x   try to produce a more deterministic automata "
+	    << "(implies -f)" << std::endl
 	    << "  -X   do not compute an automaton, read it from a file"
-	    << std::endl;
+	    << std::endl
+	    << "  -y   do not merge states with same symbolic representation "
+	    << "(implies -f)" << std::endl;
   exit(2);
 }
 
@@ -96,6 +98,7 @@ main(int argc, char** argv)
   bool degeneralize_opt = false;
   bool fm_opt = false;
   bool fm_exprop_opt = false;
+  bool fm_symb_merge_opt = true;
   bool file_opt = false;
   int output = 0;
   int formula_index = 0;
@@ -156,11 +159,6 @@ 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;
@@ -215,10 +213,20 @@ main(int argc, char** argv)
 	{
 	  output = 5;
 	}
+      else if (!strcmp(argv[formula_index], "-x"))
+	{
+	  fm_opt = true;
+	  fm_exprop_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-X"))
 	{
 	  from_file = true;
 	}
+      else if (!strcmp(argv[formula_index], "-y"))
+	{
+	  fm_opt = true;
+	  fm_symb_merge_opt = false;
+	}
       else
 	{
 	  break;
@@ -282,7 +290,8 @@ main(int argc, char** argv)
       else
 	{
 	  if (fm_opt)
-	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt);
+	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
+					       fm_symb_merge_opt);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	  spot::ltl::destroy(f);

src/tgbatest/spotlbtt.test

@@ -56,6 +56,13 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), without symb_merge"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -y -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), degeneralized"
@@ -70,6 +77,13 @@ Algorithm
    Enabled = no
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), without symb_merge, fake"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -y -T'"
+   Enabled = no
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), fake, LTL simplifications by ltl2ba"
@@ -80,28 +94,42 @@ Algorithm
 Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop)"
-   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t'"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop), without symb_merge"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -y -t'"
    Enabled = yes
 }
 
 Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), degeneralized"
-   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t -D'"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -t -D'"
    Enabled = yes
 }
 
 Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), fake"
-   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -T'"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -T'"
+   Enabled = no
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM exprop), without symb_merge, fake"
+   Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -y -T'"
    Enabled = no
 }
 
 Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba"
-   Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-fx -T\" -F'"
+   Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'"
    Enabled = no
 }
 

wrap/python/cgi/ltl2tgba.in

@@ -162,6 +162,9 @@ LTL-to-B&uuml;chi translator</H1>"""
 formula = form.getfirst('formula', '')
 
 options = [
+    ('opt_exprop',          'optimize determinism (FM only)',              1),
+    ('opt_symb_merge',
+     'merge states with same symbolic successor representation (FM only)', 1),
     ('show_parse',          'show traces during parsing',                  0),
     ('show_formula_dot',    'print the formula as .dot',                   0),
     ('show_formula_gif',    'draw the formula',                            0),
@@ -188,7 +191,6 @@ options = [
 default_translator = 'trans_fm';
 translators = [
     ('trans_fm',        'Convreur/FM'),
-    ('trans_fm_exprop', 'Convreur/FM - exploded properties'),
     ('trans_lacim',     'Convreur/LaCIM'),
     ]
 
@@ -339,12 +341,19 @@ dict = spot.bdd_dict()
 print '<p>Building automaton...',
 sys.stdout.flush()
 
+if opt_exprop:
+    exprop = 1
+else:
+    exprop = 0
+if opt_symb_merge:
+    symb_merge = 1
+else:
+    symb_merge = 0
+
 if trans_lacim:
     automaton = spot.ltl_to_tgba_lacim(f, dict)
 elif trans_fm:
-    automaton = spot.ltl_to_tgba_fm(f, dict)
+    automaton = spot.ltl_to_tgba_fm(f, dict, exprop, symb_merge)
-elif trans_fm_exprop:
-    automaton = spot.ltl_to_tgba_fm(f, dict, True)
 
 print 'done.</p>'
 sys.stdout.flush()