diff --git a/NEWS b/NEWS index d57cb59e0..8545115b7 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,9 @@ New in spot 2.2.1.dev (Not yet released) + Library: + + * A twa is required to have at least one state, the initial state. + Build: * If the system has an installed libltdl library, use it instead of diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh index 27bc9eeb4..59c5b9ae5 100644 --- a/spot/kripke/kripkegraph.hh +++ b/spot/kripke/kripkegraph.hh @@ -177,16 +177,15 @@ namespace spot graph_t::state get_init_state_number() const { + // If the kripke has no state, it has no initial state. if (num_states() == 0) - const_cast(g_).new_state(); + throw std::runtime_error("kripke has no state at all"); return init_number_; } virtual const kripke_graph_state* get_init_state() const override { - if (num_states() == 0) - const_cast(g_).new_state(); - return state_from_number(init_number_); + return state_from_number(get_init_state_number()); } /// \brief Allow to get an iterator on the state we passed in diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index fb9b6a9ef..c3ada782d 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -595,7 +595,8 @@ namespace spot /// Browsing a TωA is usually achieved using two methods: \c /// get_init_state(), and succ(). The former returns the initial /// state while the latter allows iterating over the outgoing edges - /// of any given state. + /// of any given state. A TωA is always assumed to have at least + /// one state, the initial one. /// /// Note that although this is a transition-based automata, we never /// represent edges in the API. Information about edges can be @@ -605,7 +606,7 @@ namespace spot /// The interface presented here is what we call the on-the-fly /// interface of automata, because the TωA class can be subclassed /// to implement an object that computes its successors on-the-fly. - /// The down-side is that all these methods are virtual, so you you + /// The down-side is that all these methods are virtual, so you /// pay the cost of virtual calls when iterating over automata /// constructed on-the-fly. Also the interface assumes that each /// successor state is a new object whose memory management is the diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 370ab97fb..018268def 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -154,8 +154,6 @@ namespace spot void twa_graph::purge_unreachable_states() { unsigned num_states = g_.num_states(); - if (SPOT_UNLIKELY(num_states == 0)) - return; // The TODO vector serves two purposes: // - it is a stack of state to process, // - it is a set of processed states. @@ -166,7 +164,7 @@ namespace spot std::vector todo(num_states, 0); const unsigned seen = 1 << (sizeof(unsigned)*8-1); const unsigned mask = seen - 1; - todo[0] = init_number_; + todo[0] = get_init_state_number(); todo[init_number_] |= seen; unsigned todo_pos = 1; do @@ -197,16 +195,13 @@ namespace spot void twa_graph::purge_dead_states() { unsigned num_states = g_.num_states(); - if (num_states == 0) - return; - std::vector useful(num_states, 0); // Make a DFS to compute a topological order. std::vector order; order.reserve(num_states); std::vector> todo; // state, trans - useful[init_number_] = 1; + useful[get_init_state_number()] = 1; todo.emplace_back(init_number_, g_.state_storage(init_number_).succ); do { diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index e6736a5ef..1acd66fbe 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -264,16 +264,15 @@ namespace spot state_num get_init_state_number() const { + // If the automaton has no state, it has no initial state. if (num_states() == 0) - const_cast(g_).new_state(); + throw std::runtime_error("automaton has no state at all"); return init_number_; } virtual const twa_graph_state* get_init_state() const override { - if (num_states() == 0) - const_cast(g_).new_state(); - return state_from_number(init_number_); + return state_from_number(get_init_state_number()); } virtual twa_succ_iterator* diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 325387afd..9ddcda168 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -23,11 +23,6 @@ namespace spot { unsigned complete_here(twa_graph_ptr aut) { - // We do not use the initial state, but calling - // get_init_state_number() may create it and change the number of - // states. This has to be done before calling aut->num_states(). - unsigned init = aut->get_init_state_number(); - unsigned n = aut->num_states(); unsigned sink = -1U; @@ -87,7 +82,7 @@ namespace spot // If the automaton is empty, pretend that state 0 is a sink. if (t == 0) - sink = init; + sink = aut->get_init_state_number(); // Now complete all states (excluding any newly added the sink). for (unsigned i = 0; i < n; ++i) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index f46d33e53..4dc76e3b5 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -312,16 +312,13 @@ namespace spot } } - // Calling get_init_state_number() may add a state to empty - // automata, so it has to be done first. - unsigned init = aut->get_init_state_number(); - metadata md(aut, implicit_labels, state_labels); if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) acceptance = Hoa_Acceptance_Transitions; unsigned num_states = aut->num_states(); + unsigned init = aut->get_init_state_number(); const char nl = newline ? '\n' : ' '; os << (v1_1 ? "HOA: v1.1" : "HOA: v1") << nl; diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index b6403bf4b..a164a90e2 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -171,6 +171,10 @@ namespace spot init_state->destroy(); res->set_init_state(init_num); } + else + { + res->set_init_state(res->new_state()); + } return res; } diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 7e064a3d4..cef41e554 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2011, 2013-2016 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -101,11 +101,8 @@ namespace spot unsigned nap = number_of_variables(allap); - // Call this before aut->num_states(), since it might add a state. unsigned init_num = aut->get_init_state_number(); - unsigned ns = aut->num_states(); - assert(ns > 0); if ((-1UL / ns) >> nap == 0) throw std::runtime_error("too many atomic propositions (or states)"); diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index f74499a97..5cff2cd42 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -277,8 +277,6 @@ namespace spot scc_info* given_si, Args&&... args) { unsigned in_n = aut->num_states(); - if (in_n == 0) // nothing to filter. - return make_twa_graph(aut, twa::prop_set::all()); twa_graph_ptr filtered = make_twa_graph(aut->get_dict()); filtered->copy_ap_of(aut); diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 0392a0a6c..ba3d66488 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -161,14 +161,11 @@ namespace spot throw std::runtime_error ("direct_simulation() requires separate Inf and Fin sets"); - // Call get_init_state_number() before anything else as it - // might add a state. - unsigned init_state_number = in->get_init_state_number(); scc_info_.reset(new scc_info(in)); unsigned ns = in->num_states(); - assert(ns > 0); size_a_ = ns; + unsigned init_state_number = in->get_init_state_number(); auto all_inf = in->get_acceptance().used_inf_fin_sets().first; all_inf_ = all_inf;