ltl2tgba_fm: Fix incorrect simplification of promises for M

The bug was reported by Joachim Klein.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Reduce P(a M b) to P(a & b), not to P(a).
* src/tgbatest/ltlcross.test: Test Joachim's formula.
* src/tgbatest/ltl2ta.test: Adjust some expected values.
* NEWS: Mention the bug.

NEWS

@@ -7,6 +7,10 @@ New in spot 1.2.4a (not yet released)
 
   * Bug fixes:
 
+    - Fix incorrect simplification of promises in the translation
+      of the M operator (you may suffer from the bug even if you do
+      not use this operator as some LTL patterns are automatically
+      reduced to it).
     - Fix simplification of bounded repetition in SERE formulas.
     - Fix parsing of neverclaims produced by Modella.
     - Fix a memory leak in the little-used conversion from

src/tgbaalgos/ltl2tgba_fm.cc

@@ -254,24 +254,59 @@ namespace spot
 	// Similarly
 	//      a M b = (a R (b&P(a)))
 	//      (a M b) M c = (a R (b & Pa)) R (c & P(a M b))
-	//                  = (a R (b & Pa)) R (c & P(a))
-	// The rules also apply to F:
-	//   P(F(a)) = P(a)
-      again:
-	while (const binop* b = is_binop(f))
+	//                  = (a R (b & Pa)) R (c & P(a & b))
+	//
+	// The code below therefore implement the following
+	// rules:
+	// P(a U b) = P(b)
+	// P(F(a))  = P(a)
+	// P(a M b) = P(a & b)
+	//
+	// The latter rule INCORRECTLY appears as P(a M b)=P(a)
+	// in section 3.5 of
+	//    "LTL translation improvements in Spot 1.0",
+	//     A. Duret-Lutz. IJCCBS 5(1/2):31-54, March 2014.
+	// and was unfortunately implemented this way until Spot
+	// 1.2.4.  A counterexample is given by the formula
+	//    G(Fa & ((a M b) U ((c U !d) M d)))
+	// that was found by Joachim Klein.  Here P((c U !d) M d)
+	// and P(c U !d) should not both be simplified to P(!d).
+	for (;;)
 	  {
-	    binop::type op = b->op();
-	    if (op == binop::U)
-	      f = b->second();
-	    else if (op == binop::M)
-	      f = b->first();
+	    if (const binop* b = is_binop(f))
+	      {
+		binop::type op = b->op();
+		if (op == binop::U)
+		  {
+		    // P(a U b) = P(b)
+		    f = b->second();
+		  }
+		else if (op == binop::M)
+		  {
+		    // P(a M b) = P(a & b)
+		    const formula* g =
+		      multop::instance(multop::And,
+				       b->first()->clone(),
+				       b->second()->clone());
+		    int num = dict->register_acceptance_variable(g, this);
+		    a_set &= bdd_ithvar(num);
+		    g->destroy();
+		    return num;
+		  }
+		else
+		  {
+		    break;
+		  }
+	      }
+	    else if (const unop* u = is_unop(f, unop::F))
+	      {
+		// P(F(a)) = P(a)
+		f = u->child();
+	      }
 	    else
-	      break;
-	  }
-	if (const unop* u = is_unop(f, unop::F))
-	  {
-	    f = u->child();
-	    goto again;
+	      {
+		break;
+	      }
 	  }
 	int num = dict->register_acceptance_variable(f, this);
 	a_set &= bdd_ithvar(num);
@@ -1521,9 +1556,23 @@ namespace spot
 	    {
 	      res_ = recurse(node->second(), recurring_);
 	      bdd f1 = recurse(node->first());
-	      // r(f1 M f2) = r(f2)(r(f1) + a(f1)X(f1 M f2)) if not recurring
-	      // r(f1 M f2) = r(f2)(r(f1) + a(f1))           if recurring
-	      bdd a = bdd_ithvar(dict_.register_a_variable(node->first()));
+	      // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2)X(f1 M f2)) if not recurring
+	      // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2))           if recurring
+	      //
+	      // Note that the rule above differs from the one given
+	      // in Figure 2 of
+	      //    "LTL translation improvements in Spot 1.0",
+	      //     A. Duret-Lutz. IJCCBS 5(1/2):31-54, March 2014.
+	      // Both rules should be OK, but this one is a better fit
+	      // to the promises simplifications performed in
+	      // register_a_variable() (see comments in this function).
+	      // We do not want a U (c M d) to generate two different
+	      // promises.  Generating c&d also makes the output similar
+	      // to what we would get with the equivalent a U (d U (c & d)).
+	      //
+	      // Here we just appear to emit a(f1 M f2) and the conversion
+	      // to a(f1&f2) is done  by register_a_variable().
+	      bdd a = bdd_ithvar(dict_.register_a_variable(node));
 	      if (!recurring_)
 		a &= bdd_ithvar(dict_.register_next_variable(node));
 	      res_ &= f1 | a;

src/tgbatest/ltl2ta.test

 #!/bin/sh
-# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 # Dveloppement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -133,46 +133,46 @@ grep 'states: 21$' stdout
 f="FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)"
 
 run 0 ../ltl2tgba -TA -RT -ks -in -R3f -x  -DS  "$f" >stdout
-grep 'transitions: 450$' stdout
-grep 'states: 38$' stdout
+grep 'transitions: 505$' stdout
+grep 'states: 40$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x  -DS  "$f" >stdout
-grep 'transitions: 551$' stdout
-grep 'states: 40$' stdout
+grep 'transitions: 616$' stdout
+grep 'states: 42$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks "$f" >stdout
-grep 'transitions: 424$' stdout
-grep 'states: 31$' stdout
+grep 'transitions: 498$' stdout
+grep 'states: 34$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -sp -lv -in "$f" >stdout
-grep 'transitions: 485$' stdout
-grep 'states: 32$' stdout
+grep 'transitions: 566$' stdout
+grep 'states: 35$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -in -R3 -x  -DS  "$f" >stdout
-grep 'transitions: 450$' stdout
-grep 'states: 38$' stdout
+grep 'transitions: 505$' stdout
+grep 'states: 40$' stdout
 
 run 0 ../ltl2tgba -TA -RT -ks -sp -lv -R3 -x   -DS "$f" >stdout
-grep 'transitions: 551$' stdout
-grep 'states: 40$' stdout
+grep 'transitions: 616$' stdout
+grep 'states: 42$' stdout
 
 
 run 0 ../ltl2tgba -TA -ks -sp -lv -DS "$f" >stdout
-grep 'transitions: 597$' stdout
-grep 'states: 46$' stdout
+grep 'transitions: 819$' stdout
+grep 'states: 56$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -sp -lv "$f" >stdout
-grep 'transitions: 504$' stdout
-grep 'states: 33$' stdout
+grep 'transitions: 585$' stdout
+grep 'states: 36$' stdout
 
 run 0 ../ltl2tgba -TGTA -RT -ks "$f" >stdout
-grep 'transitions: 527$' stdout
-grep 'states: 32$' stdout
+grep 'transitions: 598$' stdout
+grep 'states: 35$' stdout
 
 g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))"
 

src/tgbatest/ltlcross.test

 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,7 +23,13 @@ set -e
 
 ltl2tgba=../ltl2tgba
 
-../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 |
+
+(
+# A bug reported by Joachim Klein
+echo 'G(Fa & ((a M b) U ((c U !d) M d)))'
+# Random formulas
+../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15
+) |
 ../../bin/ltlcross --products=2 \
   "$ltl2tgba -t -l %f > %T" \
   "$ltl2tgba -t -l -R3b -r4 %f > %T" \
@@ -47,7 +53,3 @@ ltl2tgba=../ltl2tgba
   "$ltl2tgba -t -taa -r4 %f > %T" \
   "$ltl2tgba -t -taa -r4 -c %f > %T" \
   "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T"
-
-# Disabled because too slow, and too big automata produced.
-# "$ltl2tgba -t -lo -r4 %f > %T"
-# "$ltl2tgba -t -lo -R3b -r4 %f > %T" \