Fix handling of PSL operators in reductions rules.

We still don't have any PSL-specific reductions, but at least
the LTL reduction now appear to work on PSL formulas.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Fix the
call to std::copy to handle Concat, Fusion, and AndNLM.
* src/ltlvisit/reduce.cc (reduce_visitor): Fix handling
of UConcat, EConcat, and EConcatMarked.
* src/tgbatest/randpsl.test: Activate reductions.
* src/ltltest/reducpsl.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.

src/ltltest/Makefile.am

@@ -94,6 +94,7 @@ TESTS = \
   kind.test \
   syntimpl.test \
   reduc.test \
+  reducpsl.test \
   reduccmp.test
 
 distclean-local:

src/ltltest/reducpsl.test

@@ -0,0 +1,42 @@
+#! /bin/sh
+# Copyright (C) 2011 Laboratoire de Recherche et Développement 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 for the reduc visitor.
+. ./defs || exit 1
+
+set -e
+
+FILE=formulae
+: > $FILE
+for i in 10 12 14 16 18 20; do
+  run 0 ../randltl -P -u -s 0   -f $i a b c -F 100 >> $FILE
+  run 0 ../randltl -P -u -s 100 -f $i a b c d e f -F 100 >> $FILE
+done
+
+for opt in 0 1 2 3 7; do
+  run 0 ../reduc -f -h $opt "$FILE"
+done
+# Running the above through valgrind is quite slow already.
+# Don't use valgrind for the next reductions (even slower).
+for opt in 8 9; do
+  ../reduc -f -h $opt "$FILE"
+done

src/ltlvisit/basicreduce.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
+// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2007 Laboratoire d'Informatique de
 // Paris 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC),
@@ -25,6 +25,7 @@
 #include "ltlast/visitor.hh"
 #include "ltlast/allnodes.hh"
 #include <cassert>
+#include <iterator>
 
 namespace spot
 {
@@ -181,13 +182,13 @@ namespace spot
 		}
 
 #if 0
-	      // F(f1 & GF(f2)) = F(f1) & GF(F2)
+	      // F(f1 & GF(f2)) = F(f1) & GF(f2)
 	      //
 	      // As is, these two formulae are translated into
 	      // equivalent Büchi automata so the rewriting is
 	      // useless.
 	      //
-	      // However when taken in a larger formulae such as F(f1
+	      // However when taken in a larger formula such as F(f1
 	      // & GF(f2)) | F(a & GF(b)), this rewriting used to
 	      // produce (F(f1) & GF(f2)) | (F(a) & GF(b)), missing
 	      // the opportunity to apply the F(E1)|F(E2) = F(E1|E2)
@@ -862,7 +863,8 @@ namespace spot
 	    case multop::Concat:
 	    case multop::AndNLM:
 	    case multop::Fusion:
-	      std::copy(res->begin(), res->end(), tmpOther->end());
+	      std::copy(res->begin(), res->end(),
+			std::back_inserter(*tmpOther));
 	      break;
 	    }
 

src/ltlvisit/reduce.cc

@@ -157,10 +157,12 @@ namespace spot
 		case binop::Xor:
 		case binop::Equiv:
 		case binop::Implies:
+		  assert(!"operator not supported for syntactic implication");
+		  return;
 		case binop::UConcat:
 		case binop::EConcat:
 		case binop::EConcatMarked:
-		  return;
+		  break;
 
 		case binop::U:
 		  /* a < b => a U b = b */

src/tgbatest/randpsl.test

@@ -34,7 +34,7 @@ check_psl()
   run 0 ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)"
 }
 
-../../ltltest/randltl -F 50 -f 30 -u -s 0 -P a b c |
+../../ltltest/randltl -F 50 -f 30 -r 12 -u -s 0 -P a b c |
 while read formula; do
   check_psl "$formula"
 done