diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index f241a6443..51455e8dd 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -60,13 +60,13 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
 nenoform_SOURCES = equals.cc
 nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
 reduc_SOURCES = reduc.cc
-reduccmp_SOURCES = equals.cc
+reduccmp_SOURCES = equalsf.cc
 reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
 reduceu_SOURCES = equals.cc
 reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
 reductau_SOURCES = equals.cc
 reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
-reductaustr_SOURCES = equals.cc
+reductaustr_SOURCES = equalsf.cc
 reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
 syntimpl_SOURCES = syntimpl.cc
 tostring_SOURCES = tostring.cc
diff --git a/src/ltltest/equalsf.cc b/src/ltltest/equalsf.cc
new file mode 100644
index 000000000..f4a345814
--- /dev/null
+++ b/src/ltltest/equalsf.cc
@@ -0,0 +1,251 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include <iostream>
+#include <fstream>
+#include <sstream>
+#include <cassert>
+#include <cstdlib>
+#include <cstring>
+#include "ltlparse/public.hh"
+#include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/tunabbrev.hh"
+#include "ltlvisit/dump.hh"
+#include "ltlvisit/wmunabbrev.hh"
+#include "ltlvisit/nenoform.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/simplify.hh"
+#include "ltlvisit/tostring.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " [-E] file" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  bool check_first = true;
+
+  if (argc > 1 && !strcmp(argv[1], "-E"))
+    {
+      check_first = false;
+      argv[1] = argv[0];
+      ++argv;
+      --argc;
+    }
+  if (argc != 2)
+    syntax(argv[0]);
+  std::ifstream input(argv[1]);
+
+  std::string s;
+  unsigned line = 0;
+  while (std::getline(input, s))
+    {
+      ++line;
+      std::cerr << line << ": " << s << '\n';
+      if (s[0] == '#')		// Skip comments
+	continue;
+      std::vector<std::string> formulas;
+      {
+	std::istringstream ss(s);
+	std::string form;
+	while (std::getline(ss, form, ','))
+	  formulas.push_back(form);
+      }
+
+      unsigned size = formulas.size();
+      if (size == 0)		// Skip empty lines
+	continue;
+
+      if (size == 1)
+	{
+	  std::cerr << "Not enough formulas on line " << line << '\n';
+	  return 2;
+	}
+
+      spot::ltl::parse_error_list p2;
+      const spot::ltl::formula* f2 = spot::ltl::parse(formulas[size - 1], p2);
+
+      if (spot::ltl::format_parse_errors(std::cerr, formulas[size - 1], p2))
+	return 2;
+
+      for (unsigned n = 0; n < size - 1; ++n)
+	{
+
+	  spot::ltl::parse_error_list p1;
+	  const spot::ltl::formula* f1 = spot::ltl::parse(formulas[n], p1);
+
+	  if (check_first &&
+	      spot::ltl::format_parse_errors(std::cerr, formulas[n], p1))
+	    return 2;
+
+	  int exit_code = 0;
+
+	  {
+#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
+	    const spot::ltl::formula* tmp;
+#endif
+#ifdef LUNABBREV
+	    tmp = f1;
+	    f1 = spot::ltl::unabbreviate_logic(f1);
+	    tmp->destroy();
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef TUNABBREV
+	    tmp = f1;
+	    f1 = spot::ltl::unabbreviate_ltl(f1);
+	    tmp->destroy();
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef WM
+	    tmp = f1;
+	    f1 = spot::ltl::unabbreviate_wm(f1);
+	    tmp->destroy();
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef NENOFORM
+	    tmp = f1;
+	    f1 = spot::ltl::negative_normal_form(f1);
+	    tmp->destroy();
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef REDUC
+	    spot::ltl::ltl_simplifier_options opt(true, true, true,
+						  false, false);
+#  ifdef EVENT_UNIV
+	    opt.favor_event_univ = true;
+#  endif
+	    spot::ltl::ltl_simplifier simp(opt);
+	    {
+	      const spot::ltl::formula* tmp;
+	      tmp = f1;
+	      f1 = simp.simplify(f1);
+
+	      if (!simp.are_equivalent(f1, tmp))
+		{
+		  std::cerr
+		    << "Source and simplified formulae are not equivalent!\n";
+		  std::cerr
+		    << "Simplified: " << spot::ltl::to_string(f1) << '\n';
+		  exit_code = 1;
+		}
+
+	      tmp->destroy();
+	    }
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef REDUC_TAU
+	    spot::ltl::ltl_simplifier_options opt(false, false, false,
+						  true, false);
+	    spot::ltl::ltl_simplifier simp(opt);
+	    {
+	      const spot::ltl::formula* tmp;
+	      tmp = f1;
+	      f1 = simp.simplify(f1);
+
+	      if (!simp.are_equivalent(f1, tmp))
+		{
+		  std::cerr
+		    << "Source and simplified formulae are not equivalent!\n";
+		  std::cerr
+		    << "Simplified: " << spot::ltl::to_string(f1) << '\n';
+		  exit_code = 1;
+		}
+
+	      tmp->destroy();
+	    }
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+#ifdef REDUC_TAUSTR
+	    spot::ltl::ltl_simplifier_options opt(false, false, false,
+						  true, true);
+	    spot::ltl::ltl_simplifier simp(opt);
+	    {
+	      const spot::ltl::formula* tmp;
+	      tmp = f1;
+	      f1 = simp.simplify(f1);
+
+	      if (!simp.are_equivalent(f1, tmp))
+		{
+		  std::cerr
+		    << "Source and simplified formulae are not equivalent!\n";
+		  std::cerr
+		    << "Simplified: " << spot::ltl::to_string(f1) << '\n';
+		  exit_code = 1;
+		}
+
+	      tmp->destroy();
+	    }
+	    spot::ltl::dump(std::cout, f1);
+	    std::cout << std::endl;
+#endif
+
+	    exit_code |= f1 != f2;
+
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
+	    spot::ltl::ltl_simplifier simp;
+#endif
+
+	    if (!simp.are_equivalent(f1, f2))
+	      {
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
+		std::cerr
+		  << "Source and destination formulae are not equivalent!\n";
+#else
+		std::cerr
+		  << "Simpl. and destination formulae are not equivalent!\n";
+#endif
+		exit_code = 1;
+	      }
+
+	    if (exit_code)
+	      {
+		spot::ltl::dump(std::cerr, f1) << std::endl;
+		spot::ltl::dump(std::cerr, f2) << std::endl;
+		return exit_code;
+	      }
+
+	  }
+	  f1->destroy();
+	}
+      f2->destroy();
+    }
+
+  spot::ltl::atomic_prop::dump_instances(std::cerr);
+  spot::ltl::unop::dump_instances(std::cerr);
+  spot::ltl::binop::dump_instances(std::cerr);
+  spot::ltl::multop::dump_instances(std::cerr);
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  return 0;
+}
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 0ff861728..ab59c8033 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -25,368 +25,373 @@
 # Check LTL reductions
 
 . ./defs || exit 1
+set -e
 
-for x in ../reduccmp ../reductaustr; do
+cat >common.txt <<EOF
+# No reduction
+a U b, a U b
+a R b, a R b
+a & b, a & b
+a | b, a | b
+a & (a U b), a & (a U b)
+a | (a U b), a | (a U b)
 
-  # No reduction
-  run 0 $x 'a U b' 'a U b'
-  run 0 $x 'a R b' 'a R b'
-  run 0 $x 'a & b' 'a & b'
-  run 0 $x 'a | b' 'a | b'
-  run 0 $x 'a & (a U b)' 'a & (a U b)'
-  run 0 $x 'a | (a U b)' 'a | (a U b)'
+# Syntactic reduction
+a & (!b R !a), false
+(!b R !a) & a, false
+a & (!b R !a) & c, false
+c & (!b R !a) & a, false
 
-  # Syntactic reduction
-  run 0 $x 'a & (!b R !a)' 'false'
-  run 0 $x '(!b R !a) & a' 'false'
-  run 0 $x 'a & (!b R !a) & c' 'false'
-  run 0 $x 'c & (!b R !a) & a' 'false'
+a & (!b M !a), false
+(!b M !a) & a, false
+a & (!b M !a) & c, false
+c & (!b M !a) & a, false
 
-  run 0 $x 'a & (!b M !a)' 'false'
-  run 0 $x '(!b M !a) & a' 'false'
-  run 0 $x 'a & (!b M !a) & c' 'false'
-  run 0 $x 'c & (!b M !a) & a' 'false'
+a & (b U a), a
+(b U a) & a, a
+a | (b U a), (b U a)
+(b U a) | a, (b U a)
+a U (b U a), (b U a)
 
-  run 0 $x 'a & (b U a)' 'a'
-  run 0 $x '(b U a) & a' 'a'
-  run 0 $x 'a | (b U a)' '(b U a)'
-  run 0 $x '(b U a) | a' '(b U a)'
-  run 0 $x 'a U (b U a)' '(b U a)'
+a & (b W a), a
+(b W a) & a, a
+a | (b W a), (b W a)
+(b W a) | a, (b W a)
+a W (b W a), (b W a)
 
-  run 0 $x 'a & (b W a)' 'a'
-  run 0 $x '(b W a) & a' 'a'
-  run 0 $x 'a | (b W a)' '(b W a)'
-  run 0 $x '(b W a) | a' '(b W a)'
-  run 0 $x 'a W (b W a)' '(b W a)'
+a & (b U a) & a, a
+a & (b U a) & a, a
+a | (b U a) | a, (b U a)
+a | (b U a) | a, (b U a)
+a U (b U a), (b U a)
 
-  run 0 $x 'a & (b U a) & a' 'a'
-  run 0 $x 'a & (b U a) & a' 'a'
-  run 0 $x 'a | (b U a) | a' '(b U a)'
-  run 0 $x 'a | (b U a) | a' '(b U a)'
-  run 0 $x 'a U (b U a)' '(b U a)'
+a & c & (b W a), a & c
+a & d & c & e & f & g & b & (x W (g & f)), a&b&c&d&e&f&g
+(F!a & X(!b R a)) | (Ga & X(b U !a)), F!a & X(!b R a)
+d & ((!a & d) | (a & d)), (!a & d) | (a & d)
 
-  run 0 $x 'a & c & (b W a)' 'a & c'
-  run 0 $x 'a & d & c & e & f & g & b & (x W (g & f))' 'a&b&c&d&e&f&g'
-  run 0 $x '(F!a & X(!b R a)) | (Ga & X(b U !a))' 'F!a & X(!b R a)'
-  run 0 $x 'd & ((!a & d) | (a & d))' '(!a & d) | (a & d)'
+a <-> !a, 0
+a <-> a, 1
+a ^ a, 0
+a ^ !a, 1
 
-  run 0 $x 'a <-> !a' '0'
-  run 0 $x 'a <-> a' '1'
-  run 0 $x 'a ^ a' '0'
-  run 0 $x 'a ^ !a' '1'
+GFa | FGa, GFa
+XXGa | GFa, GFa
+GFa & FGa, FGa
+XXGa & GFa, XXGa
 
-  run 0 $x 'GFa | FGa' 'GFa'
-  run 0 $x 'XXGa | GFa' 'GFa'
-  run 0 $x 'GFa & FGa' 'FGa'
-  run 0 $x 'XXGa & GFa' 'XXGa'
+# Basic reductions
+X(true), true
+X(false), false
+F(true), true
+F(false), false
 
-  # Basic reductions
-  run 0 $x 'X(true)' 'true'
-  run 0 $x 'X(false)' 'false'
-  run 0 $x 'F(true)' 'true'
-  run 0 $x 'F(false)' 'false'
+XGF(f), GF(f)
 
-  run 0 $x 'XGF(f)' 'GF(f)'
+# not reduced
+a R (b W G(c)), a R (b W G(c))
+# not reduced.
+a M ((a&b) R c), a M ((a&b) R c)
+# not reduced.
+(a&b) W (a U c), (a&b) W (a U c)
 
-  case $x in
-   *tau*);;
-   *)
-     run 0 $x 'G(true)' 'true'
-     run 0 $x 'G(false)' 'false'
+# Eventuality and universality class reductions
+FFa, Fa
+FGFa, GFa
+b U Fa, Fa
+b U GFa, GFa
+Ga, Ga
 
-     run 0 $x 'a M 1' 'Fa'
-     run 0 $x 'a W 0' 'Ga'
-     run 0 $x '1 U a' 'Fa'
-     run 0 $x '0 R a' 'Ga'
+a U XXXFb, XXXFb
+EOF
 
-     run 0 $x 'G(a R b)' 'G(b)'
+cp common.txt nottau.txt
+cat >>nottau.txt<<EOF
+G(true), true
+G(false), false
 
-     run 0 $x 'FX(a)' 'XF(a)'
-     run 0 $x 'GX(a)' 'XG(a)'
+a M 1, Fa
+a W 0, Ga
+1 U a, Fa
+0 R a, Ga
 
-     run 0 $x '(Xf W 0) | X(f W 0)' 'XGf'
-     run 0 $x 'XFa & FXa' 'XFa'
+G(a R b), G(b)
 
-     run 0 $x 'GF(a | Xb)' 'GF(a | b)'
-     run 0 $x 'GF(a | Fb)' 'GF(a | b)'
-     run 0 $x 'GF(Xa | Fb)' 'GF(a | b)'
-     run 0 $x 'FG(a & Xb)' 'FG(a & b)'
-     run 0 $x 'FG(a & Gb)' 'FG(a & b)'
-     run 0 $x 'FG(Xa & Gb)' 'FG(a & b)'
+FX(a), XF(a)
+GX(a), XG(a)
 
-     run 0 $x 'X(a) U X(b)' 'X(a U b)'
-     run 0 $x 'X(a) R X(b)' 'X(a R b)'
-     run 0 $x 'Xa & Xb' 'X(a & b)'
-     run 0 $x 'Xa | Xb' 'X(a | b)'
+(Xf W 0) | X(f W 0), XGf
+XFa & FXa, XFa
 
-     run 0 $x 'X(a) M X(b)' 'X(a M b)'
-     run 0 $x 'X(a) W X(b)' 'X(a W b)'
-     run 0 $x 'X(a) M b' 'b & X(b U a)'
-     run 0 $x 'X(a) R b' 'b & X(b W a)'
-     run 0 $x 'X(a) U b' 'b | X(b M a)'
-     run 0 $x 'X(a) W b' 'b | X(b R a)'
+GF(a | Xb), GF(a | b)
+GF(a | Fb), GF(a | b)
+GF(Xa | Fb), GF(a | b)
+FG(a & Xb), FG(a & b)
+FG(a & Gb), FG(a & b)
+FG(Xa & Gb), FG(a & b)
 
-     run 0 $x '(a U b) & (c U b)' '(a & c) U b'
-     run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
-     run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
-     run 0 $x '(a R b) | (c R b)' '(a | c) R b'
+X(a) U X(b), X(a U b)
+X(a) R X(b), X(a R b)
+Xa & Xb, X(a & b)
+Xa | Xb, X(a | b)
 
-     run 0 $x 'Xa & FGb' 'X(a & FGb)'
-     run 0 $x 'Xa | FGb' 'X(a | FGb)'
-     run 0 $x 'Xa & GFb' 'X(a & GFb)'
-     run 0 $x 'Xa | GFb' 'X(a | GFb)'
-     # The following is not reduced to F(a) & GFb.  because
-     # (1) is does not help the translate the formula into a
-     #     smaller automaton, and ...
-     run 0 $x 'F(a & GFb)' 'F(a & GFb)'
-     # (2) ... it would hinder this useful reduction (that helps to
-     #     produce a smaller automaton)
-     run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
-     # FIXME: Don't we want the opposite rewriting?
-     # rewriting Fa & GFb as  F(a & GFb) seems better, but
-     # it not clear how that scales to Fa & Fb & GFc...
-     run 0 $x 'Fa & GFb' 'Fa & GFb'
-     run 0 $x 'G(a | GFb)' 'Ga | GFb'
-     # The following is not reduced to F(a & c) & GF(b) for the same
-     # reason as above.
-     run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
-     run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
+X(a) M X(b), X(a M b)
+X(a) W X(b), X(a W b)
+X(a) M b, b & X(b U a)
+X(a) R b, b & X(b W a)
+X(a) U b, b | X(b M a)
+X(a) W b, b | X(b R a)
 
-     run 0 $x 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)'
+(a U b) & (c U b), (a & c) U b
+(a R b) & (a R c), a R (b & c)
+(a U b) | (a U c), a U (b | c)
+(a R b) | (c R b), (a | c) R b
 
-     run 0 $x 'Gb W a' 'Gb|a'
-     run 0 $x 'Fb M Fa' 'Fa & Fb'
+Xa & FGb, X(a & FGb)
+Xa | FGb, X(a | FGb)
+Xa & GFb, X(a & GFb)
+Xa | GFb, X(a | GFb)
+# The following is not reduced to F(a) & GFb.  because
+# (1) is does not help the translate the formula into a
+#     smaller automaton, and ...
+F(a & GFb), F(a & GFb)
+# (2) ... it would hinder this useful reduction (that helps to
+#     produce a smaller automaton)
+F(f1 & GF(f2)) | F(a & GF(b)), F((f1&GFf2)|(a&GFb))
+# FIXME: Don't we want the opposite rewriting?
+# rewriting Fa & GFb as  F(a & GFb) seems better, but
+# it not clear how that scales to Fa & Fb & GFc...
+Fa & GFb, Fa & GFb
+G(a | GFb), Ga | GFb
+# The following is not reduced to F(a & c) & GF(b) for the same
+# reason as above.
+F(a & GFb & c), F(a & GFb & c)
+G(a | GFb | c), G(a | c) | GFb
 
-     run 0 $x 'a U (b | G(a) | c)' 'a W (b | c)'
-     run 0 $x 'a U (G(a))' 'Ga'
-     run 0 $x '(a U b) | (a W c)' 'a W (b | c)'
-     run 0 $x '(a U b) | Ga' 'a W b'
+GFa <=> GFb, G(Fa&Fb)|FG(!a&!b)
 
-     run 0 $x 'a R (b & F(a) & c)' 'a M (b & c)'
-     run 0 $x 'a R (F(a))' 'Fa'
-     run 0 $x '(a R b) & (a M c)' 'a M (b & c)'
-     run 0 $x '(a R b) & Fa' 'a M b'
+Gb W a, Gb|a
+Fb M Fa, Fa & Fb
 
-     run 0 $x '(a U b) & (c W b)' '(a & c) U b'
-     run 0 $x '(a W b) & (c W b)' '(a & c) W b'
-     run 0 $x '(a R b) | (c M b)' '(a | c) R b'
-     run 0 $x '(a M b) | (c M b)' '(a | c) M b'
+a U (b | G(a) | c), a W (b | c)
+a U (G(a)), Ga
+(a U b) | (a W c), a W (b | c)
+(a U b) | Ga, a W b
 
-     run 0 $x '(a R b) | Gb' 'a R b'
-     run 0 $x '(a M b) | Gb' 'a R b'
-     run 0 $x '(a U b) & Fb' 'a U b'
-     run 0 $x '(a W b) & Fb' 'a U b'
-     run 0 $x '(a M b) | Gb | (c M b)' '(a | c) R b'
+a R (b & F(a) & c), a M (b & c)
+a R (F(a)), Fa
+(a R b) & (a M c), a M (b & c)
+(a R b) & Fa, a M b
 
-     run 0 $x 'GFGa' 'FGa'
-     run 0 $x 'b R Ga' 'Ga'
-     run 0 $x 'b R FGa' 'FGa'
+(a U b) & (c W b), (a & c) U b
+(a W b) & (c W b), (a & c) W b
+(a R b) | (c M b), (a | c) R b
+(a M b) | (c M b), (a | c) M b
 
-     run 0 $x 'G(!a M a) M 1' '0'
-     run 0 $x 'G(!a M a) U 1' '1'
-     run 0 $x 'a R (!a M a)' '0'
-     run 0 $x 'a W (!a M a)' 'Ga'
+(a R b) | Gb, a R b
+(a M b) | Gb, a R b
+(a U b) & Fb, a U b
+(a W b) & Fb, a U b
+(a M b) | Gb | (c M b), (a | c) R b
 
-     run 0 $x 'F(a U b)' 'Fb'
-     run 0 $x 'F(a M b)' 'F(a & b)'
-     run 0 $x 'G(a R b)' 'Gb'
-     run 0 $x 'G(a W b)' 'G(a | b)'
+GFGa, FGa
+b R Ga, Ga
+b R FGa, FGa
 
-     run 0 $x 'Fa W Fb' 'F(GFa | b)'
-     run 0 $x 'Ga M Gb' 'FGa & Gb'
+G(!a M a) M 1, 0
+G(!a M a) U 1, 1
+a R (!a M a), 0
+a W (!a M a), Ga
 
-     run 0 $x 'a & XGa' 'Ga'
-     run 0 $x 'a & XG(a&b)' '(XGb)&(Ga)'
-     run 0 $x 'a & b & XG(a&b)'  'G(a&b)'
-     run 0 $x 'a & b & X(Ga&Gb)'  'G(a&b)'
-     run 0 $x 'a & b & XGa &XG(b)'  'G(a&b)'
-     run 0 $x 'a & b & XGa & XGc' 'b & Ga & XGc'
-     run 0 $x 'a & b & X(G(a&d) & b) & X(Gc)' 'b & Ga & X(b & G(c&d))'
-     run 0 $x 'a|b|c|X(F(a|b)|F(c)|Gd)' 'F(a|b|c)|XGd'
-     run 0 $x 'b|c|X(F(a|b)|F(c)|Gd)' 'b|c|X(F(a|b|c)|Gd)'
+F(a U b), Fb
+F(a M b), F(a & b)
+G(a R b), Gb
+G(a W b), G(a | b)
 
-     run 0 $x 'a | (Xa R b) | c' '(b W a) | c'
-     run 0 $x 'a | (Xa M b) | c' '(b U a) | c'
-     run 0 $x 'a | (Xa M b) | (Xa R c)' '(b U a) | (c W a)'
-     run 0 $x 'a | (Xa M b) | XF(a)' 'Fa'
-     run 0 $x 'a | (Xa R b) | XF(a)' '(b W a) | Fa' # Gb | Fa ?
-     run 0 $x 'a & (Xa W b) & c' '(b R a) & c'
-     run 0 $x 'a & (Xa U b) & c' '(b M a) & c'
-     run 0 $x 'a & (Xa W b) & (Xa U c)' '(b R a) & (c M a)'
-     run 0 $x 'a & (Xa W b) & XGa' 'Ga'
-     run 0 $x 'a & (Xa U b) & XGa' '(b M a) & Ga'  # Fb & Ga ?
-     run 0 $x 'a|(c&b&X((b&c) U a))|d' '((b&c) U a)|d'
-     run 0 $x 'a|(c&X((b&c) W a)&b)|d' '((b&c) W a)|d'
-     run 0 $x 'a&(c|b|X((b|c) M a))&d' '((b|c) M a)&d'
-     run 0 $x 'a&(c|X((b|c) R a)|b)&d' '((b|c) R a)&d'
-     run 0 $x 'g R (f|g|h)' '(f|h) W g'
-     run 0 $x 'g M (f|g|h)' '(f|h) U g'
-     run 0 $x 'g U (f&g&h)' '(f&h) M g'
-     run 0 $x 'g W (f&g&h)' '(f&h) R g'
+Fa W Fb, F(GFa | b)
+Ga M Gb, FGa & Gb
 
-     # Syntactic implication
-     run 0 $x '(a & b) R (a R c)' '(a & b)R c'
-     run 0 $x 'a R ((a & b) R c)' '(a & b)R c'
-     run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
-     run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
-     run 0 $x '(a & b) M (a R c)' '(a & b)M c'
-     run 0 $x '(a & b) M (a M c)' '(a & b)M c'
+a & XGa, Ga
+a & XG(a&b), (XGb)&(Ga)
+a & b & XG(a&b), G(a&b)
+a & b & X(Ga&Gb), G(a&b)
+a & b & XGa &XG(b), G(a&b)
+a & b & XGa & XGc, b & Ga & XGc
+a & b & X(G(a&d) & b) & X(Gc), b & Ga & X(b & G(c&d))
+a|b|c|X(F(a|b)|F(c)|Gd), F(a|b|c)|XGd
+b|c|X(F(a|b)|F(c)|Gd), b|c|X(F(a|b|c)|Gd)
 
-     run 0 $x 'a U ((a & b) U c)' 'a U c'
-     run 0 $x '(a&c) U (b R (c U d))' 'b R (c U d)'
-     run 0 $x '(a&c) U (b R (c W d))' 'b R (c W d)'
-     run 0 $x '(a&c) U (b M (c U d))' 'b M (c U d)'
-     run 0 $x '(a&c) U (b M (c W d))' 'b M (c W d)'
+a | (Xa R b) | c, (b W a) | c
+a | (Xa M b) | c, (b U a) | c
+a | (Xa M b) | (Xa R c), (b U a) | (c W a)
+a | (Xa M b) | XF(a), Fa
+# Gb | Fa ?
+a | (Xa R b) | XF(a), (b W a) | Fa
+a & (Xa W b) & c, (b R a) & c
+a & (Xa U b) & c, (b M a) & c
+a & (Xa W b) & (Xa U c), (b R a) & (c M a)
+a & (Xa W b) & XGa, Ga
+# Fb & Ga ?
+a & (Xa U b) & XGa, (b M a) & Ga
+a|(c&b&X((b&c) U a))|d, ((b&c) U a)|d
+a|(c&X((b&c) W a)&b)|d, ((b&c) W a)|d
+a&(c|b|X((b|c) M a))&d, ((b|c) M a)&d
+a&(c|X((b|c) R a)|b)&d, ((b|c) R a)&d
+g R (f|g|h), (f|h) W g
+g M (f|g|h), (f|h) U g
+g U (f&g&h), (f&h) M g
+g W (f&g&h), (f&h) R g
 
-     run 0 $x '(a R c) R (b & a)' 'c R (b & a)'
-     run 0 $x '(a M c) R (b & a)' 'c R (b & a)'
+# Syntactic implication
+(a & b) R (a R c), (a & b)R c
+a R ((a & b) R c), (a & b)R c
+a R ((a & b) M c), (a & b)M c
+a M ((a & b) M c), (a & b)M c
+(a & b) M (a R c), (a & b)M c
+(a & b) M (a M c), (a & b)M c
 
-     run 0 $x 'a W ((a&b) U c)' 'a W c'
-     run 0 $x 'a W ((a&b) W c)' 'a W c'
+a U ((a & b) U c), a U c
+(a&c) U (b R (c U d)), b R (c U d)
+(a&c) U (b R (c W d)), b R (c W d)
+(a&c) U (b M (c U d)), b M (c U d)
+(a&c) U (b M (c W d)), b M (c W d)
 
-     run 0 $x '(a M c) M (b&a)' 'c M (b&a)'
+(a R c) R (b & a), c R (b & a)
+(a M c) R (b & a), c R (b & a)
 
-     run 0 $x '((a&c) U b) U c' 'b U c'
-     run 0 $x '((a&c) W b) U c' 'b U c'
-     run 0 $x '((a&c) U b) W c' 'b W c'
-     run 0 $x '((a&c) W b) W c' 'b W c'
-     run 0 $x '(a R b) R (c&a)' 'b R (c&a)'
-     run 0 $x '(a M b) R (c&a)' 'b R (c&a)'
-     run 0 $x '(a R b) M (c&a)' 'b M (c&a)'
-     run 0 $x '(a M b) M (c&a)' 'b M (c&a)'
+a W ((a&b) U c), a W c
+a W ((a&b) W c), a W c
 
-     run 0 $x '(a R (b&c)) R (c)' '(a&b&c) R c'
-     run 0 $x '(a M (b&c)) R (c)' '(a&b&c) R c'
-     run 0 $x '(a R (b&c)) M (c)' '(a R (b&c)) M (c)' # not reduced
-     run 0 $x '(a M (b&c)) M (c)' '(a&b&c) M c'
-     run 0 $x '(a W (c&b)) W b' '(a W (c&b)) | b'
-     run 0 $x '(a U (c&b)) W b' '(a U (c&b)) | b'
-     run 0 $x '(a U (c&b)) U b' '(a U (c&b)) | b'
-     run 0 $x '(a W (c&b)) U b' '(a W (c&b)) U b' # not reduced
+(a M c) M (b&a), c M (b&a)
 
+((a&c) U b) U c, b U c
+((a&c) W b) U c, b U c
+((a&c) U b) W c, b W c
+((a&c) W b) W c, b W c
+(a R b) R (c&a), b R (c&a)
+(a M b) R (c&a), b R (c&a)
+(a R b) M (c&a), b M (c&a)
+(a M b) M (c&a), b M (c&a)
 
-     # Eventuality and universality class reductions
-     run 0 $x 'Fa M b' 'Fa & b'
-     run 0 $x 'GFa M b' 'GFa & b'
+(a R (b&c)) R (c), (a&b&c) R c
+(a M (b&c)) R (c), (a&b&c) R c
+# not reduced
+(a R (b&c)) M (c), (a R (b&c)) M (c)
+(a M (b&c)) M (c), (a&b&c) M c
+(a W (c&b)) W b, (a W (c&b)) | b
+(a U (c&b)) W b, (a U (c&b)) | b
+(a U (c&b)) U b, (a U (c&b)) | b
+# not reduced
+(a W (c&b)) U b, (a W (c&b)) U b
 
-     run 0 $x 'Fa|Xb|GFc' 'Fa | X(b|GFc)'
-     run 0 $x 'Fa|GFc' 'F(a|GFc)'
-     run 0 $x 'FGa|GFc' 'F(Ga|GFc)'
-     run 0 $x 'Ga&Xb&FGc' 'Ga & X(b&FGc)'
-     run 0 $x 'Ga&Xb&GFc' 'Ga & X(b&GFc)'
-     run 0 $x 'Ga&GFc' 'G(a&Fc)'
-     run 0 $x 'G(a|b|GFc|GFd|FGe|FGf)' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
-     run 0 $x 'G(a|b)|GFc|GFd|FGe|FGf' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
-     run 0 $x 'X(a|b)|GFc|GFd|FGe|FGf' 'X(a|b|GF(c|d)|F(Ge|Gf))'
-     run 0 $x 'Xa&Xb&GFc&GFd&Ge' 'X(a&b&G(Fc&Fd))&Ge'
+# Eventuality and universality class reductions
+Fa M b, Fa & b
+GFa M b, GFa & b
 
-     # F comes in front when possible...
-     run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)'
-     run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)'
+Fa|Xb|GFc, Fa | X(b|GFc)
+Fa|GFc, F(a|GFc)
+FGa|GFc, F(Ga|GFc)
+Ga&Xb&FGc, Ga & X(b&FGc)
+Ga&Xb&GFc, Ga & X(b&GFc)
+Ga&GFc, G(a&Fc)
+G(a|b|GFc|GFd|FGe|FGf), G(a|b)|GF(c|d)|F(Ge|Gf)
+G(a|b)|GFc|GFd|FGe|FGf, G(a|b)|GF(c|d)|F(Ge|Gf)
+X(a|b)|GFc|GFd|FGe|FGf, X(a|b|GF(c|d)|F(Ge|Gf))
+Xa&Xb&GFc&GFd&Ge, X(a&b&G(Fc&Fd))&Ge
 
-     # Because reduccmp will translate the formula,
-     # this also check for an old bug in ltl2tgba_fm.
-     run 0 $x '{(c&!c)[->0..1]}!' '0'
+# F comes in front when possible...
+GFc|GFd|FGe|FGf, F(GF(c|d)|Ge|Gf)
+G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
 
-     # Tricky case that used to break the translator,
-     # because it was translating closer on-the-fly
-     # without pruning the rational automaton.
-     run 0 $x '{(c&!c)[=2]}' '0'
+# Because reduccmp will translate the formula,
+# this also check for an old bug in ltl2tgba_fm.
+{(c&!c)[->0..1]}!, 0
 
-     run 0 $x '{a && b && c*} <>-> d' 'a&b&c&d'
-     run 0 $x '{a && b && c[*1..3]} <>-> d' 'a&b&c&d'
-     run 0 $x '{a && b && c[->0..2]} <>-> d' 'a&b&c&d'
-     run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d'
-     run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d'
-     run 0 $x '{a && b && d[=2]} <>-> d' '0'
-     run 0 $x '{a && b && d[*2..]} <>-> d' '0'
-     run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
-     run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d'
-     run 0 $x '{a && {b;c}} <>-> d' '0'
-     run 0 $x '{a && {(b;c):e}} <>-> d' '0'
-     run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better
-     run 0 $x '{a && {(b*;c*):e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem
-     run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d'
-     run 0 $x '{a && {(b*;c):e}} <>-> d' 'a & c & d & e'
-     run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
-     run 0 $x '{a && {(b;c*):e}} <>-> d' 'a & b & d & e'
-     run 0 $x '{{{b1;r1*}&&{b2;r2*}};c}' 'b1&b2&X{{r1*&&r2*};c}'
-     run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}'
-     run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'
-     run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}'
-     run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
-              '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
-     run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
-     run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
-     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
-     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced
-     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced
-     run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
-              '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
-     run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
-     run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
-     run 0 $x '{[*]}[]->b' 'Gb'
-     run 0 $x '{a;[*]}[]->b' 'Gb | !a'
-     run 0 $x '{[*];a}[]->b' 'G(b | !a)'
-     run 0 $x '{a;b;[*]}[]->c' '!a | X(!b | Gc)'
-     run 0 $x '{a;a;[*]}[]->c' '!a | X(!a | Gc)'
-     run 0 $x '{s[*]}[]->b' 'b W !s'
-     run 0 $x '{s[+]}[]->b' 'b W !s'
-     run 0 $x '{s[*2..]}[]->b' '!s | X(b W !s)'
-     run 0 $x '{a;b*;c;d*}[]->e' '!a | X(!b R ((e & X(e W !d)) | !c))'
-     run 0 $x '{a:b*:c:d*}[]->e' '!a | ((!c | (e W !d)) W !b)'
-     run 0 $x '{a|b*|c|d*}[]->e' '(e | !(a | c)) & (e W !b) & (e W !d)'
-     run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
-	      '{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'
+# Tricky case that used to break the translator,
+# because it was translating closer on-the-fly
+# without pruning the rational automaton.
+{(c&!c)[=2]}, 0
 
-     run 0 $x '{a&b&c*}<>->!Xb' '(a & b & X!b) | (a & b & c & X(c U !b))'
-     run 0 $x '{[*]}<>->b' 'Fb'
-     run 0 $x '{a;[*]}<>->b' 'Fb & a'
-     run 0 $x '{[*];a}<>->b' 'F(a & b)'
-     run 0 $x '{a;b;[*]}<>->c' 'a & X(b & Fc)'
-     run 0 $x '{a;a;[*]}<>->c' 'a & X(a & Fc)'
-     run 0 $x '{s[*]}<>->b' 'b M s'
-     run 0 $x '{s[+]}<>->b' 'b M s'
-     run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
-     run 0 $x '{1:a*}!' 'a'
-     run 0 $x '{(1;1):a*}!' 'Xa'
-     run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
-     run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
-     run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
-     run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \
-	      '{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))'
-     run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))'
-     run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})'
-     run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))'
-     run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))'
-     run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))'
-     run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
-     run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
-     run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
-     run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'
-     run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v'
-     run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v'
-     run 0 $x '{{b*&c*}[*3..5]}<>-> v' '{{b[+]|c[+]}[*0..5]} <>-> v'
+{a && b && c*} <>-> d, a&b&c&d
+{a && b && c[*1..3]} <>-> d, a&b&c&d
+{a && b && c[->0..2]} <>-> d, a&b&c&d
+{a && b && c[+]} <>-> d, a&b&c&d
+{a && b && c[=1]} <>-> d, a&b&c&d
+{a && b && d[=2]} <>-> d, 0
+{a && b && d[*2..]} <>-> d, 0
+{a && b && d[->2..4]} <>-> d, 0
+{a && { c* : b* : (g|h)*}} <>-> d, a & c & b & (g | h) & d
+{a && {b;c}} <>-> d, 0
+{a && {(b;c):e}} <>-> d, 0
+# until better
+{a && {b*;c*}} <>-> d, {a && {b*|c*}} <>-> d
+# until better
+{a && {(b*;c*):e}} <>-> d, {a && {b*|c*} && e} <>-> d
+{a && {b*;c}} <>-> d, a & c & d
+{a && {(b*;c):e}} <>-> d, a & c & d & e
+{a && {b;c*}} <>-> d, a & b & d
+{a && {(b;c*):e}} <>-> d, a & b & d & e
+{{{b1;r1*}&&{b2;r2*}};c}, b1&b2&X{{r1*&&r2*};c}
+{{b1:r1*}&&{b2:r2*}}, {{b1&&b2}:{r1*&&r2*}}
+{{r1*;b1}&&{r2*;b2}}, {{r1*&&r2*};{b1&&b2}}
+{{r1*:b1}&&{r2*:b2}}, {{r1*&&r2*}:{b1&&b2}}
+{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}, {{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}
+{{{b1;r1*}&{b2;r2*}};c}, b1&b2&X{{r1*&r2*};c}
+{{b1:(r1;x1*)}&{b2:(r2;x2*)}}, {{b1&&b2}:{{r1&&r2};{x1*&x2*}}}
+# Not reduced
+{{b1:r1*}&{b2:r2*}}, {{b1:r1*}&{b2:r2*}}
+# Not reduced
+{{r1*;b1}&{r2*;b2}}, {{r1*;b1}&{r2*;b2}}
+# Not reduced
+{{r1*:b1}&{r2*:b2}}, {{r1*:b1}&{r2*:b2}}
+{{a;b*;c}&{d;e*}&{f*;g}&{h*}}, {{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}
+{a;(b*;c*;([*0]+{d;e}))*}!, {a;{b|c|{d;e}}*}!
+{a&b&c*}|->!Xb, (X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))
+{[*]}[]->b, Gb
+{a;[*]}[]->b, Gb | !a
+{[*];a}[]->b, G(b | !a)
+{a;b;[*]}[]->c, !a | X(!b | Gc)
+{a;a;[*]}[]->c, !a | X(!a | Gc)
+{s[*]}[]->b, b W !s
+{s[+]}[]->b, b W !s
+{s[*2..]}[]->b, !s | X(b W !s)
+{a;b*;c;d*}[]->e, !a | X(!b R ((e & X(e W !d)) | !c))
+{a:b*:c:d*}[]->e, !a | ((!c | (e W !d)) W !b)
+{a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
+{{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
 
-     # not reduced
-     run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
-              '{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
-     run 0 $x '{((a*;b)+[*0])[*4..6]}!' '{((a*;b))[*0..6]}!'
-     run 0 $x '{c[*];e[*]}[]-> a' '{c[*];e[*]}[]-> a'
-     ;;
-  esac
+{a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
+{[*]}<>->b, Fb
+{a;[*]}<>->b, Fb & a
+{[*];a}<>->b, F(a & b)
+{a;b;[*]}<>->c, a & X(b & Fc)
+{a;a;[*]}<>->c, a & X(a & Fc)
+{s[*]}<>->b, b M s
+{s[+]}<>->b, b M s
+{s[*2..]}<>->b, s & X(b M s)
+{1:a*}!, a
+{(1;1):a*}!, Xa
+{a;b*;c;d*}<>->e, a & X(b U (c & (e | X(e M d))))
+{a:b*:c:d*}<>->e, a & ((c & (e M d)) M b)
+{a|b*|c|d*}<>->e, ((a | c) & e) | (e M b) | (e M d)
+{{[*0]|a};b;{[*0]|a};c;e[*]}<>->f, {{[*0]|a};b;{[*0]|a}}<>->X(c&(f|X(f M e)))
+{a;b[*];c[*];e;f*}, a & X(b W (c W e))
+{a;b*;(a* && (b;c));c*}, a & X(b W {a[*] && {b;c}})
+{a;a;b[*2..];b}, a & X(a & X(b & X(b & Xb)))
+!{a;a;b[*2..];b}, !a | X(!a | X(!b | X(!b | X!b)))
+!{a;b[*];c[*];e;f*}, !a | X(!b M (!c M !e))
+!{a;b*;(a* && (b;c));c*}, !a | X(!b M !{a[*] && {b;c}})
+{(a;c*;d)|(b;c)}, (a & X(c W d)) | (b & Xc)
+!{(a;c*;d)|(b;c)}, (X(!c M !d) | !a) & (X!c | !b)
+(Xc R b) & (Xc W 0), b & XGc
+{{c*|1}[*0..1]}<>-> v, {{c[+]|1}[*0..1]}<>-> v
+{{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*0..5]} <>-> v
+{{b*&c*}[*3..5]}<>-> v, {{b[+]|c[+]}[*0..5]} <>-> v
+# not reduced
+{a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}!
+{((a*;b)+[*0])[*4..6]}!, {((a*;b))[*0..6]}!
+{c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a
+EOF
 
-  run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
-
-  run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
-  run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
-
-  # Eventuality and universality class reductions
-  run 0 $x 'FFa' 'Fa'
-  run 0 $x 'FGFa' 'GFa'
-  run 0 $x 'b U Fa' 'Fa'
-  run 0 $x 'b U GFa' 'GFa'
-  run 0 $x 'Ga' 'Ga'
-
-  run 0 $x 'a U XXXFb' 'XXXFb'
-done
+run 0 ../reduccmp nottau.txt
+run 0 ../reductaustr common.txt
diff --git a/src/ltltest/uwrm.test b/src/ltltest/uwrm.test
index 4f8fe5e9a..c18e0dc32 100755
--- a/src/ltltest/uwrm.test
+++ b/src/ltltest/uwrm.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2012 Laboratoire de Recherche et Developpement
+# Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,52 +22,39 @@
 # These formulas comes from an appendix of tl/tl.tex
 
 . ./defs || exit 1
-
 set -e
 
-equiv()
-{
-  dst=$1
-  shift
-  for src in "$@"; do
-     ../reduccmp "$src" "$dst"
-  done
-}
-
+cat >input.txt<<EOF
 # Equivalences with U
-
-equiv Ff '1 U f'
-equiv Gf '!F!f' '!(1 U!f)'
-equiv 'f W g' '(f U g) | (G f)' '(f U g) | !(1 U ! f)' \
-              'f U (g | G f)' 'f U (g | !(1 U ! f ))'
-equiv 'f M g'  'g U (f & g)'
-equiv 'f R g'  'g W (f & g)'  '(g U (f & g)) | !(1 U ! g)' \
-               'g U ((f & g) | !(1 U ! g))'
+1 U f, Ff
+!F!f, !(1 U!f), Gf
+(f U g)|(G f), (f U g) | !(1 U ! f), f U (g | G f), f U (g | !(1 U !f)), f W g
+g U (f & g), f M g
+g W (f & g), (g U (f & g)) | !(1 U ! g), g U ((f & g) | !(1 U ! g)), f R g
 
 # Equivalences with W
-
-equiv Ff '!G!f' '!((! f) W 0)'
-equiv Gf  '0 R f'  'f W 0'
-equiv 'f U g'  '(f W g) & (F g)'  '(f W g) & !((! g) W 0)'
-equiv 'f M g'  '(g W (f & g)) & (F f)'  '(g W (f & g)) & !((!f) W 0)'
-equiv 'f R g'  'g W (f & g)'
+!G!f, !((! f) W 0), Ff
+0 R f, f W 0, Gf
+(f W g) & (F g), (f W g) & !((! g) W 0), f U g
+(g W (f & g)) & (F f), (g W (f & g)) & !((!f) W 0), f M g
+g W (f & g), f R g
 
 # Equivalences with R
+!G!f, !(0 R !f), Ff
+0 R f, Gf
+# (((X g) R f) & F g) | g, (((X g) R f ) & (!(0 R ! g))) | g, f U g
+((X g) R f) | g, g R (f | g), f W g
+(f R g) & F f, (f R g) & !(0 R !f), f R (g & F f), f R (g & !(0 R !f)), f M g
 
-equiv Ff '!G!f' '!(0 R !f)'
-equiv Gf '0 R f'
-#equiv 'f U g'  '(((X g) R f) & F g) | g' '(((X g) R f ) & (!(0 R ! g))) | g'
-equiv 'f W g'  '((X g) R f) | g' 'g R (f | g)'
-equiv 'f M g'  '( f R g) & F f'  '(f R g) & ! (0 R ! f)' \
-               'f R (g & F f)'  'f R (g & !(0 R !f))'
 # Equivalences with M
-
-equiv Ff 'f M 1'
-equiv Gf  '!F!f'  '!((!f) M 1)'
-equiv 'f U g'  '((X g) M f) | g' 'g M (f | g)'
-equiv 'f W g'  '(f U g) | G f'  '((X g) M f) | g | !((! f ) M 1)'
-equiv 'f R g'  '(f M g) | G g'  '(f M g) | !((! g) M 1)'
+f M 1, Ff
+!F!f, !((!f) M 1), Gf
+((X g) M f) | g, g M (f | g), f U g
+(f U g) | G f, ((X g) M f) | g | !((! f ) M 1), f W g
+(f M g) | G g, (f M g) | !((! g) M 1), f R g
 
 # Example from tl.tex
+#(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g, f U g
+EOF
 
-# equiv 'f U g' '(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g'
+run 0 ../reduccmp input.txt