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.
This commit is contained in:
parent
76d4fe236c
commit
a445778cd8
4 changed files with 39 additions and 1 deletions
3
NEWS
3
NEWS
|
|
@ -12,6 +12,9 @@ New in spot 2.5.1.dev (not yet released)
|
||||||
- "autfilt --acceptance-is=Fin-less" no longer accept automata
|
- "autfilt --acceptance-is=Fin-less" no longer accept automata
|
||||||
with "f" acceptance.
|
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)
|
New in spot 2.5.1 (2018-02-20)
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
|
||||||
|
|
@ -282,6 +282,13 @@ namespace spot
|
||||||
return os;
|
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
|
namespace
|
||||||
{
|
{
|
||||||
class shortest_path final: public bfs_steps
|
class shortest_path final: public bfs_steps
|
||||||
|
|
@ -343,6 +350,7 @@ namespace spot
|
||||||
|
|
||||||
twa_run_ptr twa_run::reduce() const
|
twa_run_ptr twa_run::reduce() const
|
||||||
{
|
{
|
||||||
|
ensure_non_empty_cycle("twa_run::reduce()");
|
||||||
auto& a = aut;
|
auto& a = aut;
|
||||||
auto res = std::make_shared<twa_run>(a);
|
auto res = std::make_shared<twa_run>(a);
|
||||||
state_set ss;
|
state_set ss;
|
||||||
|
|
@ -502,6 +510,7 @@ namespace spot
|
||||||
|
|
||||||
bool twa_run::replay(std::ostream& os, bool debug) const
|
bool twa_run::replay(std::ostream& os, bool debug) const
|
||||||
{
|
{
|
||||||
|
ensure_non_empty_cycle("twa_run::replay()");
|
||||||
const state* s = aut->get_init_state();
|
const state* s = aut->get_init_state();
|
||||||
int serial = 1;
|
int serial = 1;
|
||||||
const twa_run::steps* l;
|
const twa_run::steps* l;
|
||||||
|
|
@ -754,6 +763,7 @@ namespace spot
|
||||||
twa_graph_ptr
|
twa_graph_ptr
|
||||||
twa_run::as_twa(bool preserve_names) const
|
twa_run::as_twa(bool preserve_names) const
|
||||||
{
|
{
|
||||||
|
ensure_non_empty_cycle("twa_run::as_twa()");
|
||||||
auto d = aut->get_dict();
|
auto d = aut->get_dict();
|
||||||
auto res = make_twa_graph(d);
|
auto res = make_twa_graph(d);
|
||||||
res->copy_ap_of(aut);
|
res->copy_ap_of(aut);
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Recherche et Developpement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
// 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(const twa_run& run);
|
||||||
twa_run& operator=(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.
|
/// \brief Reduce an accepting run.
|
||||||
///
|
///
|
||||||
/// Return a run which is still accepting for <code>aut</code>,
|
/// Return a run which is still accepting for <code>aut</code>,
|
||||||
|
|
|
||||||
|
|
@ -59,3 +59,19 @@ try:
|
||||||
si.determine_unknown_acceptance()
|
si.determine_unknown_acceptance()
|
||||||
except RuntimeError as e:
|
except RuntimeError as e:
|
||||||
assert "scc_info::determine_unknown_acceptance() does not supp" in str(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)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue