Add a visitor to relabel the atomic proposition in formulas.

* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltlvisit/clone.cc (recurse): Don't call clone(), nobody
needs that.  Instead, really recurse.
* src/bin/ltlfilt.cc: Add a --relabel option.
* src/bin/genltl.cc: Relabel formulas if --lbt is used.
* src/sanity/style.test: Tweak detection of i++.

src/bin/genltl.cc

@@ -91,6 +91,7 @@
 #include <cstring>
 #include "ltlast/allnodes.hh"
 #include "ltlenv/defaultenv.hh"
+#include "ltlvisit/relabel.hh"
 
 using namespace spot;
 using namespace spot::ltl;
@@ -820,6 +821,15 @@ output_pattern(int pattern, int n)
       error(100, 0, "internal error: pattern not implemented");
     }
 
+  // Make sure we use only "p42"-style of atomic propositions
+  // in lbt's output.
+  if (output_format == lbt_output)
+    {
+      const spot::ltl::formula* r = spot::ltl::relabel(f, spot::ltl::Pnn);
+      f->destroy();
+      f = r;
+    }
+
   output_formula(f);
   f->destroy();
 }

src/bin/ltlfilt.cc

@@ -27,6 +27,7 @@
 #include <iostream>
 #include <fstream>
 #include <argp.h>
+#include <cstring>
 #include "progname.h"
 #include "error.h"
 
@@ -39,6 +40,7 @@
 #include "ltlparse/public.hh"
 #include "ltlvisit/simplify.hh"
 #include "ltlvisit/length.hh"
+#include "ltlvisit/relabel.hh"
 #include "ltlast/unop.hh"
 #include "ltlast/multop.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
@@ -87,6 +89,7 @@ Exit status:\n\
 #define OPT_IMPLY 24
 #define OPT_EQUIVALENT_TO 25
 #define OPT_LBT 26
+#define OPT_RELABEL 27
 
 static const argp_option options[] =
   {
@@ -95,7 +98,8 @@ static const argp_option options[] =
     { "formula", 'f', "STRING", 0, "process the formula STRING", 0 },
     { "file", 'F', "FILENAME", 0,
       "process each line of FILENAME as a formula", 0 },
-    { "lbt-input", OPT_LBT, 0, 0, "read all formulas using LBT's prefix syntax", 0 },
+    { "lbt-input", OPT_LBT, 0, 0,
+      "read all formulas using LBT's prefix syntax", 0 },
     { 0, 0, 0, 0, "Error handling:", 2 },
     { "skip-errors", OPT_SKIP_ERRORS, 0, 0,
       "output erroneous lines as-is without processing", 0 },
@@ -106,6 +110,9 @@ static const argp_option options[] =
     { 0, 0, 0, 0, "Transformation options:", 3 },
     { "negate", 'n', 0, 0, "negate each formula", 0 },
     { "nnf", OPT_NNF, 0, 0, "rewrite formulas in negative normal form", 0 },
+    { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL,
+      "relabel all atomic propositions, alphabetically unless " \
+      "specified otherwise", 0 },
     DECLARE_OPT_R,
     LEVEL_DOC(4),
     /**************************************************/
@@ -204,6 +211,8 @@ static int size_min = -1;
 static int size_max = -1;
 static int bsize_min = -1;
 static int bsize_max = -1;
+static bool relabeling = false;
+static spot::ltl::relabeling_style style = spot::ltl::Abc;
 
 static const spot::ltl::formula* implied_by = 0;
 static const spot::ltl::formula* imply = 0;
@@ -295,6 +304,15 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_PSL:
       psl = true;
       break;
+    case OPT_RELABEL:
+      relabeling = true;
+      if (!arg || !strncasecmp(arg, "abc", 6))
+	style = spot::ltl::Abc;
+      else if (!strncasecmp(arg, "pnn", 4))
+	style = spot::ltl::Pnn;
+      else
+	error(2, 0, "invalid argument for --relabel: '%s'", arg);
+      break;
     case OPT_SAFETY:
       safety = obligation = true;
       break;
@@ -415,6 +433,14 @@ namespace
 	  f = res;
 	}
 
+      if (relabeling)
+	{
+	  const spot::ltl::formula* res =
+	    spot::ltl::relabel(f, style);
+	  f->destroy();
+	  f = res;
+	}
+
       bool matched = true;
 
       matched &= !ltl || f->is_ltl_formula();

src/ltlvisit/Makefile.am

@@ -42,6 +42,7 @@ ltlvisit_HEADERS = \
   postfix.hh \
   randomltl.hh \
   reduce.hh \
+  relabel.hh \
   simpfg.hh \
   simplify.hh \
   snf.hh \
@@ -65,6 +66,7 @@ libltlvisit_la_SOURCES = \
   postfix.cc \
   randomltl.cc \
   reduce.cc \
+  relabel.cc \
   simpfg.cc \
   simplify.cc \
   snf.cc \

src/ltlvisit/clone.cc

@@ -70,8 +70,9 @@ namespace spot
     void
     clone_visitor::visit(const binop* bo)
     {
+      const formula* first = recurse(bo->first());
       result_ = binop::instance(bo->op(),
-				recurse(bo->first()), recurse(bo->second()));
+				first, recurse(bo->second()));
     }
 
     void
@@ -96,7 +97,8 @@ namespace spot
     const formula*
     clone_visitor::recurse(const formula* f)
     {
-      return f->clone();
+      f->accept(*this);
+      return result_;
     }
 
     const formula*

src/ltlvisit/relabel.cc

@@ -0,0 +1,118 @@
+// -*- coding: utf-8 -*-
+// 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 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.
+
+#include <relabel.hh>
+#include <sstream>
+#include "clone.hh"
+#include "misc/hash.hh"
+#include "ltlenv/defaultenv.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    namespace
+    {
+      class relabeler: public clone_visitor
+      {
+      public:
+	typedef Sgi::hash_map<const atomic_prop*, const formula*,
+			      ptr_hash<atomic_prop> > map;
+	map newname;
+
+	void
+	visit(const atomic_prop* ap)
+	{
+	  map::const_iterator it = newname.find(ap);
+	  if (it != newname.end())
+	    result_ = it->second->clone();
+	  else
+	    newname[ap] = result_ = next();
+	}
+
+	virtual const formula* next() = 0;
+      };
+
+      class relabeler_pnn: public relabeler
+      {
+      public:
+	relabeler_pnn()
+	  : nn(0)
+	{
+	}
+
+	unsigned nn;
+
+	const formula* next()
+	{
+	  std::ostringstream s;
+	  s << "p" << nn++;
+	  return default_environment::instance().require(s.str());
+	}
+      };
+
+      class relabeler_abc: public relabeler
+      {
+      public:
+	relabeler_abc()
+	  : nn(0)
+	{
+	}
+
+	unsigned nn;
+
+	const formula* next()
+	{
+	  std::string s;
+	  unsigned n = nn++;
+	  do
+	    {
+	      s.push_back('a' + (n % 26));
+	      n /= 26;
+	    }
+	  while (n);
+
+	  return default_environment::instance().require(s);
+	}
+      };
+    }
+
+
+    const formula*
+    relabel(const formula* f, relabeling_style style)
+    {
+      relabeler* rel = 0;
+      switch (style)
+	{
+	case Pnn:
+	  rel = new relabeler_pnn;
+	  break;
+	case Abc:
+	  rel = new relabeler_abc;
+	  break;
+	}
+      f->accept(*rel);
+      const formula* res = rel->result();
+      delete rel;
+      return res;
+    }
+  }
+}

src/ltlvisit/relabel.hh

@@ -0,0 +1,42 @@
+// -*- coding: utf-8 -*-
+// 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 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.
+
+#ifndef SPOT_LTLVISIT_RELABEL_HH
+# define SPOT_LTLVISIT_RELABEL_HH
+
+#include <ltlast/formula.hh>
+
+namespace spot
+{
+  namespace ltl
+  {
+    enum relabeling_style { Abc, Pnn };
+
+    /// \brief Relabel the atomic proposition in a formula.
+    ///
+    /// \ingroup ltl_rewriting
+    const formula* relabel(const formula* f, relabeling_style style);
+  }
+}
+
+
+
+#endif // SPOT_LTLVISIT_RELABEL_HH

src/sanity/style.test

@@ -168,7 +168,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
       egrep '(->|[.])size\(\) [=!]= 0|![a-zA-Z0-9_]*(->|[.])size\(\)|(if |while |assert)\([a-zA-Z0-9_]*(->|[.])size\(\)\)' $tmp &&
 	diag 'Prefer empty() to check emptiness.'
 
-      egrep '^[^=*]*([+][+]|--);' $tmp &&
+      egrep '^[^=*<]*([+][+]|--);' $tmp &&
 	diag 'Take good habits: use ++i instead of i++ when you have the choice.'
 
       grep '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp &&