diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 03ade57c9..3850acd74 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -1186,9 +1186,8 @@ namespace { // r == true iff the automaton i is accepting. bool r = false; - unsigned c = m->scc_count(); - for (unsigned j = 0; j < c; ++j) - if (m->is_accepting_scc(j)) + for (auto& scc: *m) + if (scc.is_accepting()) { r = true; break; @@ -1240,15 +1239,13 @@ namespace // Collect all the states of SSPACE that appear in the accepting SCCs // of PROD. (Trivial SCCs are considered accepting.) static void - states_in_acc(const spot::scc_info* m, - state_set& s) + states_in_acc(const spot::scc_info* m, state_set& s) { auto aut = m->get_aut(); auto ps = aut->get_named_prop("product-states"); - unsigned c = m->scc_count(); - for (unsigned n = 0; n < c; ++n) - if (m->is_accepting_scc(n) || m->is_trivial(n)) - for (auto i: m->states_of(n)) + for (auto& scc: *m) + if (scc.is_accepting() || scc.is_trivial()) + for (auto i: scc.states()) // Get the projection on sspace. s.insert((*ps)[i].second); } diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 56e01e835..ecd02dfd7 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) +// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche +// et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -25,22 +25,21 @@ namespace spot { bool is_guarantee_automaton(const const_tgba_digraph_ptr& aut, - const scc_info* sm) + const scc_info* si) { // Create an scc_info if the user did not give one to us. - bool need_sm = !sm; - if (need_sm) - sm = new scc_info(aut); + bool need_si = !si; + if (need_si) + si = new scc_info(aut); bool result = true; - unsigned scc_count = sm->scc_count(); - for (unsigned scc = 0; scc < scc_count; ++scc) + for (auto& scc: *si) { - if (!sm->is_accepting_scc(scc)) + if (!scc.is_accepting()) continue; // Accepting SCCs should have only one state. - auto& st = sm->states_of(scc); + auto& st = scc.states(); if (st.size() != 1) { result = false; @@ -58,8 +57,8 @@ namespace spot break; } - if (need_sm) - delete sm; + if (need_si) + delete si; return result; } diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index c8f8a7fb1..9e5f1289e 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -100,7 +100,7 @@ namespace spot // Fill STATES with any state removed, so that // remove_component() does not have to traverse the SCC // again. - root_.front().node.states.push_front(curr); + root_.front().node.states_.push_front(curr); // When backtracking the root of an SCC, we must also // remove that SCC from the ARC/ROOT stacks. We must @@ -109,23 +109,23 @@ namespace spot if (root_.front().index == h_[curr]) { int num = node_.size(); - for (auto s: root_.front().node.states) + for (auto s: root_.front().node.states_) { sccof_[s] = num; h_[s] = num + 1; } bdd cond = root_.front().in_cond; - auto acc = root_.front().node.acc; - bool triv = root_.front().node.trivial; + auto acc = root_.front().node.acc_marks(); + bool triv = root_.front().node.is_trivial(); node_.emplace_back(acc, triv); - std::swap(node_.back().succ, root_.front().node.succ); - std::swap(node_.back().states, root_.front().node.states); - node_.back().accepting = !triv && aut->acc().accepting(acc); + std::swap(node_.back().succ_, root_.front().node.succ_); + std::swap(node_.back().states_, root_.front().node.states_); + node_.back().accepting_ = !triv && aut->acc().accepting(acc); root_.pop_front(); // Record the transition between the SCC being popped // and the previous SCC. if (!root_.empty()) - root_.front().node.succ.emplace_back(cond, num); + root_.front().node.succ_.emplace_back(cond, num); } continue; } @@ -159,7 +159,7 @@ namespace spot --spi; // Record that there is a transition from this SCC to the // dest SCC labelled with cond. - auto& succ = root_.front().node.succ; + auto& succ = root_.front().node.succ_; scc_succs::iterator i = std::find_if(succ.begin(), succ.end(), [spi](const scc_trans& x) { return (x.dst == @@ -189,13 +189,13 @@ namespace spot while (threshold > root_.front().index) { assert(!root_.empty()); - acc |= root_.front().node.acc; + acc |= root_.front().node.acc_; acc |= root_.front().in_acc; - states.splice(states.end(), root_.front().node.states); + states.splice(states.end(), root_.front().node.states_); succs.insert(succs.end(), - root_.front().node.succ.begin(), - root_.front().node.succ.end()); + root_.front().node.succ_.begin(), + root_.front().node.succ_.end()); root_.pop_front(); } @@ -206,24 +206,31 @@ namespace spot // Accumulate all acceptance conditions, states, SCC // successors, and conditions into the merged SCC. - root_.front().node.acc |= acc; - root_.front().node.states.splice(root_.front().node.states.end(), - states); - root_.front().node.succ.insert(root_.front().node.succ.end(), - succs.begin(), succs.end()); + root_.front().node.acc_ |= acc; + root_.front().node.states_.splice(root_.front().node.states_.end(), + states); + root_.front().node.succ_.insert(root_.front().node.succ_.end(), + succs.begin(), succs.end()); // This SCC is no longer trivial. - root_.front().node.trivial = false; + root_.front().node.trivial_ = false; } // An SCC is useful if it is accepting or it has a successor SCC // that is useful. unsigned scccount = scc_count(); - for (unsigned i = 0; i < scccount; i++) + for (unsigned i = 0; i < scccount; ++i) { - bool useful = node_[i].accepting; - for (auto j: node_[i].succ) - useful |= node_[j.dst].useful; - node_[i].useful = useful; + if (node_[i].is_accepting()) + { + node_[i].useful_ = true; + continue; + } + for (auto j: node_[i].succ()) + if (node_[j.dst].is_useful()) + { + node_[i].useful_ = true; + break; + } } } diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 0588dd5cb..1d209312c 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -25,7 +25,6 @@ namespace spot { - class SPOT_API scc_info { public: @@ -41,24 +40,56 @@ namespace spot typedef std::vector scc_succs; - struct scc_node + class scc_node { + friend class scc_info; + protected: + scc_succs succ_; + acc_cond::mark_t acc_; + std::list states_; // States of the component + bool trivial_:1; + bool accepting_:1; + bool useful_:1; + public: scc_node(): - acc(0U), trivial(true), accepting(false), useful(false) + acc_(0U), trivial_(true), accepting_(false), useful_(false) { } scc_node(acc_cond::mark_t acc, bool trivial): - acc(acc), trivial(trivial), accepting(false), useful(false) + acc_(acc), trivial_(trivial), accepting_(false), useful_(false) { } - scc_succs succ; - acc_cond::mark_t acc; - std::list states; // States of the component - bool trivial:1; - bool accepting:1; - bool useful:1; + bool is_trivial() const + { + return trivial_; + } + + bool is_accepting() const + { + return accepting_; + } + + bool is_useful() const + { + return useful_; + } + + acc_cond::mark_t acc_marks() const + { + return acc_; + } + + const std::list& states() const + { + return states_; + } + + const scc_succs& succ() const + { + return succ_; + } }; protected: @@ -98,9 +129,22 @@ namespace spot return sccof_[st]; } + auto begin() const + SPOT_RETURN(node_.begin()); + auto end() const + SPOT_RETURN(node_.end()); + auto cbegin() const + SPOT_RETURN(node_.cbegin()); + auto cend() const + SPOT_RETURN(node_.cend()); + auto rbegin() const + SPOT_RETURN(node_.rbegin()); + auto rend() const + SPOT_RETURN(node_.rend()); + const std::list& states_of(unsigned scc) const { - return node(scc).states; + return node(scc).states(); } unsigned one_state_of(unsigned scc) const @@ -117,32 +161,32 @@ namespace spot const scc_succs& succ(unsigned scc) const { - return node(scc).succ; + return node(scc).succ(); } bool is_trivial(unsigned scc) const { - return node(scc).trivial; + return node(scc).is_trivial(); } acc_cond::mark_t acc(unsigned scc) const { - return node(scc).acc; + return node(scc).acc_marks(); } bool is_accepting_scc(unsigned scc) const { - return node(scc).accepting; + return node(scc).is_accepting(); } bool is_useful_scc(unsigned scc) const { - return node(scc).useful; + return node(scc).is_useful(); } bool is_useful_state(unsigned st) const { - return reachable_state(st) && node(scc_of(st)).useful; + return reachable_state(st) && node(scc_of(st)).is_useful(); } /// \brief Return the set of all used acceptance combinations, for