From 9460e0761e8cc294148b0fc0719493f919391e6b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 18 Jun 2012 18:25:07 +0200
Subject: [PATCH] FM: Translate X(a&b) as if it were X(a)&X(b).

This helps reducing (p&XF!p)|(!p&XFp)|X(Fp&F!p) to (p&XF!p)|(!p&XFp).

* src/tgbaalgos/ltl2tgba_fm.cc: Adjust rewriting rules of X.
* src/tgbatest/ltl2tgba.test: Add a test case.
---
 src/tgbaalgos/ltl2tgba_fm.cc | 48 ++++++++++++++++++++++++++++++++++--
 src/tgbatest/ltl2tgba.test   |  5 ++++
 2 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index ceacaa333..b76b92f6b 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1307,8 +1307,52 @@ namespace spot
 	  case unop::X:
 	    {
 	      // r(Xy) = Next[y]
-	      int x = dict_.register_next_variable(node->child());
-	      res_ = bdd_ithvar(x);
+	      // r(X(a&b&c)) = Next[a]&Next[b]&Next[c]
+	      // r(X(a|b|c)) = Next[a]|Next[b]|Next[c]
+	      //
+	      // The special case for And is to that
+	      // (p&XF!p)|(!p&XFp)|X(Fp&F!p)      (1)
+	      // get translated as
+	      // (p&XF!p)|(!p&XFp)|XFp&XF!p       (2)
+	      // and then automatically reduced to
+	      // (p&XF!p)|(!p&XFp)
+	      //
+	      // Formula (2) appears as an example of Boolean
+	      // simplification in Wring, but our LTL rewriting
+	      // rules tend to rewrite it as (1).
+	      //
+	      // The special case for Or follows naturally, but it's
+	      // effect is less clear.  Benchmarks show that it
+	      // reduces the number of states and transitions, but it
+	      // increases the number of non-deterministic states...
+	      const formula* y = node->child();
+	      if (const multop* m = is_And(y))
+		{
+		  res_ = bddtrue;
+		  unsigned s = m->size();
+		  for (unsigned n = 0; n < s; ++n)
+		    {
+		      int x = dict_.register_next_variable(m->nth(n));
+		      res_ &= bdd_ithvar(x);
+		    }
+		}
+#if 0
+	      else if (const multop* m = is_Or(y))
+		{
+		  res_ = bddfalse;
+		  unsigned s = m->size();
+		  for (unsigned n = 0; n < s; ++n)
+		    {
+		      int x = dict_.register_next_variable(m->nth(n));
+		      res_ |= bdd_ithvar(x);
+		    }
+		}
+#endif
+	      else
+		{
+		  int x = dict_.register_next_variable(y);
+		  res_ = bdd_ithvar(x);
+		}
 	      break;
 	    }
 	  case unop::Closure:
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index 008b5c64b..3421611b3 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -201,3 +201,8 @@ run 0 ../ltl2tgba -XN -kt out.never > count.never
 run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot
 run 0 ../ltl2tgba -X -kt out.spot > count.spot
 cmp count.never count.spot
+
+# The following automaton should have only 4 states.
+run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout
+grep 'transitions: 7$' stdout
+grep 'states: 4$' stdout