ltl2tgba_fm: fix translation of !{f} as done last year for {f}

* src/tgbaalgos/ltl2tgba_fm.cc: Fix.
* src/tgbatest/randpsl.test: Rewrite using ltlcross and add a testcase.
* NEWS: Mention it.

NEWS

@@ -31,6 +31,9 @@ New in spot 1.2.4a (not yet released)
       not use this operator as some LTL patterns are automatically
       reduced to it).
     - Fix simplification of bounded repetition in SERE formulas.
+    - Fix incorrect translation of PSL formulas of the form !{f} where
+      f is unsatisifable.  A similar bug was fixed for {f} in Spot
+      1.1.4, but for some reason it was not fixed for !{f}.
     - Fix parsing of neverclaims produced by Modella.
     - Fix a memory leak in the little-used conversion from
       transition-based alternating automata to tgba.

src/tgbaalgos/ltl2tgba_fm.cc

@@ -1438,48 +1438,51 @@ namespace spot
 	  case unop::NegClosure:
 	    rat_seen_ = true;
 	    {
-	      const formula* c = node->child();
 	      if (mark_all_)
 		{
 		  op = unop::NegClosureMarked;
 		  has_marked_ = true;
 		}
-	      bdd f1 = translate_ratexp(c, dict_);
 
-	      // trace_ltl_bdd(dict_, f1);
+	      const formula* f = node->child();
+	      tgba_succ_iterator* i = dict_.transdfa.succ(f);
+	      res_ = bddtrue;
 
-	      bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
-	      bdd all_props = bdd_existcomp(f1, dict_.var_set);
+	      if (!i)
+		break;
 
-	      res_ = !all_props &
-		// stick X(1) to preserve determinism.
-		bdd_ithvar(dict_.register_next_variable
-			   (constant::true_instance()));
-
-	      while (all_props != bddfalse)
+	      res_ = bddfalse;
+	      bdd missing = bddtrue;
+	      for (i->first(); !i->done(); i->next())
 		{
-		  bdd label = bdd_satoneset(all_props, var_set, bddtrue);
-		  all_props -= label;
+		  bdd label = i->current_condition();
+		  state* s = i->current_state();
+		  const formula* dest = dict_.transdfa.get_label(f, s);
+		  s->destroy();
 
-		  const formula* dest =
-		    dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set));
+		  missing -= label;
 
-		  // !{ Exp } is false if Exp accepts the empty word.
 		  if (dest->accepts_eword())
 		    {
 		      dest->destroy();
-		      continue;
 		    }
-
-		  const formula* dest2 = unop::instance(op, dest);
-
-		  if (dest2 == constant::false_instance())
-		    continue;
-
-		  int x = dict_.register_next_variable(dest2);
-		  dest2->destroy();
-		  res_ |= label & bdd_ithvar(x);
+		  else
+		    {
+		      const formula* dest2 = unop::instance(op, dest);
+		      if (dest2 == constant::false_instance())
+			continue;
+		      int x = dict_.register_next_variable(dest2);
+		      dest2->destroy();
+		      res_ |= label & bdd_ithvar(x);
+		    }
 		}
+	      delete i;
+
+	      res_ |= missing &
+		// stick X(1) to preserve determinism.
+		bdd_ithvar(dict_.register_next_variable
+			   (constant::true_instance()));
+	      //trace_ltl_bdd(dict_, res_);
 	    }
 	    break;
 

src/tgbatest/randpsl.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,23 +22,10 @@
 
 set -e
 
-check_psl()
-{
-  # Do not use "run", this is too slow.
-
-  # Make cross products with FM
-  ../ltl2tgba -f -R3 -b "$1" > out.tgba
-  ../ltl2tgba -f -R3 -Pout.tgba -E "!($1)"
-  # Also try with -x turned on.
-  ../ltl2tgba -f -x -R3 -b "$1" > out.tgba
-  ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)"
-}
-
 # Generate 50 random unique PSL formula that do not simplify to LTL
 # formulae, and that have a size of at lease 12.
 ../../bin/randltl -n -1 --tree-size 30 --seed 0 --psl a b c |
 ../../bin/ltlfilt -r --size-min 12 --unique |
 ../../bin/ltlfilt -v --ltl | head -n 50 |
-while read formula; do
-  check_psl "$formula"
-done
+../../bin/ltlcross '../ltl2tgba -R3 -t %f >%T' '../ltl2tgba -x -R3 -t %f >%T' \
+  -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}'