diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index e11099ed3..3e6cd4577 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -91,6 +91,7 @@ #include #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(); } diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 1aaf371f5..caafa5c78 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -27,6 +27,7 @@ #include #include #include +#include #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(); diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 42ccadb8a..7b20b2978 100644 --- a/src/ltlvisit/Makefile.am +++ b/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 \ diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index c2baf29cc..2170b7b3d 100644 --- a/src/ltlvisit/clone.cc +++ b/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* diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc new file mode 100644 index 000000000..ecda0d537 --- /dev/null +++ b/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 +#include +#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 > 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; + } + } +} diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh new file mode 100644 index 000000000..4fe90ea71 --- /dev/null +++ b/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 + +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 diff --git a/src/sanity/style.test b/src/sanity/style.test index 31deae76e..88f22dc3e 100755 --- a/src/sanity/style.test +++ b/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 &&