alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: implement relabel_apply()

Browse source 
* spot/tl/relabel.hh, spot/tl/relabel.cc: Here.
* NEWS: Mention it.
* tests/python/relabel.py: Use it.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-18 09:33:30 +02:00
parent e325289a12
commit 066133b829
4 changed files with 30 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -59,6 +59,9 @@ New in spot 2.7.4.dev (not yet released)
{a:{[*i..j];b}}. The formula::sugar_delay() function implement {a:{[*i..j];b}}. The formula::sugar_delay() function implement
this SVA operator in terms of the existing PSL operators. 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) New in spot 2.7.4 (2019-04-27)
Bugs fixed: Bugs fixed:

15
spot/tl/relabel.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -482,4 +482,17 @@ namespace spot
bse_relabeler rel(gen, c, m); bse_relabeler rel(gen, c, m);
return rel.visit(f); 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);
}
} }

11
spot/tl/relabel.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -48,4 +48,13 @@ namespace spot
SPOT_API SPOT_API
formula relabel_bse(formula f, relabeling_style style, formula relabel_bse(formula f, relabeling_style style,
relabeling_map* m = nullptr); 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);
} }

4
tests/python/relabel.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*- # -*- 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 # de l'Epita
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -31,6 +31,8 @@ assert(res == """#define p0 a & b
#define p1 c #define p1 c
GFp0 -> (FGp0 & Gp1)""") GFp0 -> (FGp0 & Gp1)""")
h = spot.relabel_apply(g, m)
assert h == f
autg = g.translate() autg = g.translate()
spot.relabel_here(autg, m) spot.relabel_here(autg, m)