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

relabel_bse: fix incorrect detection of common APs

Browse source 
Based on a report by Jean Kreber.

* spot/tl/relabel.cc (cut_points): Really connect children of Boolean
operators using undirected edges, not directed ones.
* tests/core/ltlrel.test: Add test cases.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-11 23:50:07 +02:00
parent 0b25820211
commit 33289f5166
3 changed files with 35 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -122,6 +122,9 @@ New in spot 2.8.7.dev (not yet released)
- Emptiness checks, and scc_info should now ignore edges labeled
with false.
- relabel_bse() could incorrectly relabel Boolean subformulas that
had some atomic propositions in common.
New in spot 2.8.7 (2020-03-13)
Bugs fixed:

21
spot/tl/relabel.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et
// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -194,15 +194,15 @@ namespace spot
// ╱ ╲ ╱ ╲
// a─────b c─────d
//
// (The root node is also a cut-point, but we only consider Boolean
// cut-points for relabeling.)
// (The root node is also a cut point, but we only consider Boolean
// cut points for relabeling.)
//
// On the other hand, (a & b) U (b & !c) has only one Boolean
// cut-point which corresponds to the NOT operator:
//
// (a&b)U(b&!c)
// ╱ ╲
// a&b b&c
// a&b b&!c
// ╱ ╲ ╱ ╲
// a─────b────!c
// │
@ -222,7 +222,7 @@ namespace spot
// replace that node by a fresh atomic proposition.
//
// In the example above (a&b)U(b&!c), the last recursion
// stop a, b, and !c, producing (p0&p1)U(p1&p2).
// stops on a, b, and !c, producing (p0&p1)U(p1&p2).
namespace
{
typedef std::vector<formula> succ_vec;
@ -282,20 +282,23 @@ namespace spot
if (sz > 1 && f.is_boolean())
{
// For Boolean nodes, connect all children in a
// loop. This way the node can only be a cut-point
// loop. This way the node can only be a cut point
// if it separates all children from the reset of
// the graph (not only one).
formula pred = f[0];
for (i = 1; i < sz; ++i)
{
formula next = f[i];
// Note that we only add an edge in one
// direction, because we are building a cycle
// between all children anyway.
// Note that we only add an edge in both directions,
// as the cut point algorithm really need undirected
// graphs. (We used to do only one direction, and
// that turned out to be a bug.)
g[pred].emplace_back(next);
g[next].emplace_back(pred);
pred = next;
}
g[pred].emplace_back(f[0]);
g[f[0]].emplace_back(pred);
}
s.pop();
}

21
tests/core/ltlrel.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2016 Laboratoire de Recherche et Développement
# Copyright (C) 2013, 2016, 2020 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -89,3 +89,22 @@ Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & p3 & X((!p0 & p3) U p4)))) U p0)
p3 -> !p5
p4 -> p4
EOF
# The next two formulas come from a report by Jens Kreber.
t <<EOF
!b & e U (a & b & c)
!p0 & (p1 U (p0 & p2 & p3))
p0 -> b
p1 -> e
p2 -> a
p3 -> c
EOF
t <<EOF
X!c & X(b & c & d & a U e)
X!p0 & X(p0 & p1 & p2 & (p3 U p4))
p0 -> c
p1 -> b
p2 -> d
p3 -> a
p4 -> e
EOF