Add support for unambiguous automata

* src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/ltl2tgba_fm.cc: Implement
generation of unambiguous automata.
* src/tests/ltl2tgba.cc: Add option -fu to test it.
* src/bin/common_post.cc: Adjust the group of options so we can easily
add more from ltl2tgba.cc.
* src/bin/ltl2tgba.cc: Add support for -U and --unambigous.
* src/twaalgos/translate.cc, src/twaalgos/translate.hh: Add support
for Unambiguous.
* src/tests/ltlcross.test, src/tests/ltlcross2.test: Test both
bin/ltl2tgba and tgbatest/ltl2tgba.
* NEWS: Mention the change.

NEWS

@@ -221,6 +221,12 @@ New in spot 1.99b (not yet released)
       new style can be requested from command-line tools using option
       --spin=6 (or -s6 for short).
 
+    - Support for building unambiguous automata.  ltl_to_tgba() has a
+      new options to produce unambiguous TGBA, i.e., TGBAs in which
+      every word is accepted by at most one path.  The ltl2tgba
+      command line has a new option, --unambigous (or -U) to produce
+      these automata.
+
   * Noteworthy code changes
 
     - Boost is not used anymore.

src/bin/common_post.cc

@@ -37,11 +37,11 @@ static const argp_option options[] =
   {
     /**************************************************/
     { 0, 0, 0, 0, "Translation intent:", 20 },
-    { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 },
+    { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 20 },
-    { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 },
+    { "deterministic", 'D', 0, 0, "prefer deterministic automata", 20 },
-    { "any", 'a', 0, 0, "no preference", 0 },
+    { "any", 'a', 0, 0, "no preference", 20 },
     { "complete", 'C', 0, 0, "output a complete automaton (combine "
-      "with other intents)", 0 },
+      "with other intents)", 20 },
     /**************************************************/
     { 0, 0, 0, 0, "Optimization level:", 21 },
     { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 },

src/bin/ltl2tgba.cc

@@ -63,7 +63,8 @@ static const argp_option options[] =
     /**************************************************/
     { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "the formula, in Spot's syntax", 4 },
-   /**************************************************/
+    /**************************************************/
+    { "unambiguous", 'U', 0, 0, "produce unambiguous automata", 20 },
     { 0, 0, 0, 0, "Miscellaneous options:", -1 },
     { "extra-options", 'x', "OPTS", 0,
       "fine-tuning options (see spot-x (7))", 0 },
@@ -81,6 +82,7 @@ const struct argp_child children[] =
   };
 
 static spot::option_map extra_options;
+bool unambiguous = false;
 
 static int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -94,6 +96,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case 'M':
       type = spot::postprocessor::Monitor;
       break;
+    case 'U':
+      unambiguous = true;
+      break;
     case 'x':
       {
 	const char* opt = extra_options.parse_options(arg);
@@ -175,6 +180,24 @@ main(int argc, char** argv)
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
     exit(err);
 
+  // Using both --unambiguous --deterministic do not really make
+  // sense.
+  if (unambiguous)
+    {
+      if (type == spot::postprocessor::Monitor)
+	{
+	  // We do not now how to make unambiguous monitors, other
+	  // than deterministic monitors.
+	  unambiguous = false;
+	  pref = spot::postprocessor::Deterministic;
+	}
+      else if (pref == spot::postprocessor::Deterministic)
+	{
+	  error(2, 0,
+		"--unambiguous and --deterministic are incompatible options");
+	}
+    }
+
   if (jobs.empty())
     error(2, 0, "No formula to translate?  Run '%s --help' for usage.",
 	  program_name);
@@ -183,6 +206,8 @@ main(int argc, char** argv)
   trans.set_pref(pref | comp);
   trans.set_type(type);
   trans.set_level(level);
+  if (unambiguous)
+    trans.set_pref(spot::translator::Unambiguous);
 
   try
     {

src/tests/ltl2tgba.cc

@@ -146,6 +146,7 @@ syntax(char* prog)
 	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
 	    << "  -fr   reduce formula at each step of FM" << std::endl
 	    << "          as specified with the -r{1..7} options" << std::endl
+	    << "  -fu   build unambiguous automata" << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
             << "  -p    branching postponement (implies -f)" << std::endl
             << "  -U[PROPS]  consider atomic properties of the formula as "
@@ -330,6 +331,7 @@ checked_main(int argc, char** argv)
   bool fm_red = false;
   bool fm_exprop_opt = false;
   bool fm_symb_merge_opt = true;
+  bool fm_unambiguous = false;
   bool file_opt = false;
   bool degen_reset = true;
   bool degen_order = false;
@@ -512,6 +514,12 @@ checked_main(int argc, char** argv)
 	  fm_red = true;
 	  translation = TransFM;
 	}
+      else if (!strcmp(argv[formula_index], "-fu"))
+	{
+	  fm_unambiguous = true;
+	  fm_exprop_opt = true;
+	  translation = TransFM;
+	}
       else if (!strcmp(argv[formula_index], "-F"))
 	{
 	  file_opt = true;
@@ -1060,7 +1068,8 @@ checked_main(int argc, char** argv)
 				       post_branching,
 				       fair_loop_approx,
 				       unobservables,
-				       fm_red ? simp : 0);
+				       fm_red ? simp : 0,
+				       fm_unambiguous);
 	      break;
 	    case TransCompo:
 	      {

src/tests/ltlcross.test

@@ -41,6 +41,7 @@ EOF
 ../../bin/ltlcross --products=2 \
   "$ltl2tgba -t -f %f > %T" \
   "$ltl2tgba -t -f -y %f > %T" \
+  "$ltl2tgba -t -f -fu %f > %T" \
   "$ltl2tgba -t -f -r4 %f > %T" \
   "$ltl2tgba -t -f -R3 %f > %T" \
   "$ltl2tgba -t -f -R3 -Rm %f > %T" \

src/tests/ltlcross2.test

@@ -43,4 +43,6 @@ ltl2tgba=../../bin/ltl2tgba
 "$ltl2tgba --spin=6 --ba --medium %f > %N" \
 "$ltl2tgba --hoa  -BDC %f > %H" \
 "$ltl2tgba --lbtt -BC %f > %T" \
+"$ltl2tgba --lbtt --unambiguous --low %f > %T" \
+"$ltl2tgba --lbtt --unambiguous --high %f > %T" \
 --json=output.json --csv=output.csv

src/twaalgos/ltl2tgba_fm.cc

@@ -142,7 +142,7 @@ namespace spot
       translate_dict(const bdd_dict_ptr& dict,
 		     acc_cond& acc,
 		     ltl_simplifier* ls, bool exprop,
-		     bool single_acc)
+		     bool single_acc, bool unambiguous)
 	: dict(dict),
 	  ls(ls),
 	  a_set(bddtrue),
@@ -151,7 +151,8 @@ namespace spot
 	  transdfa(*this),
 	  exprop(exprop),
 	  single_acc(single_acc),
-	  acc(acc)
+	  acc(acc),
+	  unambiguous(unambiguous)
       {
       }
 
@@ -187,6 +188,7 @@ namespace spot
       acc_cond& acc;
       // Map BDD variables to acceptance marks.
       std::map<int, unsigned> bm;
+      bool unambiguous;
 
       enum translate_flags
 	{
@@ -1289,6 +1291,15 @@ namespace spot
       {
       }
 
+      bdd
+      neg_of(const formula* node)
+      {
+	const formula* n = dict_.ls->negative_normal_form(node, true);
+	bdd r = recurse(n);
+	n->destroy();
+	return r;
+      }
+
       void
       reset(bool mark_all)
       {
@@ -1360,6 +1371,8 @@ namespace spot
 	      bdd a = bdd_ithvar(dict_.register_a_variable(child));
 	      if (!recurring_)
 		a &= bdd_ithvar(dict_.register_next_variable(node));
+	      if (dict_.unambiguous)
+		a &= neg_of(child);
 	      res_ = y | a;
 	      break;
 	    }
@@ -1575,6 +1588,8 @@ namespace spot
 	      f1 &= bdd_ithvar(dict_.register_a_variable(node->second()));
 	      if (!recurring_)
 		f1 &= bdd_ithvar(dict_.register_next_variable(node));
+	      if (dict_.unambiguous)
+		f1 &= neg_of(node->second());
 	      res_ = f2 | f1;
 	      break;
 	    }
@@ -1589,6 +1604,8 @@ namespace spot
 	      bdd f2 = recurse(node->second());
 	      if (!recurring_)
 		f1 &= bdd_ithvar(dict_.register_next_variable(node));
+	      if (dict_.unambiguous)
+		f1 &= neg_of(node->second());
 	      res_ = f2 | f1;
 	      break;
 	    }
@@ -1601,10 +1618,15 @@ namespace spot
 			     || node->first() == constant::false_instance());
 	      // r(f1 R f2) = r(f2)(r(f1) + X(f1 R f2))  if not recurring
 	      // r(f1 R f2) = r(f2)                      if recurring
-	      if (recurring_)
+	      if (recurring_ && !dict_.unambiguous)
 		break;
 	      bdd f1 = recurse(node->first());
-	      res_ &= f1 | bdd_ithvar(dict_.register_next_variable(node));
+	      bdd f2 = bddtrue;
+	      if (!recurring_)
+		f2 = bdd_ithvar(dict_.register_next_variable(node));
+	      if (dict_.unambiguous)
+		f2 &= neg_of(node->first());
+	      res_ &= f1 | f2;
 	      break;
 	    }
 	  case binop::M:
@@ -1630,6 +1652,8 @@ namespace spot
 	      bdd a = bdd_ithvar(dict_.register_a_variable(node));
 	      if (!recurring_)
 		a &= bdd_ithvar(dict_.register_next_variable(node));
+	      if (dict_.unambiguous)
+		a &= neg_of(node->first());
 	      res_ &= f1 | a;
 	      break;
 	    }
@@ -1805,11 +1829,28 @@ namespace spot
 	    }
 	  case multop::Or:
 	    {
-	      res_ = bddfalse;
+	      if (!dict_.unambiguous)
-	      unsigned s = node->size();
+		{
-	      for (unsigned n = 0; n < s; ++n)
+		  res_ = bddfalse;
-		res_ |= recurse(node->nth(n));
+		  unsigned s = node->size();
-	      break;
+		  for (unsigned n = 0; n < s; ++n)
+		    res_ |= recurse(node->nth(n));
+		  break;
+		}
+	      else
+		{
+		  bdd prev = bddtrue;
+		  res_ = bddfalse;
+		  unsigned s = node->size();
+		  for (unsigned n = 0; n < s; ++n)
+		    {
+		      const formula* sub = node->nth(n);
+		      res_ |= prev & recurse(sub);
+		      prev &= neg_of(sub);
+		    }
+		  break;
+
+		}
 	    }
 	  case multop::Concat:
 	  case multop::Fusion:
@@ -2202,7 +2243,7 @@ namespace spot
   ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict,
 		 bool exprop, bool symb_merge, bool branching_postponement,
 		 bool fair_loop_approx, const atomic_prop_set* unobs,
-		 ltl_simplifier* simplifier)
+		 ltl_simplifier* simplifier, bool unambiguous)
   {
     const formula* f2;
     ltl_simplifier* s = simplifier;
@@ -2232,7 +2273,8 @@ namespace spot
     twa_graph_ptr a = make_twa_graph(dict);
     auto namer = a->create_namer<const formula*>();
 
-    translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence());
+    translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence(),
+		     unambiguous);
 
     // Compute the set of all promises that can possibly occur
     // inside the formula.

src/twaalgos/ltl2tgba_fm.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
-// Développement de l'Epita (LRDE).
+// Recherche et Développement de l'Epita (LRDE).
 // 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.
@@ -120,6 +120,24 @@ namespace spot
       }
       \endverbatim */
   ///
+  /// \param unambiguous When true, unambigous TGBA will be produced using
+  /// the trick described in the following paper.
+  /** \verbatim
+      @InProceedings{	  benedikt.13.tacas,
+        author	  = {Michael Benedikt and Rastislav Lenhardt and James
+      		     Worrell},
+        title     = {{LTL} Model Checking of Interval Markov Chains},
+        booktitle = {19th International Conference on Tools and Algorithms for
+      		     the Construction and Analysis of Systems (TACAS'13)},
+        year      = {2013},
+        pages     = {32--46},
+        series	  = {Lecture Notes in Computer Science},
+        volume	  = {7795},
+        editor	  = {Nir Piterman and Scott A. Smolka},
+        publisher = {Springer}
+      }
+      \endvarbatim */
+  ///
   /// \return A spot::twa_graph that recognizes the language of \a f.
   SPOT_API twa_graph_ptr
   ltl_to_tgba_fm(const ltl::formula* f, const bdd_dict_ptr& dict,
@@ -127,5 +145,6 @@ namespace spot
 		 bool branching_postponement = false,
 		 bool fair_loop_approx = false,
 		 const ltl::atomic_prop_set* unobs = 0,
-		 ltl::ltl_simplifier* simplifier = 0);
+		 ltl::ltl_simplifier* simplifier = 0,
+		 bool unambiguous = false);
 }

src/twaalgos/translate.cc

@@ -28,6 +28,7 @@ namespace spot
   void translator::setup_opt(const option_map* opt)
   {
     comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
+    unambiguous_ = false;
 
     if (!opt)
       return;
@@ -63,6 +64,21 @@ namespace spot
 
   twa_graph_ptr translator::run(const ltl::formula** f)
   {
+    if (unambiguous_)
+      {
+	if (type_ == postprocessor::Monitor)
+	  {
+	    // Deterministic monitor are unambiguous, so the
+	    // unambiguous option is not really relevant for monitors.
+	    unambiguous_ = false;
+	    set_pref(postprocessor::Deterministic);
+	  }
+	else if (pref_ == postprocessor::Deterministic)
+	  {
+	    unambiguous_ = false;
+	  }
+      }
+
     const ltl::formula* r = simpl_->simplify(*f);
     (*f)->destroy();
     *f = r;
@@ -74,9 +90,10 @@ namespace spot
     twa_graph_ptr aut;
     if (comp_susp_ > 0)
       {
+	// FIXME: Handle unambiguous_ automata?
 	int skel_wdba = skel_wdba_;
 	if (skel_wdba < 0)
-	  skel_wdba = (pref_ == spot::postprocessor::Deterministic) ? 1 : 2;
+	  skel_wdba = (pref_ == postprocessor::Deterministic) ? 1 : 2;
 
 	aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0,
 		       skel_simul_ == 0, early_susp_ != 0,
@@ -84,8 +101,9 @@ namespace spot
       }
     else
       {
-	bool exprop = level_ == spot::postprocessor::High;
+	bool exprop = unambiguous_ || level_ == postprocessor::High;
-	aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop);
+	aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
+			     true, false, false, 0, 0, unambiguous_);
       }
     aut = this->postprocessor::run(aut, r);
     return aut;

src/twaalgos/translate.hh

@@ -83,6 +83,7 @@ namespace spot
     }
 
     typedef postprocessor::output_pref output_pref;
+    enum output_pref_extra { Unambiguous };
 
     void
     set_pref(output_pref pref)
@@ -90,6 +91,13 @@ namespace spot
       this->postprocessor::set_pref(pref);
     }
 
+    void
+    set_pref(output_pref_extra)
+    {
+      unambiguous_ = true;
+    }
+
+
     typedef postprocessor::optimization_level optimization_level;
 
     void
@@ -122,6 +130,7 @@ namespace spot
     int early_susp_;
     int skel_wdba_;
     int skel_simul_;
+    bool unambiguous_;
   };
   /// @}
 }