diff --git a/NEWS b/NEWS index 5690e4eae..5884c2869 100644 --- a/NEWS +++ b/NEWS @@ -59,6 +59,9 @@ New in spot 2.7.4.dev (not yet released) {a:{[*i..j];b}}. The formula::sugar_delay() function implement this SVA operator in terms of the existing PSL operators. + - spot::relabel_apply() make it easier to reverse the effect + of spot::relabel() or spot::relabel_bse() on formula. + New in spot 2.7.4 (2019-04-27) Bugs fixed: diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc index 383f559c1..b594e4f1e 100644 --- a/spot/tl/relabel.cc +++ b/spot/tl/relabel.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -482,4 +482,17 @@ namespace spot bse_relabeler rel(gen, c, m); return rel.visit(f); } + + formula + relabel_apply(formula f, relabeling_map* m) + { + if (f.is(op::ap)) + { + auto i = m->find(f); + if (i != m->end()) + return i->second; + } + return f.map(relabel_apply, m); + } + } diff --git a/spot/tl/relabel.hh b/spot/tl/relabel.hh index ffbcce7ef..384d1d43f 100644 --- a/spot/tl/relabel.hh +++ b/spot/tl/relabel.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2015, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -48,4 +48,13 @@ namespace spot SPOT_API formula relabel_bse(formula f, relabeling_style style, relabeling_map* m = nullptr); + + /// \ingroup tl_rewriting + /// \brief Replace atomic propositions of \a f by subformulas + /// specified in \a m. + /// + /// Atomic proposition that do not appear in \a m are not + /// replaced. + SPOT_API + formula relabel_apply(formula f, relabeling_map* m); } diff --git a/tests/python/relabel.py b/tests/python/relabel.py index 9d983eabd..344581ca1 100644 --- a/tests/python/relabel.py +++ b/tests/python/relabel.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -31,6 +31,8 @@ assert(res == """#define p0 a & b #define p1 c GFp0 -> (FGp0 & Gp1)""") +h = spot.relabel_apply(g, m) +assert h == f autg = g.translate() spot.relabel_here(autg, m)