From fb6a2a50b5b61e476d205ed1448c3bc29d553c35 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 30 Apr 2012 18:03:33 +0200
Subject: [PATCH] One more test for U,W,R,M rewritins.

* src/ltltest/uwrm.test: New file.
* src/ltltest/Makefile.am: Add it.
---
 src/ltltest/Makefile.am |  3 +-
 src/ltltest/uwrm.test   | 75 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100755 src/ltltest/uwrm.test

diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index b1b174665..031a47c6f 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -96,7 +96,8 @@ TESTS = \
   syntimpl.test \
   reduc.test \
   reducpsl.test \
-  reduccmp.test
+  reduccmp.test \
+  uwrm.test
 
 distclean-local:
 	rm -rf $(TESTS:.test=.dir)
diff --git a/src/ltltest/uwrm.test b/src/ltltest/uwrm.test
new file mode 100755
index 000000000..6479a7137
--- /dev/null
+++ b/src/ltltest/uwrm.test
@@ -0,0 +1,75 @@
+#! /bin/sh
+# Copyright (C) 2012 Laboratoire de Recherche et Developpement
+# de l'Epita (LRDE).
+#
+# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+# Check LTL reductions for U, W, M and R.
+# 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
+}
+
+# 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))'
+
+# 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)'
+
+# Equivalences with R
+
+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)'
+
+# Example from tl.tex
+
+# equiv 'f U g' '(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g'