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

relabel: fix handling of concat and fusion

Browse source 
* spot/tl/relabel.cc (formula_to_fgraph): Do not assume that n-ary
operators are Boolean operators.
* tests/python/relabel.py: Add a test case found while discussing
some expression with Antoine Martin.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-13 11:34:38 +02:00
parent 666d78d499
commit 179672fe3b
3 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -3,6 +3,9 @@ New in spot 2.11.1.dev (not yet released)
Bugs fixed: Bugs fixed:
- Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520) - Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520)
- spot::relabel_bse() was incorrectly relabeling some dependent
Boolean subexpressions in SERE. (Note that this had no
consequence on automata translated from those SERE.)
New in spot 2.11.1 (2022-10-10) New in spot 2.11.1 (2022-10-10)

14
spot/tl/relabel.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et // Copyright (C) 2012-2016, 2018-2020, 2022 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.
@ -363,7 +363,7 @@ namespace spot
goto done; goto done;
} }
} }
if (sz > 2 && !f.is_boolean()) if (sz > 2 && !f.is_boolean() && f.is(op::And, op::Or))
{ {
/// If we have a formula like (a & b & Xc), consider /// If we have a formula like (a & b & Xc), consider
/// it as ((a & b) & Xc) in the graph to isolate the /// it as ((a & b) & Xc) in the graph to isolate the
@ -384,7 +384,7 @@ namespace spot
for (i = 1; i < sz; ++i) for (i = 1; i < sz; ++i)
{ {
formula next = f[i]; formula next = f[i];
// Note that we only add an edge in both directions, // Note that we add an edge in both directions,
// as the cut point algorithm really need undirected // as the cut point algorithm really need undirected
// graphs. (We used to do only one direction, and // graphs. (We used to do only one direction, and
// that turned out to be a bug.) // that turned out to be a bug.)
@ -581,6 +581,14 @@ namespace spot
conv.visit(f); conv.visit(f);
} }
//// Uncomment to print the graph.
// for (auto& [f, sv]: g)
// {
// std::cerr << f << ":\n";
// for (auto& s: sv)
// std::cerr << " " << s << '\n';
// }
// Compute its cut-points // Compute its cut-points
fset c; fset c;
cut_points(g, c, f); cut_points(g, c, f);

4
tests/python/relabel.py
View file

@ -55,3 +55,7 @@ try:
spot.relabel_here(autg, m) spot.relabel_here(autg, m)
except RuntimeError as e: except RuntimeError as e:
tc.assertIn("old labels", str(e)) tc.assertIn("old labels", str(e))
f = spot.parse_infix_sere("(p9;p21|p22):(p1&p2;p11&p22;p1&p2)").f
g = spot.relabel_bse(f, spot.Abc)
tc.assertEqual(str(g), "(a;(b | c)):(d;(c & e);d)")