Commit dc5237c7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

relabel: fix infinite recursion in relabel_bse()

Reported by František Blahoudek.

* spot/tl/relabel.cc: Fix.
* tests/core/ltlrel.test: Add test case.
* NEWS: Mention the bug.
parent 1c8c8691
......@@ -4,6 +4,7 @@ New in spot 2.0.1a (not yet released)
* Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1
headers.
* Fix an infinite recursion in relabel_bse().
New in spot 2.0.1 (2016-05-09)
......
......@@ -433,13 +433,14 @@ namespace spot
/// it as ((a & b) & Xc) in the graph to isolate the
/// Boolean operands as a single node.
formula b = f.boolean_operands(&i);
if (b)
if (b && b != f)
{
res.reserve(sz - i + 1);
res.push_back(visit(b));
}
else
{
i = 0;
res.reserve(sz);
}
for (; i < sz; ++i)
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement to
# Copyright (C) 2013, 2016 Laboratoire de Recherche et Dévelopement to
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -77,3 +77,15 @@ t <<EOF
p1 -> b
p2 -> c
EOF
# This one used to stack overflow due to an infinite recursion
# in the relabeling function. Reported by František Blahoudek.
t <<EOF
<>p1 -> ((p0 -> (!p1 U (!p1 && p3 && !p5 && X((!p1 && !p5) U p4)))) U p1)
Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & p3 & X((!p0 & p3) U p4)))) U p0)
p0 -> p1
p1 -> p0
p2 -> p3
p3 -> !p5
p4 -> p4
EOF
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment