ltl2tgba_fm: produce unambiguous automata for PSL as well

* src/twaalgos/ltl2tgba_fm.cc: Fix the PSL operators.
* src/tests/unambig.test: Add more tests.

src/tests/unambig.test

@@ -31,7 +31,8 @@ for f in 'Ga' \
          'Ga | FGb' \
          'XFGa | GFb | Gc' \
          '(Ga -> Gb) W c' \
-	 'F(a & !b & (!c W b))'
+	 'F(a & !b & (!c W b))' \
+         'G({{1;1}*}<>->a)'
 do
   $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
   $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous
@@ -39,7 +40,7 @@ do
   $ltl2tgba -UH "!($f)" | $autfilt --check | grep unambiguous
 done
 
-for f in FGa
+for f in FGa '(({p1[*0..1]}[]-> 0) R XFp0)'
 do
   $ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous
   $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
@@ -86,3 +87,9 @@ EOF
 run 1 $autfilt -q --is-unambiguous input
 run 0 $autfilt --check input > output
 test `grep -c unambiguous output` = 0
+
+# Check 1000 random PSL formulas
+../../bin/randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H |
+  $autfilt -v --is-unamb --stats=%M && exit 1
+
+:

src/twaalgos/ltl2tgba_fm.cc

@@ -1690,15 +1690,33 @@ namespace spot
 
 		      const formula* dest2 =
 			binop::instance(op, dest, node->second()->clone());
-
+		      bool unamb = dict_.unambiguous;
 		      if (dest2 != constant::false_instance())
 			{
+			  // If the rhs is Boolean, the
+			  // unambiguous code will produce a more
+			  // deterministic automaton at no additional
+			  // cost.  You can test this on
+			  //   G({{1;1}*}<>->a)
+			  if (node->second()->is_boolean())
+			    unamb = true;
+
 			  int x = dict_.register_next_variable(dest2);
 			  dest2->destroy();
-			  res_ |= label & bdd_ithvar(x);
+			  bdd toadd = label & bdd_ithvar(x);
+			  if (dest->accepts_eword() && unamb)
+			    toadd &= neg_of(node->second());
+			  res_ |= toadd;
 			}
 		      if (dest->accepts_eword())
-			res_ |= label & f2;
+			{
+			  bdd toadd = label & f2;
+			  if (unamb)
+			    // Preserve determinism
+			    toadd &= bdd_ithvar(dict_.register_next_variable
+						(constant::true_instance()));
+			  res_ |= toadd;
+			}
 		    }
 		}
 	      else
@@ -1739,24 +1757,49 @@ namespace spot
 	      // word should recognize f2, and the automaton for f1
 	      // should be understood as universal.
 	      //
-	      // The crux of this translation (the use of implication,
+	      // The crux of this translation (i.e., the
-	      // and the interpretation as a universal automaton) was
+	      // interpretation of first() as a universal automaton,
-	      // explained to me (adl) by Felix Klaedtke.
+	      // and using implication to encode it)  was explained
+	      // to me (adl) by Felix Klaedtke.
 	      bdd f2 = recurse(node->second());
 	      bdd f1 = translate_ratexp(node->first(), dict_);
-	      res_ = bddtrue;
 
-	      bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
+	      if (exprop_)
-	      bdd all_props = bdd_existcomp(f1, dict_.var_set);
-	      while (all_props != bddfalse)
 		{
+		  res_ = bddfalse;
+		  bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
+		  bdd all_props = bdd_existcomp(f1, dict_.var_set);
+		  bdd missing = !all_props;
+		  while (all_props != bddfalse)
+		    {
+		      bdd label = bdd_satoneset(all_props, var_set, bddtrue);
+		      all_props -= label;
 
-		  bdd one_prop_set = bddtrue;
+		      const formula* dest =
-		  if (exprop_)
+			dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set));
-		    one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
-		  all_props -= one_prop_set;
 
-		  minato_isop isop(f1 & one_prop_set);
+		      const formula* dest2 =
+			binop::instance(op, dest, node->second()->clone());
+
+		      bdd udest =
+			bdd_ithvar(dict_.register_next_variable(dest2));
+
+		      if (dest->accepts_eword())
+			udest &= f2;
+
+		      dest2->destroy();
+		      res_ |= label & udest;
+		    }
+		  // Make the automaton complete.
+		  res_ |= missing &
+		    // stick X(1) to preserve determinism.
+		    bdd_ithvar(dict_.register_next_variable
+			       (constant::true_instance()));
+		}
+	      else
+		{
+		  res_ = bddtrue;
+		  minato_isop isop(f1);
 		  bdd cube;
 		  while ((cube = isop.next()) != bddfalse)
 		    {
@@ -1773,7 +1816,6 @@ namespace spot
 			udest &= f2;
 
 		      dest2->destroy();
-
 		      res_ &= bdd_apply(label, udest, bddop_imp);
 		    }
 		}
@@ -2081,42 +2123,52 @@ namespace spot
 	  {
 	    bdd res = bddfalse;
 
-	    minato_isop isop(t.symbolic);
+	    bdd var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set);
-	    bdd cube;
+	    bdd all_props = bdd_existcomp(t.symbolic, d_.var_set);
-	    while ((cube = isop.next()) != bddfalse)
+	    while (all_props != bddfalse)
 	      {
-		bdd label = bdd_exist(cube, d_.next_set);
+		bdd one_prop_set = bddtrue;
-		bdd dest_bdd = bdd_existcomp(cube, d_.next_set);
+		if (d_.exprop)
-		const formula* dest =
+		  one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
-		  d_.conj_bdd_to_formula(dest_bdd);
+		all_props -= one_prop_set;
 
-		// Handle a Miyano-Hayashi style unrolling for
+		minato_isop isop(t.symbolic & one_prop_set);
-		// rational operators.  Marked nodes correspond to
+		bdd cube;
-		// subformulae in the Miyano-Hayashi set.
+		while ((cube = isop.next()) != bddfalse)
-		const formula* tmp =  d_.mt.simplify_mark(dest);
+		  {
-		dest->destroy();
+		    bdd label = bdd_exist(cube, d_.next_set);
-		dest = tmp;
+		    bdd dest_bdd = bdd_existcomp(cube, d_.next_set);
+		    const formula* dest =
+		      d_.conj_bdd_to_formula(dest_bdd);
 
-		if (dest->is_marked())
+		    // Handle a Miyano-Hayashi style unrolling for
-		  {
+		    // rational operators.  Marked nodes correspond to
-		    // Make the promise that we will exit marked sets.
+		    // subformulae in the Miyano-Hayashi set.
-		    int a =
+		    const formula* tmp =  d_.mt.simplify_mark(dest);
-		      d_.register_a_variable(constant::true_instance());
-		    label &= bdd_ithvar(a);
-		  }
-		else
-		  {
-		    // We have no marked operators, but still
-		    // have other rational operator to check.
-		    // Start a new marked cycle.
-		    const formula* dest2 = d_.mt.mark_concat_ops(dest);
 		    dest->destroy();
-		    dest = dest2;
+		    dest = tmp;
+
+		    if (dest->is_marked())
+		      {
+			// Make the promise that we will exit marked sets.
+			int a =
+			  d_.register_a_variable(constant::true_instance());
+			label &= bdd_ithvar(a);
+		      }
+		    else
+		      {
+			// We have no marked operators, but still
+			// have other rational operator to check.
+			// Start a new marked cycle.
+			const formula* dest2 = d_.mt.mark_concat_ops(dest);
+			dest->destroy();
+			dest = dest2;
+		      }
+		    // Note that simplify_mark may have changed dest.
+		    dest_bdd = bdd_ithvar(d_.register_next_variable(dest));
+		    dest->destroy();
+		    res |= label & dest_bdd;
 		  }
-		// Note that simplify_mark may have changed dest.
-		dest_bdd = bdd_ithvar(d_.register_next_variable(dest));
-		dest->destroy();
-		res |= label & dest_bdd;
 	      }
 	    t.symbolic = res;
 //	    std::cerr << "Marking rewriting:" << std::endl;