From 9e959cdc7eec8a9b02b8541d8d42d40fc05b7df9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 17 Apr 2015 15:18:47 +0200
Subject: [PATCH] stutter: new variant of Etessami's check

* src/tgbaalgos/stutter.cc: Add a new variant of Etessami's check,
closer to his original paper in IPL.
* src/ltltest/stutter.test: Add more tests.
* bench/stutter/user.sh: Include this new variant in the benchmark.
---
 bench/stutter/user.sh    |  4 ++--
 src/ltltest/stutter.test | 25 ++++++++++++++++++++++++-
 src/tgbaalgos/stutter.cc | 24 +++++++++++++++++++-----
 3 files changed, 45 insertions(+), 8 deletions(-)

diff --git a/bench/stutter/user.sh b/bench/stutter/user.sh
index 5800ef514..fae92303e 100755
--- a/bench/stutter/user.sh
+++ b/bench/stutter/user.sh
@@ -8,9 +8,9 @@ set -e -x
 (
 must_exit=false
 echo ap,algo,time,matched,exit.status
-for ap in 1 2 3 4; do
+for ap in 1 2 3; do
     $RANDLTL $ap --tree-size=..30 -n -1 | $LTLFILT --ap=$ap | $LTLFILT -v --nox -n 500 > formulas
-    for algo in 1 2 3 4 5 6 7 8 0; do
+    for algo in 1 2 3 4 5 6 7 8 0 9; do
 	es=0
 	SPOT_STUTTER_CHECK=$algo /usr/bin/time -o user-$ap-$algo.csv -f "$ap,$algo,%e" $LTLFILT --stutter-invariant formulas > matched-$ap-$algo.ltl || must_exit=true es=$?
 	matched=`wc -l < matched-$ap-$algo.ltl`
diff --git a/src/ltltest/stutter.test b/src/ltltest/stutter.test
index 327eccc73..636692564 100755
--- a/src/ltltest/stutter.test
+++ b/src/ltltest/stutter.test
@@ -42,7 +42,7 @@ for i in 10 12 14 16 18 20; do
   $randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
 done
 
-# We do not check i=0, it is too slow.
+# We do not check i=0 and i=9, as they are too slow.
 for i in 1 2 3 4 5 6 7 8; do
     SPOT_STUTTER_CHECK=$i
     export SPOT_STUTTER_CHECK
@@ -53,3 +53,26 @@ done
 for i in 2 3 4 5 6 7 8; do
     diff res.1 res.$i
 done
+
+
+# Do a similar test on fewer formulas, so we can cover 0 and 9.
+cat >$FILE <<EOF
+F(a & X(!a & b))
+F(a & X(!a & Xb))
+F(a & X!a & Xb)
+F(a & X(a & Xb))
+F(a & Xb)
+Xa
+EOF
+
+# We do not check i=0 and i=9, as they are too slow.
+for i in 0 1 2 3 4 5 6 7 8 9; do
+    SPOT_STUTTER_CHECK=$i
+    export SPOT_STUTTER_CHECK
+    $time $ltlfilt --stutter-invariant -F $FILE > res.$i
+done
+
+# All results should be equal
+for i in 1 2 3 4 5 6 7 8 9; do
+    diff res.0 res.$i
+done
diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc
index a9c5c4bd2..916ef556f 100644
--- a/src/tgbaalgos/stutter.cc
+++ b/src/tgbaalgos/stutter.cc
@@ -25,8 +25,10 @@
 #include "ltlvisit/apcollect.hh"
 #include "translate.hh"
 #include "ltlast/unop.hh"
+#include "ltlast/binop.hh"
 #include "ltlvisit/remove_x.hh"
 #include "tgbaalgos/product.hh"
+#include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgba/bddprint.hh"
 #include <deque>
@@ -542,7 +544,7 @@ namespace spot
       {
 	char* endptr;
 	long res = strtol(stutter_check, &endptr, 10);
-	if (*endptr || res < 0 || res > 8)
+	if (*endptr || res < 0 || res > 9)
 	  throw
 	    std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
 	return res;
@@ -561,16 +563,28 @@ namespace spot
 
     int algo = default_stutter_check_algorithm();
 
-    if (algo == 0) // Etessami's check via syntactic transformation.
+    if (algo == 0 || algo == 9)
+      // Etessami's check via syntactic transformation.
       {
 	if (!f->is_ltl_formula())
 	  throw std::runtime_error("Cannot use the syntactic "
 				   "stutter-invariance check "
 				   "for non-LTL formulas");
 	const ltl::formula* g = remove_x(f);
-	ltl::ltl_simplifier ls;
-	bool res = ls.are_equivalent(f, g);
-	g->destroy();
+	bool res;
+	if (algo == 0)		// Equivalence check
+	  {
+	    ltl::ltl_simplifier ls;
+	    res = ls.are_equivalent(f, g);
+	    g->destroy();
+	  }
+	else
+	  {
+	    const ltl::formula* h = ltl::binop::instance(ltl::binop::Xor,
+							 f->clone(), g);
+	    res = ltl_to_tgba_fm(h, make_bdd_dict())->is_empty();
+	    h->destroy();
+	  }
 	return res;
       }