From ce51ed3002bc29ac7db4cb4de8c9418e3771c9ab Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 15 Apr 2010 19:05:03 +0200
Subject: [PATCH] Reorder recent additions to reduccmp.test.

* src/ltltest/reduccmp.test: Reorder the test added by the
previous patches.  Some are not supposed to be reduced by
reductaustr.
---
 ChangeLog                 |  8 ++++++++
 src/ltltest/reduccmp.test | 37 ++++++++++++++++++++-----------------
 2 files changed, 28 insertions(+), 17 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 0a9fb1d5b..a1152bf28 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2010-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Reorder recent additions to reduccmp.test.
+
+	* src/ltltest/reduccmp.test: Reorder the test added by the
+	previous patches.  Some are not supposed to be reduced by
+	reductaustr.
+
 2010-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix a long-standing bug in the stronger rule for R and its recent
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index fb3ecac97..0f4415e14 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -66,24 +66,25 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'a | (b U a) | a' '(b U a)'
   run 0 $x 'a U (b U a)' '(b U a)'
 
-  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'
-
   # Basics reduction
   run 0 $x 'X(true)' 'true'
   run 0 $x 'X(false)' 'false'
   run 0 $x 'F(true)' 'true'
   run 0 $x 'F(false)' 'false'
-  run 0 $x 'G(true)' 'true'
-  run 0 $x 'G(false)' 'false'
 
   run 0 $x 'XGF(f)' 'GF(f)'
 
   case $x in
    *tau*);;
    *)
+     run 0 $x 'G(true)' 'true'
+     run 0 $x 'G(false)' 'false'
+
+     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'
+
      run 0 $x 'G(a R b)' 'G(b)'
 
      run 0 $x 'FX(a)' 'XF(a)'
@@ -140,18 +141,23 @@ for x in ../reduccmp ../reductaustr; do
      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'
+
+     run 0 $x 'GFGa' 'FGa'
+     run 0 $x 'b R Ga' 'Ga'
+     run 0 $x 'b R FGa' 'FGa'
+
+     # 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'
      ;;
   esac
 
   run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
 
-  # 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'
   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.
 
@@ -161,7 +167,4 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'b U Fa' 'Fa'
   run 0 $x 'b U GFa' 'GFa'
   run 0 $x 'Ga' 'Ga'
-  run 0 $x 'GFGa' 'FGa'
-  run 0 $x 'b R Ga' 'Ga'
-  run 0 $x 'b R FGa' 'FGa'
 done