diff --git a/NEWS b/NEWS index 99b1f1f40..af455e012 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,10 @@ New in spot 2.11.6.dev (not yet released) autfilt input.hoa -o output-%l.hoa + - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that + will replace boolean subformulas by fresh atomic propositions even + if those subformulas share atomic propositions. + Library: - The following new trivial simplifications have been implemented for SEREs: @@ -29,6 +33,10 @@ New in spot 2.11.6.dev (not yet released) - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula() that converts a BDD into a CNF instead of a DNF. + - spot::relabel_overlapping_bse() is a new function that will + replace boolean subformulas by fresh atomic propositions even if + those subformulas share atomic propositions. + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index ed2f2d08d..5ed7a2fe1 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -94,6 +94,7 @@ enum { OPT_REJECT_WORD, OPT_RELABEL, OPT_RELABEL_BOOL, + OPT_RELABEL_OVERLAP, OPT_REMOVE_WM, OPT_REMOVE_X, OPT_SAFETY, @@ -139,8 +140,12 @@ static const argp_option options[] = "relabel all atomic propositions, alphabetically unless " \ "specified otherwise", 0 }, { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL, - "relabel Boolean subexpressions, alphabetically unless " \ - "specified otherwise", 0 }, + "relabel Boolean subexpressions that do not share atomic propositions," + " relabel alphabetically unless specified otherwise", 0 }, + { "relabel-overlapping-bool", OPT_RELABEL_OVERLAP, "abc|pnn", + OPTION_ARG_OPTIONAL, + "relabel Boolean subexpressions even if they share atomic propositions," + " relabel alphabetically unless specified otherwise", 0 }, { "define", OPT_DEFINE, "FILENAME", OPTION_ARG_OPTIONAL, "when used with --relabel or --relabel-bool, output the relabeling map " "using #define statements", 0 }, @@ -316,7 +321,10 @@ static bool recurrence = false; static bool persistence = false; static range size = { -1, -1 }; static range bsize = { -1, -1 }; -enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling }; +enum relabeling_mode { NoRelabeling = 0, + ApRelabeling, + BseRelabeling, + OverlappingRelabeling }; static relabeling_mode relabeling = NoRelabeling; static spot::relabeling_style style = spot::Abc; static bool remove_x = false; @@ -358,6 +366,19 @@ parse_formula_arg(const std::string& input) return pf.f; } +static void +parse_relabeling_style(const char* arg, const char* optname) +{ + if (!arg || !strncasecmp(arg, "abc", 6)) + style = spot::Abc; + else if (!strncasecmp(arg, "pnn", 4)) + style = spot::Pnn; + else + error(2, 0, "invalid argument for --relabel%s: '%s'\n" + "expecting 'abc' or 'pnn'", optname, arg); +} + + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -500,16 +521,16 @@ parse_opt(int key, char* arg, struct argp_state*) } break; case OPT_RELABEL: + relabeling = ApRelabeling; + parse_relabeling_style(arg, ""); + break; case OPT_RELABEL_BOOL: - relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling); - if (!arg || !strncasecmp(arg, "abc", 6)) - style = spot::Abc; - else if (!strncasecmp(arg, "pnn", 4)) - style = spot::Pnn; - else - error(2, 0, "invalid argument for --relabel%s: '%s'", - (key == OPT_RELABEL_BOOL ? "-bool" : ""), - arg); + relabeling = BseRelabeling; + parse_relabeling_style(arg, "-bool"); + break; + case OPT_RELABEL_OVERLAP: + relabeling = OverlappingRelabeling; + parse_relabeling_style(arg, "-overlapping-bool"); break; case OPT_REMOVE_WM: unabbreviate += "MW"; @@ -701,6 +722,12 @@ namespace f = spot::relabel_bse(f, style, &relmap); break; } + case OverlappingRelabeling: + { + relmap.clear(); + f = spot::relabel_overlapping_bse(f, style, &relmap); + break; + } case NoRelabeling: break; } diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc index 26c7564c1..f57c0c919 100644 --- a/spot/tl/relabel.cc +++ b/spot/tl/relabel.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2020, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -80,7 +80,9 @@ namespace spot } }; - + // if subexp == false, matches APs + // if subexp == true, matches boolean subexps + template class relabeler { public: @@ -101,54 +103,89 @@ namespace spot formula rename(formula old) { + if constexpr (subexp) + { + // have we given a name to the negation of this formula? + auto neg = newname.find(formula::Not(old)); + if (neg != newname.end()) + return formula::Not(neg->second); + } + auto r = newname.emplace(old, nullptr); if (!r.second) - { - return r.first->second; - } - else - { - formula res = gen->next(); - r.first->second = res; - if (oldnames) - (*oldnames)[res] = old; - return res; - } + return r.first->second; + + formula res = gen->next(); + r.first->second = res; + if (oldnames) + (*oldnames)[res] = old; + return res; } formula visit(formula f) { - if (f.is(op::ap)) - return rename(f); + if ((!subexp && f.is(op::ap)) + || (subexp && f.is_boolean())) + { + return rename(f); + } + if (subexp && f.is(op::Or, op::And) && f[0].is_boolean()) + { + // Boolean terms are always beginning of And and Or, so + // the above test capture Or/And that some Boolean arguments + // and some non-Boolean arguments. + unsigned i = 0; + formula b = f.boolean_operands(&i); + unsigned sz = f.size(); + std::vector res; + res.reserve(sz - i + 1); + res.emplace_back(visit(b)); + for (; i < sz; ++i) + res.emplace_back(visit(f[i])); + return formula::multop(f.kind(), res); + } else - return f.map([this](formula f) - { - return this->visit(f); - }); + { + return f.map([this](formula f) + { + return this->visit(f); + }); + } } }; - } + template + formula + relabel_do(formula f, relabeling_style style, relabeling_map* m) + { + ap_generator* gen = nullptr; + switch (style) + { + case Pnn: + gen = new pnn_generator; + break; + case Abc: + gen = new abc_generator; + break; + } + relabeler r(gen, m); + return r.visit(f); + } + } formula relabel(formula f, relabeling_style style, relabeling_map* m) { - ap_generator* gen = nullptr; - switch (style) - { - case Pnn: - gen = new pnn_generator; - break; - case Abc: - gen = new abc_generator; - break; - } + return relabel_do(f, style, m); + } - relabeler r(gen, m); - return r.visit(f); + formula + relabel_overlapping_bse(formula f, relabeling_style style, relabeling_map* m) + { + return relabel_do(f, style, m); } namespace @@ -502,7 +539,7 @@ namespace spot } - class bse_relabeler final: public relabeler + class bse_relabeler final: public relabeler { public: const fset& c; diff --git a/spot/tl/relabel.hh b/spot/tl/relabel.hh index 384d1d43f..59efdf94b 100644 --- a/spot/tl/relabel.hh +++ b/spot/tl/relabel.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015, 2019 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2015, 2019, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -34,6 +34,9 @@ namespace spot /// /// If \a m is non-null, it is filled with correspondence /// between the new names (keys) and the old names (values). + /// + /// \see relabel_bse + /// \see relabel_overlaping_bse SPOT_API formula relabel(formula f, relabeling_style style, relabeling_map* m = nullptr); @@ -45,9 +48,27 @@ namespace spot /// /// If \a m is non-null, it is filled with correspondence /// between the new names (keys) and the old names (values). + /// + /// The relabel_overlapping_bse() will introduce a new atomic + /// proposition for each maximal Boolean subexpression encountered, + /// even if they overlap (i.e., share common atomic + /// propositions). For instance `(a & b & c) U (c & d & e)` will be + /// simply be relabeled as `p0 U p1`. This kind of renaming to not + /// preserves the + /// + /// The relabel_bse() version will make sure that the replaced + /// subexpressions do not share atomic propositions. For instance + /// `(a & b & c) U (c & d & e)` will be simply be relabeled as + /// `(p0 & p1) U (p1 & p2)`, were `p1` replaces `c` and the rest + /// is obvious. + /// + /// @{ SPOT_API formula relabel_bse(formula f, relabeling_style style, relabeling_map* m = nullptr); + SPOT_API formula + relabel_overlapping_bse(formula f, relabeling_style style, relabeling_map* m); + // @} /// \ingroup tl_rewriting /// \brief Replace atomic propositions of \a f by subformulas diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 43d50ce06..192a60fef 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2020, 2022 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2013-2020, 2022, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -361,6 +361,8 @@ G(d & e) | FG(Xf| !c) | h | i b & !Xc & e & (f | g) b & GF(a | c) & !GF!(a | c) F(a <-> b) -> (c xor d) +(a & b & c) U (c & d & e) +(a & b & c) U !(a & b & c) EOF cat >exp <out @@ -393,6 +397,14 @@ p0 || []p1 || <>[](p2 || Xp3) #define p0 ((c && !d) || (!c && d)) #define p1 ((a && !b) || (!a && b)) p0 || []p1 +#define p0 (a && b) +#define p1 (c) +#define p2 (d && e) +(p0 && p1) U (p1 && p2) +#define p0 (a) +#define p1 (b) +#define p2 (c) +(p0 && p1 && p2) U (!p0 || !p1 || !p2) EOF run 0 ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out @@ -433,11 +445,53 @@ p0 && []<>(p1 || p2) && ![]<>!(p1 || p2) #define p2 (c) #define p3 (d) <>(p0 <-> p1) -> !(p2 <-> p3) +#define p0 (a) +#define p1 (b) +#define p2 (c) +#define p3 (d) +#define p4 (e) +(p0 && p1 && p2) U (p2 && p3 && p4) +#define p0 (a) +#define p1 (b) +#define p2 (c) +(p0 && p1 && p2) U !(p0 && p1 && p2) EOF run 0 ltlfilt -s -u --relabel=pnn --define in >out diff exp out +cat >exp < b) +#define p1 (c xor d) +Fp0 -> p1 +#define p0 (a & b & c) +#define p1 (c & d & e) +p0 U p1 +#define p0 (a & b & c) +p0 U !p0 +EOF + +run 0 ltlfilt -u --relabel-over=pnn --define in >out +diff exp out + + toolong='((p2=0) * (p3=1))' # work around the 80-col check cat >exp <exp <out diff exp out @@ -484,6 +548,8 @@ h | i | G(d & e) | FG(!c | Xf)@ b & e & (f | g) & !Xc@ b & GF(a | c) & !GF!(a | c)@ F(a <-> b) -> (c xor d)@ +(a & b & c) U (c & d & e)@ +(a & b & c) U !(a & b & c)@ EOF diff exp out