From 31b3a228053bf9186ce58db220ca6053020c25ff Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 20 May 2012 12:43:02 +0200
Subject: [PATCH] FM: Simplify promises of U, M, and F formulae.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Simplify promises by replacing P(a U b), P(b M a), and P(Fb), by P(b).
---
 src/tgbaalgos/ltl2tgba_fm.cc | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 7c35046f3..ceacaa333 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -236,6 +236,36 @@ namespace spot
       int
       register_a_variable(const formula* f)
       {
+	// A promise of 'x', noted P(x) is pretty much like the F(x)
+	// LTL formula, it ensure that 'x' will be fulfilled (= not
+	// promised anymore) eventually.
+	// So   a U b = ((a&Pb) W b)
+	//      a U (b U c) = (a&P(b U c)) W (b&P(c) W c)
+	// the latter encoding may be simplified to
+	//      a U (b U c) = (a&P(c)) W (b&P(c) W c)
+	//
+	// 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))
+	  {
+	    binop::type op = b->op();
+	    if (op == binop::U)
+	      f = b->second();
+	    else if (op == binop::M)
+	      f = b->first();
+	    else
+	      break;
+	  }
+	if (const unop* u = is_unop(f, unop::F))
+	  {
+	    f = u->child();
+	    goto again;
+	  }
 	int num = dict->register_acceptance_variable(f, this);
 	a_set &= bdd_ithvar(num);
 	return num;