unabbreviate_wm: fix a segfault.

* src/ltlvisit/wmunabbrev.cc: Fix clone() order.
* src/ltltest/equals.cc: Add a mode for unabbreviate_wm().
* src/ltltest/unabbrevwm.test: New file.
* src/ltltest/Makefile.am: Add it.

src/ltltest/Makefile.am

@@ -41,7 +41,8 @@ check_PROGRAMS = \
   syntimpl \
   tostring \
   tunabbrev \
-  tunenoform
+  tunenoform \
+  unabbrevwm
 
 consterm_SOURCES = consterm.cc
 equals_SOURCES = equals.cc
@@ -67,6 +68,8 @@ tunabbrev_SOURCES = equals.cc
 tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
 tunenoform_SOURCES = equals.cc
 tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
+unabbrevwm_SOURCES = equals.cc
+unabbrevwm_CPPFLAGS = $(AM_CPPFLAGS) -DWM
 
 
 EXTRA_DIST = $(TESTS)
@@ -83,6 +86,7 @@ TESTS = \
   tunabbrev.test \
   nenoform.test \
   tunenoform.test \
+  unabbrevwm.test \
   consterm.test \
   kind.test \
   lenient.test \

src/ltltest/equals.cc

@@ -28,6 +28,7 @@
 #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"
@@ -70,7 +71,7 @@ main(int argc, char** argv)
   int exit_code;
 
   {
-#if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM)
+#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
     const spot::ltl::formula* tmp;
 #endif
 #ifdef LUNABBREV
@@ -87,6 +88,13 @@ main(int argc, char** argv)
     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);

src/ltltest/unabbrevwm.test

@@ -0,0 +1,30 @@
+#! /bin/sh
+# Copyright (C) 2012 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 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/>.
+
+
+# Check for the unabbreviate_logic visitor
+
+. ./defs || exit 1
+
+set -e
+
+# This caused a segfault at some point
+run 0 ../unabbrevwm \
+  '(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))' \
+  '(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))'

src/ltlvisit/wmunabbrev.cc

@@ -62,14 +62,16 @@ namespace spot
 	    case binop::W:
 	      // f1 W f2 = f2 R (f2 | f1)
 	      result_ =
-		binop::instance(binop::R, f2->clone(),
+		binop::instance(binop::R, f2,
-				multop::instance(multop::Or, f2, f1));
+				multop::instance(multop::Or,
+						 f2->clone(), f1));
 	      break;
 	    case binop::M:
 	      // f1 M f2 = f2 U (g2 & f1)
 	      result_ =
-		binop::instance(binop::U, f2->clone(),
+		binop::instance(binop::U, f2,
-				multop::instance(multop::And, f2, f1));
+				multop::instance(multop::And,
+						 f2->clone(), f1));
 	      break;
 	    }
 	}