diff --git a/NEWS b/NEWS index e64801692..6370fbd06 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,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: diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 606c6d3ab..3c8284899 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -282,6 +282,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 @@ -343,6 +350,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(a); state_set ss; @@ -502,6 +510,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; @@ -754,6 +763,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); diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index bbbed6390..c83a9e768 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -1,5 +1,5 @@ // -*- 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 aut, diff --git a/tests/python/except.py b/tests/python/except.py index be8169ba9..12687ec6a 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -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)