Commit 028b56d5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

twa_run: better protection against empty cycles

Fixes #337.

* spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh: Here.
* tests/python/except.py: Test it.
* NEWS: Mention the issue.
parent 1c26764b
Pipeline #1009 passed with stages
in 132 minutes and 40 seconds
......@@ -34,6 +34,9 @@ New in spot 2.5.1.dev (not yet released)
- "autfilt --acceptance-is=Fin-less" no longer accept automata
with "f" acceptance.
- twa_run methods will now diagnose cases where the cycle is
unexpectedly empty instead of segfaulting.
New in spot 2.5.1 (2018-02-20)
Library:
......
......@@ -283,6 +283,13 @@ namespace spot
return os;
}
void twa_run::ensure_non_empty_cycle(const char* where) const
{
if (cycle.empty())
throw std::runtime_error(std::string(where)
+ " expects a non-empty cycle");
}
namespace
{
class shortest_path final: public bfs_steps
......@@ -344,6 +351,7 @@ namespace spot
twa_run_ptr twa_run::reduce() const
{
ensure_non_empty_cycle("twa_run::reduce()");
auto& a = aut;
auto res = std::make_shared<twa_run>(a);
state_set ss;
......@@ -503,6 +511,7 @@ namespace spot
bool twa_run::replay(std::ostream& os, bool debug) const
{
ensure_non_empty_cycle("twa_run::replay()");
const state* s = aut->get_init_state();
int serial = 1;
const twa_run::steps* l;
......@@ -755,6 +764,7 @@ namespace spot
twa_graph_ptr
twa_run::as_twa(bool preserve_names) const
{
ensure_non_empty_cycle("twa_run::as_twa()");
auto d = aut->get_dict();
auto res = make_twa_graph(d);
res->copy_ap_of(aut);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de
// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -402,6 +402,15 @@ namespace spot
twa_run(const twa_run& run);
twa_run& operator=(const twa_run& run);
/// \brief Raise an exception of the cycle is empty.
///
/// It is OK for a twa_run to have an empty cycle while the run is
/// being filled by some procedure. But after that, we expect
/// cycles to be non-empty. Calling this function will raise an
/// std::runtime_error if the cycle is empty, giving \a where
/// (usually the name of the calling function) as context.
void ensure_non_empty_cycle(const char* where) const;
/// \brief Reduce an accepting run.
///
/// Return a run which is still accepting for <code>aut</code>,
......
......@@ -59,3 +59,19 @@ try:
si.determine_unknown_acceptance()
except RuntimeError as e:
assert "scc_info::determine_unknown_acceptance() does not supp" in str(e)
r = spot.twa_run(aut)
try:
a = r.as_twa()
except RuntimeError as e:
assert "empty cycle" in str(e)
try:
a = r.replay(spot.get_cout())
except RuntimeError as e:
assert "empty cycle" in str(e)
try:
a = r.reduce()
except RuntimeError as e:
assert "empty cycle" in str(e)
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