diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 2ef5a33c0..56476428e 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -216,7 +216,7 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; -typedef spot::twa_graph::graph_t::trans_storage_t tr_t; +typedef spot::twa_graph::graph_t::edge_storage_t tr_t; typedef std::set> unique_aut_t; static long int match_count = 0; static spot::option_map extra_options; @@ -502,7 +502,7 @@ namespace // If --stats or --name is used, duplicate the automaton so we // never modify the original automaton (e.g. with - // merge_transitions()) and the statistics about it make sense. + // merge_edges()) and the statistics about it make sense. auto aut = ((automaton_format == Stats) || opt_name) ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all()) : haut->aut; @@ -512,7 +512,7 @@ namespace if (opt_stripacc) spot::strip_acceptance_here(aut); if (opt_merge) - aut->merge_transitions(); + aut->merge_edges(); if (opt_clean_acc || opt_rem_fin) cleanup_acceptance_here(aut); if (opt_sep_sets) @@ -534,7 +534,7 @@ namespace bool matched = true; matched &= opt_states.contains(aut->num_states()); - matched &= opt_edges.contains(aut->num_transitions()); + matched &= opt_edges.contains(aut->num_edges()); matched &= opt_accsets.contains(aut->acc().num_sets()); if (opt_is_complete) matched &= is_complete(aut); @@ -602,8 +602,8 @@ namespace auto tmp = spot::canonicalize(make_twa_graph(aut, spot::twa::prop_set::all())); - if (!opt->uniq->emplace(tmp->transition_vector().begin() + 1, - tmp->transition_vector().end()).second) + if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1, + tmp->edge_vector().end()).second) return 0; } @@ -681,7 +681,7 @@ main(int argc, char** argv) if (opt->are_isomorphic) { if (opt_merge) - opt->are_isomorphic->merge_transitions(); + opt->are_isomorphic->merge_edges(); opt->isomorphism_checker = std::unique_ptr (new spot::isomorphism_checker(opt->are_isomorphic)); } diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 6958c8d99..7500274a2 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1151,7 +1151,7 @@ namespace if (x[i]->acc().uses_fin_acceptance()) \ { \ auto st = x[i]->num_states(); \ - auto tr = x[i]->num_transitions(); \ + auto tr = x[i]->num_edges(); \ auto ac = x[i]->acc().num_sets(); \ x[i] = remove_fin(x[i]); \ if (verbose) \ @@ -1161,7 +1161,7 @@ namespace << tr << " ed., " \ << ac << " sets) -> (" \ << x[i]->num_states() << " st., " \ - << x[i]->num_transitions() << " ed., " \ + << x[i]->num_edges() << " ed., " \ << x[i]->acc().num_sets() << " sets)\n"; \ } \ } @@ -1246,7 +1246,7 @@ namespace if (verbose) std::cerr << "info: state-space has " - << statespace->num_transitions() + << statespace->num_edges() << " edges\n"; // Products of the state space with the positive automata. @@ -1263,7 +1263,7 @@ namespace std::cerr << ("info: building product between state-space and" " P") << i << " (" << pos[i]->num_states() << " st., " - << pos[i]->num_transitions() << " ed.)\n"; + << pos[i]->num_edges() << " ed.)\n"; auto p = spot::product(pos[i], statespace); pos_prod[i] = p; auto sm = new spot::scc_info(p); @@ -1287,7 +1287,7 @@ namespace std::cerr << ("info: building product between state-space and" " N") << i << " (" << neg[i]->num_states() << " st., " - << neg[i]->num_transitions() << " ed.)\n"; + << neg[i]->num_edges() << " ed.)\n"; auto p = spot::product(neg[i], statespace); neg_prod[i] = p; diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 5174a8edb..7946c3970 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -63,7 +63,7 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\n\ \n\ Build 3 random, complete, and deterministic Rabin automata\n\ with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\ -a high density of transitions, and 3 to 4 atomic propositions:\n\ +a high density of edges, and 3 to 4 atomic propositions:\n\ % randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\ "; @@ -79,15 +79,15 @@ static const argp_option options[] = { "acceptance", 'A', "ACCEPTANCE", 0, "specify the acceptance type of the automaton", 0 }, { "acc-probability", 'a', "FLOAT", 0, - "probability that a transition belong to one acceptance set (0.2)", 0 }, + "probability that an edge belongs to one acceptance set (0.2)", 0 }, { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\ "use a negative value for unbounded generation", 0 }, { "ba", 'B', 0, 0, "build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 }, { "colored", OPT_COLORED, 0, 0, - "build an automaton in which each transition (or state if combined with " + "build an automaton in which each edge (or state if combined with " "-S) belong to a single acceptance set", 0 }, - { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 }, + { "density", 'd', "FLOAT", 0, "density of the edges (0.2)", 0 }, { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ", 0 }, { "unique", 'u', 0, 0, @@ -133,7 +133,7 @@ static const struct argp_child children[] = }; static const char* opt_acceptance = nullptr; -typedef spot::twa_graph::graph_t::trans_storage_t tr_t; +typedef spot::twa_graph::graph_t::edge_storage_t tr_t; typedef std::set> unique_aut_t; static spot::ltl::atomic_prop_set aprops; static range ap_count_given = {-1, -2}; // Must be two different negative val @@ -364,8 +364,8 @@ main(int argc, char** argv) { auto tmp = spot::canonicalize (make_twa_graph(aut, spot::twa::prop_set::all())); - std::vector trans(tmp->transition_vector().begin() + 1, - tmp->transition_vector().end()); + std::vector trans(tmp->edge_vector().begin() + 1, + tmp->edge_vector().end()); if (!opt_uniq->emplace(trans).second) { --trials; diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index ff64411c1..fc718d038 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -247,12 +247,12 @@ namespace spot unsigned in_scc = sm_.scc_of_state(sin); bdd cond = si->current_condition(); - unsigned t = out_->new_transition(in, out, cond); + unsigned t = out_->new_edge(in, out, cond); if (realizable_[in_scc]) { if (final_.find(sin) != final_.end()) - out_->trans_data(t).acc = acc_; + out_->edge_data(t).acc = acc_; } else if (sm_.scc_of_state(sout) == in_scc) { @@ -278,12 +278,11 @@ namespace spot // implementation create more transitions than needed: // we do not need more than one transition per // accepting cycle. - out_->new_transition(in, out + shift, cond); + out_->new_edge(in, out + shift, cond); // Acceptance transitions are those in the Li // set. (Löding's Fi set.) - out_->new_acc_transition(in + shift, out + shift, cond, - l.get(i)); + out_->new_acc_edge(in + shift, out + shift, cond, l.get(i)); } } } diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index afb8a5d23..e8fc0043b 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -275,7 +275,7 @@ states: { for (map_t::const_iterator i = result.dest_map.begin(); i != result.dest_map.end(); ++i) - result.d->aut->new_transition(result.cur_state, i->first, i->second); + result.d->aut->new_edge(result.cur_state, i->first, i->second); } %% diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 7e470d41a..2c6598e7f 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -70,7 +70,7 @@ namespace spot int out = d_->aut->state_number(sout); bdd cond = si->current_condition(); - out_->new_transition(in, out, cond); + out_->new_edge(in, out, cond); // Create one clone of the automaton per accepting pair, // removing states from the Ui part of the (Li, Ui) pairs. @@ -94,12 +94,11 @@ namespace spot // implementation create more transitions than needed: // we do not need more than one transition per // accepting cycle. - out_->new_transition(in, out + shift, cond); + out_->new_edge(in, out + shift, cond); // A transition is accepting if it is in the Li // set. (Löding's Fi set.) - out_->new_acc_transition(in + shift, out + shift, cond, - l.get(i)); + out_->new_acc_edge(in + shift, out + shift, cond, l.get(i)); } } } diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 15b70081c..25ab54219 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -155,7 +155,7 @@ namespace spot dest = dres.first->second = res->new_state(); todo.push_back(d); } - res->new_transition(src, dest, t.cond, acc); + res->new_edge(src, dest, t.cond, acc); // Jump to level ∅ if (s.pend == 0) @@ -175,7 +175,7 @@ namespace spot dest = dres.first->second = res->new_state(); todo.push_back(d); } - res->new_transition(src, dest, t.cond); + res->new_edge(src, dest, t.cond); } } } diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 8497c152d..3cd1fec50 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -30,7 +30,7 @@ namespace spot { - template + template class SPOT_API digraph; namespace internal @@ -144,12 +144,12 @@ namespace spot // We have two implementations, one with attached State_Data, and // one without. - template + template struct SPOT_API distate_storage final: public State_Data { - Transition succ = 0; // First outgoing transition (used when iterating) - Transition succ_tail = 0; // Last outgoing transition (used for - // appending new transitions) + Edge succ = 0; // First outgoing edge (used when iterating) + Edge succ_tail = 0; // Last outgoing edge (used for + // appending new edges) template - struct SPOT_API trans_storage final: public Trans_Data + typename StateOut, typename Edge, typename Edge_Data> + struct SPOT_API edge_storage final: public Edge_Data { - typedef Transition transition; + typedef Edge edge; StateOut dst; // destination - Transition next_succ; // next outgoing transition with same + Edge next_succ; // next outgoing edge with same // source, or 0 StateIn src; // source - explicit trans_storage() - : Trans_Data{} + explicit edge_storage() + : Edge_Data{} { } template - trans_storage(StateOut dst, Transition next_succ, + edge_storage(StateOut dst, Edge next_succ, StateIn src, Args&&... args) - : Trans_Data{std::forward(args)...}, + : Edge_Data{std::forward(args)...}, dst(dst), next_succ(next_succ), src(src) { } - bool operator<(const trans_storage& other) const + bool operator<(const edge_storage& other) const { if (src < other.src) return true; @@ -204,7 +204,7 @@ namespace spot return this->data() < other.data(); } - bool operator==(const trans_storage& other) const + bool operator==(const edge_storage& other) const { return src == other.src && dst == other.dst && @@ -213,46 +213,46 @@ namespace spot }; ////////////////////////////////////////////////// - // Transition iterator + // Edge iterator ////////////////////////////////////////////////// - // This holds a graph and a transition number that is the start of - // a list, and it iterates over all the trans_storage_t elements + // This holds a graph and a edge number that is the start of + // a list, and it iterates over all the edge_storage_t elements // of that list. template - class SPOT_API trans_iterator: + class SPOT_API edge_iterator: std::iterator::value, - const typename Graph::trans_storage_t, - typename Graph::trans_storage_t>::type> + const typename Graph::edge_storage_t, + typename Graph::edge_storage_t>::type> { typedef std::iterator::value, - const typename Graph::trans_storage_t, - typename Graph::trans_storage_t>::type> + const typename Graph::edge_storage_t, + typename Graph::edge_storage_t>::type> super; public: - typedef typename Graph::transition transition; + typedef typename Graph::edge edge; - trans_iterator() + edge_iterator() : g_(nullptr), t_(0) { } - trans_iterator(Graph* g, transition t): g_(g), t_(t) + edge_iterator(Graph* g, edge t): g_(g), t_(t) { } - bool operator==(trans_iterator o) const + bool operator==(edge_iterator o) const { return t_ == o.t_; } - bool operator!=(trans_iterator o) const + bool operator!=(edge_iterator o) const { return t_ != o.t_; } @@ -260,24 +260,24 @@ namespace spot typename super::reference operator*() { - return g_->trans_storage(t_); + return g_->edge_storage(t_); } typename super::pointer operator->() { - return &g_->trans_storage(t_); + return &g_->edge_storage(t_); } - trans_iterator operator++() + edge_iterator operator++() { t_ = operator*().next_succ; return *this; } - trans_iterator operator++(int) + edge_iterator operator++(int) { - trans_iterator ti = *this; + edge_iterator ti = *this; t_ = operator*().next_succ; return ti; } @@ -287,52 +287,52 @@ namespace spot return t_; } - transition trans() const + edge trans() const { return t_; } protected: Graph* g_; - transition t_; + edge t_; }; template - class SPOT_API killer_trans_iterator: public trans_iterator + class SPOT_API killer_edge_iterator: public edge_iterator { - typedef trans_iterator super; + typedef edge_iterator super; public: typedef typename Graph::state_storage_t state_storage_t; - typedef typename Graph::transition transition; + typedef typename Graph::edge edge; - killer_trans_iterator(Graph* g, transition t, state_storage_t& src): + killer_edge_iterator(Graph* g, edge t, state_storage_t& src): super(g, t), src_(src), prev_(0) { } - killer_trans_iterator operator++() + killer_edge_iterator operator++() { prev_ = this->t_; this->t_ = this->operator*().next_succ; return *this; } - killer_trans_iterator operator++(int) + killer_edge_iterator operator++(int) { - killer_trans_iterator ti = *this; + killer_edge_iterator ti = *this; ++*this; return ti; } - // Erase the current transition and advance the iterator. + // Erase the current edge and advance the iterator. void erase() { - transition next = this->operator*().next_succ; + edge next = this->operator*().next_succ; - // Update source state and previous transitions + // Update source state and previous edges if (prev_) { - this->g_->trans_storage(prev_).next_succ = next; + this->g_->edge_storage(prev_).next_succ = next; } else { @@ -345,18 +345,18 @@ namespace spot assert(next == 0); } - // Erased transitions have themselves as next_succ. + // Erased edges have themselves as next_succ. this->operator*().next_succ = this->t_; - // Advance iterator to next transition. + // Advance iterator to next edge. this->t_ = next; - ++this->g_->killed_trans_; + ++this->g_->killed_edge_; } protected: state_storage_t& src_; - transition prev_; + edge prev_; }; @@ -364,36 +364,36 @@ namespace spot // State OUT ////////////////////////////////////////////////// - // Fake container listing the outgoing transitions of a state. + // Fake container listing the outgoing edges of a state. template class SPOT_API state_out { public: - typedef typename Graph::transition transition; - state_out(Graph* g, transition t): + typedef typename Graph::edge edge; + state_out(Graph* g, edge t): g_(g), t_(t) { } - trans_iterator begin() + edge_iterator begin() { return {g_, t_}; } - trans_iterator end() + edge_iterator end() { return {}; } - void recycle(transition t) + void recycle(edge t) { t_ = t; } protected: Graph* g_; - transition t_; + edge t_; }; ////////////////////////////////////////////////// @@ -401,24 +401,24 @@ namespace spot ////////////////////////////////////////////////// template - class SPOT_API all_trans_iterator: + class SPOT_API all_edge_iterator: std::iterator::value, - const typename Graph::trans_storage_t, - typename Graph::trans_storage_t>::type> + const typename Graph::edge_storage_t, + typename Graph::edge_storage_t>::type> { typedef std::iterator::value, - const typename Graph::trans_storage_t, - typename Graph::trans_storage_t>::type> + const typename Graph::edge_storage_t, + typename Graph::edge_storage_t>::type> super; typedef typename std::conditional::value, - const typename Graph::trans_vector, - typename Graph::trans_vector>::type + const typename Graph::edge_vector_t, + typename Graph::edge_vector_t>::type tv_t; unsigned t_; @@ -433,36 +433,36 @@ namespace spot } public: - all_trans_iterator(unsigned pos, tv_t& tv) + all_edge_iterator(unsigned pos, tv_t& tv) : t_(pos), tv_(tv) { skip_(); } - all_trans_iterator(tv_t& tv) + all_edge_iterator(tv_t& tv) : t_(tv.size()), tv_(tv) { } - all_trans_iterator& operator++() + all_edge_iterator& operator++() { skip_(); return *this; } - all_trans_iterator operator++(int) + all_edge_iterator operator++(int) { - all_trans_iterator old = *this; + all_edge_iterator old = *this; ++*this; return old; } - bool operator==(all_trans_iterator o) const + bool operator==(all_edge_iterator o) const { return t_ == o.t_; } - bool operator!=(all_trans_iterator o) const + bool operator!=(all_edge_iterator o) const { return t_ != o.t_; } @@ -485,10 +485,10 @@ namespace spot class SPOT_API all_trans { typedef typename std::conditional::value, - const typename Graph::trans_vector, - typename Graph::trans_vector>::type + const typename Graph::edge_vector_t, + typename Graph::edge_vector_t>::type tv_t; - typedef all_trans_iterator iter_t; + typedef all_edge_iterator iter_t; tv_t& tv_; public: @@ -513,69 +513,69 @@ namespace spot // The actual graph implementation - template + template class digraph { - friend class internal::trans_iterator; - friend class internal::trans_iterator; - friend class internal::killer_trans_iterator; + friend class internal::edge_iterator; + friend class internal::edge_iterator; + friend class internal::killer_edge_iterator; public: - typedef internal::trans_iterator iterator; - typedef internal::trans_iterator const_iterator; + typedef internal::edge_iterator iterator; + typedef internal::edge_iterator const_iterator; static constexpr bool alternating() { return Alternating; } - // Extra data to store on each state or transition. + // Extra data to store on each state or edge. typedef State_Data state_data_t; - typedef Trans_Data trans_data_t; + typedef Edge_Data edge_data_t; - // State and transitions are identified by their indices in some + // State and edges are identified by their indices in some // vector. typedef unsigned state; - typedef unsigned transition; + typedef unsigned edge; - // The type of an output state (when seen from a transition) + // The type of an output state (when seen from a edge) // depends on the kind of graph we build typedef typename std::conditional, state>::type out_state; - typedef internal::distate_storage> state_storage_t; - typedef internal::trans_storage> - trans_storage_t; + typedef internal::edge_storage> + edge_storage_t; typedef std::vector state_vector; - typedef std::vector trans_vector; + typedef std::vector edge_vector_t; protected: state_vector states_; - trans_vector transitions_; - // Number of erased transitions. - unsigned killed_trans_; + edge_vector_t edges_; + // Number of erased edges. + unsigned killed_edge_; public: /// \brief construct an empty graph /// /// Construct an empty graph, and reserve space for \a max_states - /// states and \a max_trans transitions. These are not hard + /// states and \a max_trans edges. These are not hard /// limits, but just hints to pre-allocate a data structure that /// may hold that much items. digraph(unsigned max_states = 10, unsigned max_trans = 0) - : killed_trans_(0) + : killed_edge_(0) { states_.reserve(max_states); if (max_trans == 0) max_trans = max_states * 2; - transitions_.reserve(max_trans + 1); - // Transition number 0 is not used, because we use this index - // to mark the absence of a transition. - transitions_.resize(1); - // This causes transition 0 to be considered as dead. - transitions_[0].next_succ = 0; + edges_.reserve(max_trans + 1); + // Edge number 0 is not used, because we use this index + // to mark the absence of a edge. + edges_.resize(1); + // This causes edge 0 to be considered as dead. + edges_[0].next_succ = 0; } unsigned num_states() const @@ -583,17 +583,17 @@ namespace spot return states_.size(); } - unsigned num_transitions() const + unsigned num_edges() const { - return transitions_.size() - killed_trans_ - 1; + return edges_.size() - killed_edge_ - 1; } - bool valid_trans(transition t) const + bool valid_trans(edge t) const { - // Erased transitions have their next_succ pointing to + // Erased edges have their next_succ pointing to // themselves. - return (t < transitions_.size() && - transitions_[t].next_succ != t); + return (t < edges_.size() && + edges_[t].next_succ != t); } template @@ -645,49 +645,49 @@ namespace spot return states_[s].data(); } - trans_storage_t& - trans_storage(transition s) + edge_storage_t& + edge_storage(edge s) { - assert(s < transitions_.size()); - return transitions_[s]; + assert(s < edges_.size()); + return edges_[s]; } - const trans_storage_t& - trans_storage(transition s) const + const edge_storage_t& + edge_storage(edge s) const { - assert(s < transitions_.size()); - return transitions_[s]; + assert(s < edges_.size()); + return edges_[s]; } - typename trans_storage_t::data_t& - trans_data(transition s) + typename edge_storage_t::data_t& + edge_data(edge s) { - assert(s < transitions_.size()); - return transitions_[s].data(); + assert(s < edges_.size()); + return edges_[s].data(); } - const typename trans_storage_t::data_t& - trans_data(transition s) const + const typename edge_storage_t::data_t& + edge_data(edge s) const { - assert(s < transitions_.size()); - return transitions_[s].data(); + assert(s < edges_.size()); + return edges_[s].data(); } template - transition - new_transition(state src, out_state dst, Args&&... args) + edge + new_edge(state src, out_state dst, Args&&... args) { assert(src < states_.size()); - transition t = transitions_.size(); - transitions_.emplace_back(dst, 0, src, std::forward(args)...); + edge t = edges_.size(); + edges_.emplace_back(dst, 0, src, std::forward(args)...); - transition st = states_[src].succ_tail; + edge st = states_[src].succ_tail; assert(st < t || !st); if (!st) states_[src].succ = t; else - transitions_[st].next_succ = t; + edges_[st].next_succ = t; states_[src].succ_tail = t; return t; } @@ -698,10 +698,10 @@ namespace spot return &ss - &states_.front(); } - transition index_of_transition(const trans_storage_t& tt) const + edge index_of_edge(const edge_storage_t& tt) const { - assert(!transitions_.empty()); - return &tt - &transitions_.front(); + assert(!edges_.empty()); + return &tt - &edges_.front(); } internal::state_out @@ -728,13 +728,13 @@ namespace spot return out(index_of_state(src)); } - internal::killer_trans_iterator + internal::killer_edge_iterator out_iteraser(state_storage_t& src) { return {this, src.succ, src}; } - internal::killer_trans_iterator + internal::killer_edge_iterator out_iteraser(state src) { return out_iteraser(state_storage(src)); @@ -750,52 +750,52 @@ namespace spot return states_; } - internal::all_trans transitions() const + internal::all_trans edges() const { - return transitions_; + return edges_; } - internal::all_trans transitions() + internal::all_trans edges() { - return transitions_; + return edges_; } - // When using this method, beware that the first entry (transition - // #0) is not a real transition, and that any transition with - // next_succ pointing to itself is an erased transition. + // When using this method, beware that the first entry (edge + // #0) is not a real edge, and that any edge with + // next_succ pointing to itself is an erased edge. // - // You should probably use transitions() instead. - const trans_vector& transition_vector() const + // You should probably use edges() instead. + const edge_vector_t& edge_vector() const { - return transitions_; + return edges_; } - trans_vector& transition_vector() + edge_vector_t& edge_vector() { - return transitions_; + return edges_; } - bool is_dead_transition(unsigned t) const + bool is_dead_edge(unsigned t) const { - return transitions_[t].next_succ == t; + return edges_[t].next_succ == t; } - bool is_dead_transition(const trans_storage_t& t) const + bool is_dead_edge(const edge_storage_t& t) const { - return t.next_succ == index_of_transition(t); + return t.next_succ == index_of_edge(t); } // To help debugging void dump_storage(std::ostream& o) const { - unsigned tend = transitions_.size(); + unsigned tend = edges_.size(); for (unsigned t = 1; t < tend; ++t) { o << 't' << t << ": (s" - << transitions_[t].src << ", s" - << transitions_[t].dst << ") t" - << transitions_[t].next_succ << '\n'; + << edges_[t].src << ", s" + << edges_[t].dst << ") t" + << edges_[t].next_succ << '\n'; } unsigned send = states_.size(); for (unsigned s = 0; s < send; ++s) @@ -806,49 +806,49 @@ namespace spot } } - // Remove all dead transitions. The transitions_ vector is left + // Remove all dead edges. The edges_ vector is left // in a state that is incorrect and should eventually be fixed by - // a call to chain_transitions_() before any iteration on the + // a call to chain_edges_() before any iteration on the // successor of a state is performed. - void remove_dead_transitions_() + void remove_dead_edges_() { - if (killed_trans_ == 0) + if (killed_edge_ == 0) return; - auto i = std::remove_if(transitions_.begin() + 1, transitions_.end(), - [this](const trans_storage_t& t) { - return this->is_dead_transition(t); + auto i = std::remove_if(edges_.begin() + 1, edges_.end(), + [this](const edge_storage_t& t) { + return this->is_dead_edge(t); }); - transitions_.erase(i, transitions_.end()); - killed_trans_ = 0; + edges_.erase(i, edges_.end()); + killed_edge_ = 0; } - // This will invalidate all iterators, and also destroy transition - // chains. Call chain_transitions_() immediately afterwards + // This will invalidate all iterators, and also destroy edge + // chains. Call chain_edges_() immediately afterwards // unless you know what you are doing. - template> - void sort_transitions_(Predicate p = Predicate()) + template> + void sort_edges_(Predicate p = Predicate()) { //std::cerr << "\nbefore\n"; //dump_storage(std::cerr); - std::stable_sort(transitions_.begin() + 1, transitions_.end(), p); + std::stable_sort(edges_.begin() + 1, edges_.end(), p); } - // Should be called only when it is known that all transitions + // Should be called only when it is known that all edges // with the same destination are consecutive in the vector. - void chain_transitions_() + void chain_edges_() { state last_src = -1U; - transition tend = transitions_.size(); - for (transition t = 1; t < tend; ++t) + edge tend = edges_.size(); + for (edge t = 1; t < tend; ++t) { - state src = transitions_[t].src; + state src = edges_[t].src; if (src != last_src) { states_[src].succ = t; if (last_src != -1U) { states_[last_src].succ_tail = t - 1; - transitions_[t - 1].next_succ = 0; + edges_[t - 1].next_succ = 0; } while (++last_src != src) { @@ -858,13 +858,13 @@ namespace spot } else { - transitions_[t - 1].next_succ = t; + edges_[t - 1].next_succ = t; } } if (last_src != -1U) { states_[last_src].succ_tail = tend - 1; - transitions_[tend - 1].next_succ = 0; + edges_[tend - 1].next_succ = 0; } unsigned send = states_.size(); while (++last_src != send) @@ -876,18 +876,18 @@ namespace spot //dump_storage(std::cerr); } - // Rename all the states in the transition vector. The - // transitions_ vector is left in a state that is incorrect and - // should eventually be fixed by a call to chain_transitions_() + // Rename all the states in the edge vector. The + // edges_ vector is left in a state that is incorrect and + // should eventually be fixed by a call to chain_edges_() // before any iteration on the successor of a state is performed. void rename_states_(const std::vector& newst) { assert(newst.size() == states_.size()); - unsigned tend = transitions_.size(); + unsigned tend = edges_.size(); for (unsigned t = 1; t < tend; t++) { - transitions_[t].dst = newst[transitions_[t].dst]; - transitions_[t].src = newst[transitions_[t].src]; + edges_[t].dst = newst[edges_[t].dst]; + edges_[t].src = newst[edges_[t].src]; } } @@ -908,40 +908,40 @@ namespace spot continue; if (dst == -1U) { - // This is an erased state. Mark all its transitions as + // This is an erased state. Mark all its edges as // dead (i.e., t.next_succ should point to t for each of // them). auto t = states_[s].succ; while (t) - std::swap(t, transitions_[t].next_succ); + std::swap(t, edges_[t].next_succ); continue; } states_[dst] = std::move(states_[s]); } states_.resize(used_states); - // Shift all transitions in transitions_. The algorithm is + // Shift all edges in edges_. The algorithm is // similar to remove_if, but it also keeps the correspondence // between the old and new index as newidx[old] = new. - unsigned tend = transitions_.size(); - std::vector newidx(tend); + unsigned tend = edges_.size(); + std::vector newidx(tend); unsigned dest = 1; - for (transition t = 1; t < tend; ++t) + for (edge t = 1; t < tend; ++t) { - if (is_dead_transition(t)) + if (is_dead_edge(t)) continue; if (t != dest) - transitions_[dest] = std::move(transitions_[t]); + edges_[dest] = std::move(edges_[t]); newidx[t] = dest; ++dest; } - transitions_.resize(dest); - killed_trans_ = 0; + edges_.resize(dest); + killed_edge_ = 0; - // Adjust next_succ and dst pointers in all transitions. - for (transition t = 1; t < dest; ++t) + // Adjust next_succ and dst pointers in all edges. + for (edge t = 1; t < dest; ++t) { - auto& tr = transitions_[t]; + auto& tr = edges_[t]; tr.next_succ = newidx[tr.next_succ]; tr.dst = newst[tr.dst]; tr.src = newst[tr.src]; diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh index 75fea5715..0565c24db 100644 --- a/src/graph/ngraph.hh +++ b/src/graph/ngraph.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. // @@ -36,7 +36,7 @@ namespace spot public: typedef typename Graph::state state; - typedef typename Graph::transition transition; + typedef typename Graph::edge edge; typedef State_Name name; typedef std::unordered_mapsecond; p.first->second = s; // Add the successor of OLD to those of S. - auto& trans = g_.transition_vector(); + auto& trans = g_.edge_vector(); auto& states = g_.states(); trans[states[s].succ_tail].next_succ = states[old].succ; states[s].succ_tail = states[old].succ_tail; states[old].succ = 0; states[old].succ_tail = 0; - // Remove all references to old in transitions: + // Remove all references to old in edges: unsigned tend = trans.size(); for (unsigned t = 1; t < tend; ++t) { @@ -130,35 +130,34 @@ namespace spot } template - transition - new_transition(name src, name dst, Args&&... args) + edge + new_edge(name src, name dst, Args&&... args) { - return g_.new_transition(get_state(src), get_state(dst), - std::forward(args)...); + return g_.new_edge(get_state(src), get_state(dst), + std::forward(args)...); } template - transition - new_transition(name src, - const std::vector& dst, Args&&... args) + edge + new_edge(name src, const std::vector& dst, Args&&... args) { std::vector d; d.reserve(dst.size()); for (auto n: dst) d.push_back(get_state(n)); - return g_.new_transition(get_state(src), d, std::forward(args)...); + return g_.new_edge(get_state(src), d, std::forward(args)...); } template - transition - new_transition(name src, + edge + new_edge(name src, const std::initializer_list& dst, Args&&... args) { std::vector d; d.reserve(dst.size()); for (auto n: dst) d.push_back(get_state(n)); - return g_.new_transition(get_state(src), d, std::forward(args)...); + return g_.new_edge(get_state(src), d, std::forward(args)...); } }; } diff --git a/src/ltlvisit/exclusive.cc b/src/ltlvisit/exclusive.cc index 7e050157e..69f26d8eb 100644 --- a/src/ltlvisit/exclusive.cc +++ b/src/ltlvisit/exclusive.cc @@ -168,7 +168,7 @@ namespace spot bdd support = bddtrue; { std::set bdd_seen; - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) if (bdd_seen.insert(t.cond.id()).second) support &= bdd_support(t.cond); } diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index c45e5cc14..8cb9dc938 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -1021,16 +1021,14 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt "(previous edge is labeled)"); else cond = res.state_label; - res.h->aut->new_transition(res.cur_state, $1, - cond, - $2 | res.acc_state); + res.h->aut->new_edge(res.cur_state, $1, + cond, $2 | res.acc_state); } labeled-edge: trans-label checked-state-num trans-acc_opt { if (res.cur_label != bddfalse) - res.h->aut->new_transition(res.cur_state, $2, - res.cur_label, - $3 | res.acc_state); + res.h->aut->new_edge(res.cur_state, $2, + res.cur_label, $3 | res.acc_state); } | trans-label state-conj-2 trans-acc_opt { @@ -1067,8 +1065,8 @@ unlabeled-edge: checked-state-num trans-acc_opt } } if (cond != bddfalse) - res.h->aut->new_transition(res.cur_state, $1, - cond, $2 | res.acc_state); + res.h->aut->new_edge(res.cur_state, $1, + cond, $2 | res.acc_state); } | state-conj-2 trans-acc_opt { @@ -1097,7 +1095,7 @@ never: "never" { res.namer = res.h->aut->create_namer(); if (res.accept_all_needed && !res.accept_all_seen) { unsigned n = res.namer->new_state("accept_all"); - res.h->aut->new_acc_transition(n, n, bddtrue); + res.h->aut->new_acc_edge(n, n, bddtrue); } // If we aliased existing state, we have some unreachable // states to remove. @@ -1172,7 +1170,7 @@ nc-state: auto acc = !strncmp("accept", $1->c_str(), 6) ? res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U); - res.namer->new_transition(*$1, *$1, bddtrue, acc); + res.namer->new_edge(*$1, *$1, bddtrue, acc); delete $1; } | nc-ident-list { delete $1; } @@ -1185,7 +1183,7 @@ nc-state: { bdd c = bdd_from_int(p.first); bdd_delref(p.first); - res.namer->new_transition(*$1, *p.second, c, acc); + res.namer->new_edge(*$1, *p.second, c, acc); delete p.second; } delete $1; @@ -1445,9 +1443,9 @@ lbtt-transitions: { res.states_map.emplace(dst, dst); } - res.h->aut->new_transition(res.cur_state, dst, - res.cur_label, - res.acc_state | $3); + res.h->aut->new_edge(res.cur_state, dst, + res.cur_label, + res.acc_state | $3); } %% @@ -1563,7 +1561,7 @@ static void fix_acceptance(result_& r) auto onlyneg = r.neg_acc_sets - r.pos_acc_sets; if (onlyneg) { - for (auto& t: r.h->aut->transition_vector()) + for (auto& t: r.h->aut->edge_vector()) t.acc ^= onlyneg; } @@ -1579,7 +1577,7 @@ static void fix_acceptance(result_& r) auto v = acc.sets(both); auto vs = v.size(); base = acc.add_sets(vs); - for (auto& t: r.h->aut->transition_vector()) + for (auto& t: r.h->aut->edge_vector()) if ((t.acc & both) != both) for (unsigned i = 0; i < vs; ++i) if (!t.acc.has(v[i])) @@ -1631,7 +1629,7 @@ static void fix_initial_state(result_& r) // unless one of the actual initial state has no incoming edge. auto& aut = r.h->aut; std::vector has_incoming(aut->num_states(), 0); - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) has_incoming[t.dst] = true; bool found = false; @@ -1649,7 +1647,7 @@ static void fix_initial_state(result_& r) for (auto p: start) if (p != init) for (auto& t: aut->out(p)) - aut->new_transition(init, t.dst, t.cond); + aut->new_edge(init, t.dst, t.cond); } } diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index a2a5b443d..78a94aa49 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -198,7 +198,7 @@ int main(int argc, char* argv[]) auto buchi = spot::degeneralize(a); std::cout << "Buchi: " << buchi->num_states() - << buchi->num_transitions() + << buchi->num_edges() << buchi->acc().num_sets() << std::endl; diff --git a/src/tests/graph.cc b/src/tests/graph.cc index f981e894c..f823497a5 100644 --- a/src/tests/graph.cc +++ b/src/tests/graph.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. // @@ -89,12 +89,12 @@ bool f1() auto s1 = g.new_state(); auto s2 = g.new_state(); auto s3 = g.new_state(); - g.new_transition(s1, s2); - g.new_transition(s1, s3); - g.new_transition(s2, s3); - g.new_transition(s3, s1); - g.new_transition(s3, s2); - g.new_transition(s3, s3); + g.new_edge(s1, s2); + g.new_edge(s1, s3); + g.new_edge(s2, s3); + g.new_edge(s3, s1); + g.new_edge(s3, s2); + g.new_edge(s3, s3); dot(std::cout, g); @@ -118,10 +118,10 @@ bool f2() auto s1 = g.new_state(1); auto s2 = g.new_state(2); auto s3 = g.new_state(3); - g.new_transition(s1, s2); - g.new_transition(s1, s3); - g.new_transition(s2, s3); - g.new_transition(s3, s2); + g.new_edge(s1, s2); + g.new_edge(s1, s3); + g.new_edge(s2, s3); + g.new_edge(s3, s2); dot(std::cout, g); @@ -140,10 +140,10 @@ bool f3() auto s1 = g.new_state(); auto s2 = g.new_state(); auto s3 = g.new_state(); - g.new_transition(s1, s2, 1); - g.new_transition(s1, s3, 2); - g.new_transition(s2, s3, 3); - g.new_transition(s3, s2, 4); + g.new_edge(s1, s2, 1); + g.new_edge(s1, s3, 2); + g.new_edge(s2, s3, 3); + g.new_edge(s3, s2, 4); dot(std::cout, g); @@ -162,10 +162,10 @@ bool f4() auto s1 = g.new_state(2); auto s2 = g.new_state(3); auto s3 = g.new_state(4); - g.new_transition(s1, s2, 1); - g.new_transition(s1, s3, 2); - g.new_transition(s2, s3, 3); - g.new_transition(s3, s2, 4); + g.new_edge(s1, s2, 1); + g.new_edge(s1, s3, 2); + g.new_edge(s2, s3, 3); + g.new_edge(s3, s2, 4); dot(std::cout, g); @@ -184,10 +184,10 @@ bool f5() auto s1 = g.new_state(); auto s2 = g.new_state(); auto s3 = g.new_state(); - g.new_transition(s1, s2, std::make_pair(1, 1.2f)); - g.new_transition(s1, s3, std::make_pair(2, 1.3f)); - g.new_transition(s2, s3, std::make_pair(3, 1.4f)); - g.new_transition(s3, s2, std::make_pair(4, 1.5f)); + g.new_edge(s1, s2, std::make_pair(1, 1.2f)); + g.new_edge(s1, s3, std::make_pair(2, 1.3f)); + g.new_edge(s2, s3, std::make_pair(3, 1.4f)); + g.new_edge(s3, s2, std::make_pair(4, 1.5f)); int f = 0; float h = 0; @@ -206,10 +206,10 @@ bool f6() auto s1 = g.new_state(); auto s2 = g.new_state(); auto s3 = g.new_state(); - g.new_transition(s1, s2, 1, 1.2f); - g.new_transition(s1, s3, 2, 1.3f); - g.new_transition(s2, s3, 3, 1.4f); - g.new_transition(s3, s2, 4, 1.5f); + g.new_edge(s1, s2, 1, 1.2f); + g.new_edge(s1, s3, 2, 1.3f); + g.new_edge(s2, s3, 3, 1.4f); + g.new_edge(s3, s2, 4, 1.5f); int f = 0; float h = 0; @@ -227,10 +227,10 @@ bool f7() auto s1 = g.new_state(2); auto s2 = g.new_state(3); auto s3 = g.new_state(4); - g.new_transition(s1, {s2, s3}, 1); - g.new_transition(s1, {s3}, 2); - g.new_transition(s2, {s3}, 3); - g.new_transition(s3, {s2}, 4); + g.new_edge(s1, {s2, s3}, 1); + g.new_edge(s1, {s3}, 2); + g.new_edge(s2, {s3}, 3); + g.new_edge(s3, {s2}, 4); int f = 0; for (auto& t: g.out(s1)) @@ -273,10 +273,10 @@ bool f8() auto s1 = g.new_state(2, 4); auto s2 = g.new_state(3, 6); auto s3 = g.new_state(4, 8); - g.new_transition(s1, s2, 1, 3); - g.new_transition(s1, s3, 2, 5); - g.new_transition(s2, s3, 3, 7); - g.new_transition(s3, s2, 4, 9); + g.new_edge(s1, s2, 1, 3); + g.new_edge(s1, s3, 2, 5); + g.new_edge(s2, s3, 3, 7); + g.new_edge(s3, s2, 4, 9); dot(std::cout, g); diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc index c84c2700b..20192ddc7 100644 --- a/src/tests/ltl2tgba.cc +++ b/src/tests/ltl2tgba.cc @@ -613,7 +613,7 @@ checked_main(int argc, char** argv) if (spot::format_parse_aut_errors(std::cerr, argv[formula_index] + 2, pel)) return 2; - daut->aut->merge_transitions(); + daut->aut->merge_edges(); system_aut = daut->aut; tm.stop("reading -P's argument"); } @@ -1018,7 +1018,7 @@ checked_main(int argc, char** argv) tm.stop("parsing hoa"); if (spot::format_parse_aut_errors(std::cerr, input, pel)) return 2; - daut->aut->merge_transitions(); + daut->aut->merge_edges(); a = daut->aut; assume_sba = a->is_sba(); } diff --git a/src/tests/ngraph.cc b/src/tests/ngraph.cc index e1fd7da32..d718a9a3b 100644 --- a/src/tests/ngraph.cc +++ b/src/tests/ngraph.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. // @@ -128,12 +128,12 @@ bool f1() auto s1 = gg.new_state("s1"); auto s2 = gg.new_state("s2"); auto s3 = gg.new_state("s3"); - gg.new_transition("s1", "s2"); - gg.new_transition("s1", "s3"); - gg.new_transition("s2", "s3"); - gg.new_transition("s3", "s1"); - gg.new_transition("s3", "s2"); - gg.new_transition("s3", "s3"); + gg.new_edge("s1", "s2"); + gg.new_edge("s1", "s3"); + gg.new_edge("s2", "s3"); + gg.new_edge("s3", "s1"); + gg.new_edge("s3", "s2"); + gg.new_edge("s3", "s3"); dot(std::cout, gg); @@ -158,10 +158,10 @@ bool f2() auto s1 = gg.new_state("s1", 1); gg.new_state("s2", 2); gg.new_state("s3", 3); - gg.new_transition("s1", "s2"); - gg.new_transition("s1", "s3"); - gg.new_transition("s2", "s3"); - gg.new_transition("s3", "s2"); + gg.new_edge("s1", "s2"); + gg.new_edge("s1", "s3"); + gg.new_edge("s2", "s3"); + gg.new_edge("s3", "s2"); dot(std::cout, gg); @@ -181,10 +181,10 @@ bool f3() auto s1 = gg.new_state("s1"); gg.new_state("s2"); gg.new_state("s3"); - gg.new_transition("s1", "s2", 1); - gg.new_transition("s1", "s3", 2); - gg.new_transition("s2", "s3", 3); - gg.new_transition("s3", "s2", 4); + gg.new_edge("s1", "s2", 1); + gg.new_edge("s1", "s3", 2); + gg.new_edge("s2", "s3", 3); + gg.new_edge("s3", "s2", 4); dot(std::cout, gg); @@ -204,10 +204,10 @@ bool f4() auto s1 = gg.new_state("s1", 2); gg.new_state("s2", 3); gg.new_state("s3", 4); - gg.new_transition("s1", "s2", 1); - gg.new_transition("s1", "s3", 2); - gg.new_transition("s2", "s3", 3); - gg.new_transition("s3", "s2", 4); + gg.new_edge("s1", "s2", 1); + gg.new_edge("s1", "s3", 2); + gg.new_edge("s2", "s3", 3); + gg.new_edge("s3", "s2", 4); dot(std::cout, gg); @@ -228,10 +228,10 @@ bool f5() auto s1 = gg.new_state("s1"); gg.new_state("s2"); gg.new_state("s3"); - gg.new_transition("s1", "s2", std::make_pair(1, 1.2f)); - gg.new_transition("s1", "s3", std::make_pair(2, 1.3f)); - gg.new_transition("s2", "s3", std::make_pair(3, 1.4f)); - gg.new_transition("s3", "s2", std::make_pair(4, 1.5f)); + gg.new_edge("s1", "s2", std::make_pair(1, 1.2f)); + gg.new_edge("s1", "s3", std::make_pair(2, 1.3f)); + gg.new_edge("s2", "s3", std::make_pair(3, 1.4f)); + gg.new_edge("s3", "s2", std::make_pair(4, 1.5f)); int f = 0; float h = 0; @@ -252,10 +252,10 @@ bool f6() auto s1 = gg.new_state("s1"); gg.new_state("s2"); gg.new_state("s3"); - gg.new_transition("s1", "s2", 1, 1.2f); - gg.new_transition("s1", "s3", 2, 1.3f); - gg.new_transition("s2", "s3", 3, 1.4f); - gg.new_transition("s3", "s2", 4, 1.5f); + gg.new_edge("s1", "s2", 1, 1.2f); + gg.new_edge("s1", "s3", 2, 1.3f); + gg.new_edge("s2", "s3", 3, 1.4f); + gg.new_edge("s3", "s2", 4, 1.5f); int f = 0; float h = 0; @@ -276,10 +276,10 @@ bool f7() auto s1 = gg.new_state("s1", 2); gg.new_state("s2", 3); gg.new_state("s3", 4); - gg.new_transition("s1", {"s2", "s3"}, 1); - gg.new_transition("s1", {"s3"}, 2); - gg.new_transition("s2", {"s3"}, 3); - gg.new_transition("s3", {"s2"}, 4); + gg.new_edge("s1", {"s2", "s3"}, 1); + gg.new_edge("s1", {"s3"}, 2); + gg.new_edge("s2", {"s3"}, 3); + gg.new_edge("s3", {"s2"}, 4); int f = 0; for (auto& t: g.out(s1)) @@ -324,10 +324,10 @@ bool f8() auto s1 = gg.new_state("s1", 2, 4); gg.new_state("s2", 3, 6); gg.new_state("s3", 4, 8); - gg.new_transition("s1", "s2", 1, 3); - gg.new_transition("s1", "s3", 2, 5); - gg.new_transition("s2", "s3", 3, 7); - gg.new_transition("s3", "s2", 4, 9); + gg.new_edge("s1", "s2", 1, 3); + gg.new_edge("s1", "s3", 2, 5); + gg.new_edge("s2", "s3", 3, 7); + gg.new_edge("s3", "s2", 4, 9); dot(std::cout, gg); @@ -392,10 +392,10 @@ bool f9() auto s3 = gg.new_state("s3"); gg.alias_state(s3, "s3b"); - gg.new_transition("s1", "s2", 1, 3); - gg.new_transition("s1", "s3", 2, 5); - gg.new_transition("s2", "s3b", 3, 7); - gg.new_transition("s3", "s2", 4, 9); + gg.new_edge("s1", "s2", 1, 3); + gg.new_edge("s1", "s3", 2, 5); + gg.new_edge("s2", "s3b", 3, 7); + gg.new_edge("s3", "s2", 4, 9); dot(std::cout, gg); diff --git a/src/tests/twagraph.cc b/src/tests/twagraph.cc index ddea8f195..646ebb12c 100644 --- a/src/tests/twagraph.cc +++ b/src/tests/twagraph.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. // @@ -42,13 +42,13 @@ void f1() auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); - tg->new_transition(s1, s1, bddfalse, 0U); - tg->new_transition(s1, s2, p1, 0U); - tg->new_transition(s1, s3, p2, tg->acc().mark(1)); - tg->new_transition(s2, s3, p1 & p2, tg->acc().mark(0)); - tg->new_transition(s3, s1, p1 | p2, tg->acc().marks({0, 1})); - tg->new_transition(s3, s2, p1 >> p2, 0U); - tg->new_transition(s3, s3, bddtrue, tg->acc().marks({0, 1})); + tg->new_edge(s1, s1, bddfalse, 0U); + tg->new_edge(s1, s2, p1, 0U); + tg->new_edge(s1, s3, p2, tg->acc().mark(1)); + tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); + tg->new_edge(s3, s1, p1 | p2, tg->acc().marks({0, 1})); + tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s3, bddtrue, tg->acc().marks({0, 1})); spot::print_dot(std::cout, tg); @@ -69,19 +69,19 @@ void f1() } auto all = tg->acc().marks({0, 1}); - tg->new_transition(s3, s1, p1 | p2, all); - tg->new_transition(s3, s2, p1 >> p2, 0U); - tg->new_transition(s3, s1, bddtrue, all); + tg->new_edge(s3, s1, p1 | p2, all); + tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s1, bddtrue, all); - std::cerr << tg->num_transitions() << '\n'; - assert(tg->num_transitions() == 7); + std::cerr << tg->num_edges() << '\n'; + assert(tg->num_edges() == 7); spot::print_dot(std::cout, tg); - tg->merge_transitions(); + tg->merge_edges(); spot::print_dot(std::cout, tg); - std::cerr << tg->num_transitions() << '\n'; - assert(tg->num_transitions() == 5); + std::cerr << tg->num_edges() << '\n'; + assert(tg->num_edges() == 5); // Add enough states so that the state vector is reallocated. for (unsigned i = 0; i < 100; ++i) diff --git a/src/twa/twagraph.cc b/src/twa/twagraph.cc index d2ea465b4..b1c8d3697 100644 --- a/src/twa/twagraph.cc +++ b/src/twa/twagraph.cc @@ -53,31 +53,31 @@ namespace spot delete namer; } - void twa_graph::merge_transitions() + void twa_graph::merge_edges() { - g_.remove_dead_transitions_(); + g_.remove_dead_edges_(); - typedef graph_t::trans_storage_t tr_t; - g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) - { - if (lhs.src < rhs.src) - return true; - if (lhs.src > rhs.src) - return false; - if (lhs.dst < rhs.dst) - return true; - if (lhs.dst > rhs.dst) - return false; - return lhs.acc < rhs.acc; - // Do not sort on conditions, we'll merge - // them. - }); + typedef graph_t::edge_storage_t tr_t; + g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) + { + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.dst < rhs.dst) + return true; + if (lhs.dst > rhs.dst) + return false; + return lhs.acc < rhs.acc; + // Do not sort on conditions, we'll merge + // them. + }); - auto& trans = this->transition_vector(); + auto& trans = this->edge_vector(); unsigned tend = trans.size(); unsigned out = 0; unsigned in = 1; - // Skip any leading false transition. + // Skip any leading false edge. while (in < tend && trans[in].cond == bddfalse) ++in; if (in < tend) @@ -87,11 +87,11 @@ namespace spot trans[out] = trans[in]; for (++in; in < tend; ++in) { - if (trans[in].cond == bddfalse) // Unusable transition + if (trans[in].cond == bddfalse) // Unusable edge continue; - // Merge transitions with the same source, destination, and + // Merge edges with the same source, destination, and // acceptance. (We test the source last, because this is the - // most likely test to be true as transitions are ordered by + // most likely test to be true as edges are ordered by // sources and then destinations.) if (trans[out].dst == trans[in].dst && trans[out].acc == trans[in].acc @@ -113,31 +113,31 @@ namespace spot tend = out; out = in = 2; - // FIXME: We could should also merge transitions when using + // FIXME: We could should also merge edges when using // fin_acceptance, but the rule for Fin sets are different than // those for Inf sets, (and we need to be careful if a set is used // both as Inf and Fin) if ((in < tend) && !acc().uses_fin_acceptance()) { - typedef graph_t::trans_storage_t tr_t; - g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) - { - if (lhs.src < rhs.src) - return true; - if (lhs.src > rhs.src) - return false; - if (lhs.dst < rhs.dst) - return true; - if (lhs.dst > rhs.dst) - return false; - return lhs.cond.id() < rhs.cond.id(); - // Do not sort on acceptance, we'll merge - // them. - }); + typedef graph_t::edge_storage_t tr_t; + g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) + { + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.dst < rhs.dst) + return true; + if (lhs.dst > rhs.dst) + return false; + return lhs.cond.id() < rhs.cond.id(); + // Do not sort on acceptance, we'll merge + // them. + }); for (; in < tend; ++in) { - // Merge transitions with the same source, destination, + // Merge edges with the same source, destination, // and conditions. (We test the source last, for the // same reason as above.) if (trans[out].dst == trans[in].dst @@ -157,7 +157,7 @@ namespace spot trans.resize(out); } - g_.chain_transitions_(); + g_.chain_edges_(); } void twa_graph::purge_unreachable_states() @@ -228,7 +228,7 @@ namespace spot order.push_back(src); continue; } - auto& t = g_.trans_storage(tid); + auto& t = g_.edge_storage(tid); todo.back().second = t.next_succ; unsigned dst = t.dst; if (useful[dst] != 1) @@ -246,13 +246,13 @@ namespace spot bool useless = true; while (t) { - // Erase any transition to a useless state. + // Erase any edge to a useless state. if (!useful[t->dst]) { t.erase(); continue; } - // if we have a transition to a useful state, then the + // if we have a edge to a useful state, then the // state is useful. useless = false; ++t; diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh index ed3d43a49..68aa2c02c 100644 --- a/src/twa/twagraph.hh +++ b/src/twa/twagraph.hh @@ -73,22 +73,22 @@ namespace spot } }; - struct SPOT_API twa_graph_trans_data + struct SPOT_API twa_graph_edge_data { bdd cond; acc_cond::mark_t acc; - explicit twa_graph_trans_data() + explicit twa_graph_edge_data() : cond(bddfalse), acc(0) { } - twa_graph_trans_data(bdd cond, acc_cond::mark_t acc = 0U) + twa_graph_edge_data(bdd cond, acc_cond::mark_t acc = 0U) : cond(cond), acc(acc) { } - bool operator<(const twa_graph_trans_data& other) const + bool operator<(const twa_graph_edge_data& other) const { if (cond.id() < other.cond.id()) return true; @@ -97,7 +97,7 @@ namespace spot return acc < other.acc; } - bool operator==(const twa_graph_trans_data& other) const + bool operator==(const twa_graph_edge_data& other) const { return cond.id() == other.cond.id() && acc == other.acc; @@ -110,19 +110,19 @@ namespace spot public twa_succ_iterator { private: - typedef typename Graph::transition transition; + typedef typename Graph::edge edge; typedef typename Graph::state_data_t state; const Graph* g_; - transition t_; - transition p_; + edge t_; + edge p_; public: - twa_graph_succ_iterator(const Graph* g, transition t) + twa_graph_succ_iterator(const Graph* g, edge t) : g_(g), t_(t) { } - virtual void recycle(transition t) + virtual void recycle(edge t) { t_ = t; } @@ -135,7 +135,7 @@ namespace spot virtual bool next() { - p_ = g_->trans_storage(p_).next_succ; + p_ = g_->edge_storage(p_).next_succ; return p_; } @@ -148,22 +148,22 @@ namespace spot { assert(!done()); return const_cast - (&g_->state_data(g_->trans_storage(p_).dst)); + (&g_->state_data(g_->edge_storage(p_).dst)); } virtual bdd current_condition() const { assert(!done()); - return g_->trans_data(p_).cond; + return g_->edge_data(p_).cond; } virtual acc_cond::mark_t current_acceptance_conditions() const { assert(!done()); - return g_->trans_data(p_).acc; + return g_->edge_data(p_).acc; } - transition pos() const + edge pos() const { return p_; } @@ -173,8 +173,8 @@ namespace spot class SPOT_API twa_graph final: public twa { public: - typedef digraph graph_t; - typedef graph_t::trans_storage_t trans_storage_t; + typedef digraph graph_t; + typedef graph_t::edge_storage_t edge_storage_t; protected: graph_t g_; @@ -248,9 +248,9 @@ namespace spot return g_.num_states(); } - unsigned num_transitions() const + unsigned num_edges() const { - return g_.num_transitions(); + return g_.num_edges(); } void set_init_state(graph_t::state s) @@ -323,49 +323,49 @@ namespace spot return format_state(state_number(st)); } - twa_graph_trans_data& trans_data(const twa_succ_iterator* it) + twa_graph_edge_data& edge_data(const twa_succ_iterator* it) { auto* i = down_cast*>(it); - return g_.trans_data(i->pos()); + return g_.edge_data(i->pos()); } - twa_graph_trans_data& trans_data(unsigned t) + twa_graph_edge_data& edge_data(unsigned t) { - return g_.trans_data(t); + return g_.edge_data(t); } - const twa_graph_trans_data& trans_data(const twa_succ_iterator* it) const + const twa_graph_edge_data& edge_data(const twa_succ_iterator* it) const { auto* i = down_cast*>(it); - return g_.trans_data(i->pos()); + return g_.edge_data(i->pos()); } - const twa_graph_trans_data& trans_data(unsigned t) const + const twa_graph_edge_data& edge_data(unsigned t) const { - return g_.trans_data(t); + return g_.edge_data(t); } - trans_storage_t& trans_storage(const twa_succ_iterator* it) + edge_storage_t& edge_storage(const twa_succ_iterator* it) { auto* i = down_cast*>(it); - return g_.trans_storage(i->pos()); + return g_.edge_storage(i->pos()); } - trans_storage_t& trans_storage(unsigned t) + edge_storage_t& edge_storage(unsigned t) { - return g_.trans_storage(t); + return g_.edge_storage(t); } - const trans_storage_t - trans_storage(const twa_succ_iterator* it) const + const edge_storage_t + edge_storage(const twa_succ_iterator* it) const { auto* i = down_cast*>(it); - return g_.trans_storage(i->pos()); + return g_.edge_storage(i->pos()); } - const trans_storage_t trans_storage(unsigned t) const + const edge_storage_t edge_storage(unsigned t) const { - return g_.trans_storage(t); + return g_.edge_storage(t); } unsigned new_state() @@ -378,19 +378,19 @@ namespace spot return g_.new_states(n); } - unsigned new_transition(unsigned src, unsigned dst, + unsigned new_edge(unsigned src, unsigned dst, bdd cond, acc_cond::mark_t acc = 0U) { - return g_.new_transition(src, dst, cond, acc); + return g_.new_edge(src, dst, cond, acc); } - unsigned new_acc_transition(unsigned src, unsigned dst, + unsigned new_acc_edge(unsigned src, unsigned dst, bdd cond, bool acc = true) { if (acc) - return g_.new_transition(src, dst, cond, acc_.all_sets()); + return g_.new_edge(src, dst, cond, acc_.all_sets()); else - return g_.new_transition(src, dst, cond); + return g_.new_edge(src, dst, cond); } #ifndef SWIG @@ -404,18 +404,18 @@ namespace spot auto states() SPOT_RETURN(g_.states()); - auto transitions() const - SPOT_RETURN(g_.transitions()); - auto transitions() - SPOT_RETURN(g_.transitions()); + auto edges() const + SPOT_RETURN(g_.edges()); + auto edges() + SPOT_RETURN(g_.edges()); - auto transition_vector() const - SPOT_RETURN(g_.transition_vector()); - auto transition_vector() - SPOT_RETURN(g_.transition_vector()); + auto edge_vector() const + SPOT_RETURN(g_.edge_vector()); + auto edge_vector() + SPOT_RETURN(g_.edge_vector()); - auto is_dead_transition(const graph_t::trans_storage_t& t) const - SPOT_RETURN(g_.is_dead_transition(t)); + auto is_dead_edge(const graph_t::edge_storage_t& t) const + SPOT_RETURN(g_.is_dead_edge(t)); #endif virtual bdd compute_support_conditions(const state* s) const @@ -426,9 +426,9 @@ namespace spot return sum; } - /// Iterate over all transitions, and merge those with compatible + /// Iterate over all edges, and merge those with compatible /// extremities and acceptance. - void merge_transitions(); + void merge_edges(); /// Remove all states without successors. void purge_dead_states(); @@ -440,7 +440,7 @@ namespace spot { assert(has_state_based_acc() || num_sets() == 0); for (auto& t: g_.out(s)) - // Stop at the first transition, since the remaining should be + // Stop at the first edge, since the remaining should be // labeled identically. return t.acc; return 0U; @@ -450,7 +450,7 @@ namespace spot { assert(has_state_based_acc() || num_sets() == 0); for (auto& t: g_.out(s)) - // Stop at the first transition, since the remaining should be + // Stop at the first edge, since the remaining should be // labeled identically. return acc_.accepting(t.acc); return false; @@ -464,11 +464,11 @@ namespace spot bool operator==(const twa_graph& aut) const { if (num_states() != aut.num_states() || - num_transitions() != aut.num_transitions() || + num_edges() != aut.num_edges() || num_sets() != aut.num_sets()) return false; - auto& trans1 = transition_vector(); - auto& trans2 = aut.transition_vector(); + auto& trans1 = edge_vector(); + auto& trans2 = aut.edge_vector(); return std::equal(trans1.begin() + 1, trans1.end(), trans2.begin() + 1); } diff --git a/src/twa/twamask.hh b/src/twa/twamask.hh index 28fb71727..608fc705b 100644 --- a/src/twa/twamask.hh +++ b/src/twa/twamask.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,8 +33,8 @@ namespace spot /// can optionally be reset to \a init. SPOT_API const_twa_ptr build_twa_mask_keep(const const_twa_ptr& to_mask, - const state_set& to_keep, - const state* init = 0); + const state_set& to_keep, + const state* init = 0); /// \ingroup twa_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting a given set of states. @@ -44,8 +44,8 @@ namespace spot /// \a init. SPOT_API const_twa_ptr build_twa_mask_ignore(const const_twa_ptr& to_mask, - const state_set& to_ignore, - const state* init = 0); + const state_set& to_ignore, + const state* init = 0); /// \ingroup twa_on_the_fly_algorithms @@ -61,6 +61,6 @@ namespace spot /// all_acceptance_conditions(). SPOT_API const_twa_ptr build_twa_mask_acc_ignore(const const_twa_ptr& to_mask, - unsigned to_ignore, - const state* init = 0); + unsigned to_ignore, + const state* init = 0); } diff --git a/src/twaalgos/are_isomorphic.cc b/src/twaalgos/are_isomorphic.cc index a78485803..7a42bac5d 100644 --- a/src/twaalgos/are_isomorphic.cc +++ b/src/twaalgos/are_isomorphic.cc @@ -29,7 +29,7 @@ namespace { - typedef spot::twa_graph::graph_t::trans_storage_t tr_t; + typedef spot::twa_graph::graph_t::edge_storage_t tr_t; bool tr_t_less_than(const tr_t& t1, const tr_t& t2) { @@ -101,7 +101,7 @@ namespace const spot::const_twa_graph_ptr aut2) { return aut1->num_states() != aut2->num_states() || - aut1->num_transitions() != aut2->num_transitions() || + aut1->num_edges() != aut2->num_edges() || // FIXME: At some point, it would be nice to support reordering // of acceptance sets (issue #58). aut1->acc().get_acceptance() != aut2->acc().get_acceptance(); diff --git a/src/twaalgos/are_isomorphic.hh b/src/twaalgos/are_isomorphic.hh index c71445191..f0da226f1 100644 --- a/src/twaalgos/are_isomorphic.hh +++ b/src/twaalgos/are_isomorphic.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -49,6 +49,5 @@ namespace spot twa_graph_ptr ref_; bool ref_deterministic_ = false; unsigned nondet_states_ = 0; - std::vector reftrans_; }; } diff --git a/src/twaalgos/canonicalize.cc b/src/twaalgos/canonicalize.cc index b61f44196..4d9041cef 100644 --- a/src/twaalgos/canonicalize.cc +++ b/src/twaalgos/canonicalize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,13 +24,13 @@ namespace { - typedef std::pair - trans_sig_t; + typedef std::pair + edge_sig_t; struct signature_t { - std::vector ingoing; - std::vector outgoing; + std::vector ingoing; + std::vector outgoing; unsigned classnum; bool @@ -49,7 +49,7 @@ namespace { std::vector signature(aut->num_states(), signature_t()); - for (auto& t : aut->transitions()) + for (auto& t : aut->edges()) { signature[t.dst].ingoing.emplace_back(t.data(), state2class[t.src]); signature[t.src].outgoing.emplace_back(t.data(), state2class[t.dst]); @@ -102,8 +102,8 @@ namespace spot auto& g = aut->get_graph(); g.rename_states_(state2class); aut->set_init_state(state2class[aut->get_init_state_number()]); - g.sort_transitions_(); - g.chain_transitions_(); + g.sort_edges_(); + g.chain_edges_(); return aut; } } diff --git a/src/twaalgos/cleanacc.cc b/src/twaalgos/cleanacc.cc index c89b72802..8ffde1915 100644 --- a/src/twaalgos/cleanacc.cc +++ b/src/twaalgos/cleanacc.cc @@ -31,7 +31,7 @@ namespace spot acc_cond::mark_t used_in_cond = c.used_sets(); acc_cond::mark_t used_in_aut = 0U; - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) used_in_aut |= t.acc; auto useful = used_in_aut & used_in_cond; @@ -42,7 +42,7 @@ namespace spot return aut; // Remove useless marks from the automaton - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) t.acc = t.acc.strip(useless); // Remove useless marks from the acceptance condition diff --git a/src/twaalgos/complete.cc b/src/twaalgos/complete.cc index b65e140be..13e722862 100644 --- a/src/twaalgos/complete.cc +++ b/src/twaalgos/complete.cc @@ -35,7 +35,7 @@ namespace spot // We cannot safely complete an automaton if its // acceptance is always satisfiable. auto acc = aut->set_buchi(); - for (auto& t: aut->transition_vector()) + for (auto& t: aut->edge_vector()) t.acc = acc; } else @@ -67,7 +67,7 @@ namespace spot } } - unsigned t = aut->num_transitions(); + unsigned t = aut->num_edges(); // Now complete all states (excluding any newly added the sink). for (unsigned i = 0; i < n; ++i) @@ -80,39 +80,39 @@ namespace spot // FIXME: This is ugly. // // In case the automaton uses state-based acceptance, we - // need to put the new transition in the same set as all + // need to put the new edge in the same set as all // the other. // - // In case the automaton uses transition-based acceptance, + // In case the automaton uses edge-based acceptance, // it does not matter what acceptance set we put the new - // transition into. + // edge into. // - // So in both cases, we put the transition in the same - // acceptance sets as the last outgoing transition of the + // So in both cases, we put the edge in the same + // acceptance sets as the last outgoing edge of the // state. acc = t.acc; } // If the state has incomplete successors, we need to add a - // transition to some sink state. + // edge to some sink state. if (missingcond != bddfalse) { // If we haven't found any sink, simply add one. if (sink == -1U) { sink = aut->new_state(); - aut->new_transition(sink, sink, bddtrue, um.second); + aut->new_edge(sink, sink, bddtrue, um.second); } // In case the automaton use state-based acceptance, propagate - // the acceptance of the first transition to the one we add. - aut->new_transition(i, sink, missingcond, acc); + // the acceptance of the first edge to the one we add. + aut->new_edge(i, sink, missingcond, acc); } } // Get rid of any named property if the automaton changed. - if (t < aut->num_transitions()) + if (t < aut->num_edges()) aut->release_named_properties(); else - assert(t == aut->num_transitions()); + assert(t == aut->num_edges()); return sink; } diff --git a/src/twaalgos/compsusp.cc b/src/twaalgos/compsusp.cc index 57ceecb4b..2d4821e52 100644 --- a/src/twaalgos/compsusp.cc +++ b/src/twaalgos/compsusp.cc @@ -266,7 +266,7 @@ namespace spot p.second = ris; } - // This loops over all the right transitions + // This loops over all the right edges // if RI is defined. Otherwise this just makes // one iteration as if the right automaton was // looping in state 0 with "true". @@ -277,7 +277,7 @@ namespace spot if (ri) { cond = lc & ri->current_condition(); - // Skip incompatible transitions. + // Skip incompatible edges. if (cond == bddfalse) { ri->next(); @@ -303,7 +303,7 @@ namespace spot acc_cond::mark_t a = res->acc().join(la, li->current_acceptance_conditions(), ra, racc); - res->new_transition(src, dest, bdd_exist(cond, v), a); + res->new_edge(src, dest, bdd_exist(cond, v), a); if (ri) ri->next(); diff --git a/src/twaalgos/cycles.cc b/src/twaalgos/cycles.cc index 74a17560b..e7b2c0c16 100644 --- a/src/twaalgos/cycles.cc +++ b/src/twaalgos/cycles.cc @@ -88,14 +88,14 @@ namespace spot if (cur.succ == 0) cur.succ = aut_->get_graph().state_storage(cur.s).succ; else - cur.succ = aut_->trans_storage(cur.succ).next_succ; + cur.succ = aut_->edge_storage(cur.succ).next_succ; if (cur.succ) { // Explore one successor. // Ignore those that are not on the SCC, or destination // that have been "virtually" deleted from A(v). - unsigned s = aut_->trans_storage(cur.succ).dst; + unsigned s = aut_->edge_storage(cur.succ).dst; if ((sm_.scc_of(s) != scc) || (info_[cur.s].del[s])) continue; diff --git a/src/twaalgos/degen.cc b/src/twaalgos/degen.cc index d4e5b2371..329610e62 100644 --- a/src/twaalgos/degen.cc +++ b/src/twaalgos/degen.cc @@ -55,7 +55,7 @@ namespace spot // Queue of state to be processed. typedef std::deque queue_t; - // Acceptance set common to all outgoing transitions (of the same + // Acceptance set common to all outgoing edges (of the same // SCC -- we do not care about the other) of some state. class outgoing_acc { @@ -75,7 +75,7 @@ namespace spot bool seen = false; for (auto& t: a_->out(s)) { - // Ignore transitions that leave the SCC of s. + // Ignore edges that leave the SCC of s. unsigned d = t.dst; unsigned s2 = sm_ ? sm_->scc_of(d) : 0; if (s2 != s1) @@ -237,10 +237,10 @@ namespace spot // and vice-versa. ds2num_map ds2num; - // This map is used to find transitions that go to the same + // This map is used to find edges that go to the same // destination with the same acceptance. The integer key is // (dest*2+acc) where dest is the destination state number, and - // acc is 1 iff the transition is accepting. The source + // acc is 1 iff the edge is accepting. The source // is always that of the current iteration. typedef std::map tr_cache_t; tr_cache_t tr_cache; @@ -268,7 +268,7 @@ namespace spot if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first)) s.second = order.size(); // Otherwise, check for acceptance conditions common to all - // outgoing transitions, and assume we have already seen these and + // outgoing edges, and assume we have already seen these and // start on the associated level. if (s.second == 0) { @@ -345,12 +345,12 @@ namespace spot { // Ignore the last expected acceptance set (the value of // prev below) if it is common to all other outgoing - // transitions (of the current state) AND if it is not - // used by any outgoing transition of the destination + // edges (of the current state) AND if it is not + // used by any outgoing edge of the destination // state. // // 1) It's correct to do that, because this acceptance - // set is common to other outgoing transitions. + // set is common to other outgoing edges. // Therefore if we make a cycle to this state we // will eventually see that acceptance set thanks // to the "pulling" of the common acceptance sets @@ -360,7 +360,7 @@ namespace spot // degeneralization idempotent (up to a renaming // of states). Consider the following automaton // where 1 is initial and => marks accepting - // transitions: 1=>1, 1=>2, 2->2, 2->1. This is + // edges: 1=>1, 1=>2, 2->2, 2->1. This is // already an SBA, with 1 as accepting state. // However if you try degeralize it without // ignoring *prev, you'll get two copies of state @@ -389,9 +389,9 @@ namespace spot } } } - // A transition in the SLEVEL acceptance set should + // A edge in the SLEVEL acceptance set should // be directed to the next acceptance set. If the - // current transition is also in the next acceptance + // current edge is also in the next acceptance // set, then go to the one after, etc. // // See Denis Oddoux's PhD thesis for a nice @@ -419,7 +419,7 @@ namespace spot { // Complete (or replace) the acceptance sets of // this link with the acceptance sets common to - // all transitions leaving the destination state. + // all edges leaving the destination state. if (s_scc == scc) acc |= otheracc; else @@ -452,7 +452,7 @@ namespace spot { // Consider both the current acceptance // sets, and the acceptance sets common to - // the outgoing transitions of the + // the outgoing edges of the // destination state. But don't do // that if the state is accepting and we // are not skipping levels. @@ -471,12 +471,12 @@ namespace spot } // In case we are building a TBA is_acc has to be - // set differently for each transition, and + // set differently for each edge, and // we do not need to stay use final level. if (!want_sba) { is_acc = d.second == order.size(); - if (is_acc) // The transition is accepting + if (is_acc) // The edge is accepting { d.second = 0; // Make it go to the first level. // Skip levels as much as possible. @@ -526,10 +526,10 @@ namespace spot unsigned& t = tr_cache[dest * 2 + is_acc]; - if (t == 0) // Create transition. - t = res->new_acc_transition(src, dest, i.cond, is_acc); - else // Update existing transition. - res->trans_data(t).cond |= i.cond; + if (t == 0) // Create edge. + t = res->new_acc_edge(src, dest, i.cond, is_acc); + else // Update existing edge. + res->edge_data(t).cond |= i.cond; } tr_cache.clear(); } @@ -546,7 +546,7 @@ namespace spot delete m; - res->merge_transitions(); + res->merge_edges(); return res; } } diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc index 8f4ee374c..21e39577e 100644 --- a/src/twaalgos/dot.cc +++ b/src/twaalgos/dot.cc @@ -427,7 +427,7 @@ namespace spot } void - process_link(const twa_graph::trans_storage_t& t, int number) + process_link(const twa_graph::edge_storage_t& t, int number) { std::string label = bdd_format_formula(aut_->get_dict(), t.cond); os_ << " " << t.src << " -> " << t.dst; diff --git a/src/twaalgos/dtbasat.cc b/src/twaalgos/dtbasat.cc index 6584f2130..861298a2f 100644 --- a/src/twaalgos/dtbasat.cc +++ b/src/twaalgos/dtbasat.cc @@ -302,7 +302,7 @@ namespace spot // Compute the AP used in the hard way. bdd ap = bddtrue; - for (auto& t: ref->transitions()) + for (auto& t: ref->edges()) ap &= bdd_support(t.cond); // Count the number of atomic propositions @@ -679,8 +679,8 @@ namespace spot && acc_states.find(t->second.src) != acc_states.end(); last_aut_trans = - a->new_acc_transition(t->second.src, t->second.dst, - t->second.cond, accept); + a->new_acc_edge(t->second.src, t->second.dst, + t->second.cond, accept); last_sat_trans = &t->second; dout << v << '\t' << t->second << "δ\n"; @@ -697,7 +697,7 @@ namespace spot assert(!state_based); // This assumes that the SAT solvers output // variables in increasing order. - a->trans_data(last_aut_trans).acc = acc; + a->edge_data(last_aut_trans).acc = acc; } else if (state_based) { @@ -733,7 +733,7 @@ namespace spot else dout << -pit.second << "\t¬" << pit.first << "C\n"; #endif - a->merge_transitions(); + a->merge_edges(); return a; } } diff --git a/src/twaalgos/dtgbacomp.cc b/src/twaalgos/dtgbacomp.cc index afe41dfca..8c46482b2 100644 --- a/src/twaalgos/dtgbacomp.cc +++ b/src/twaalgos/dtgbacomp.cc @@ -51,27 +51,27 @@ namespace spot res->new_states(num_sets * n + 1); unsigned sink = res->num_states() - 1; // The sink state has an accepting self-loop. - res->new_acc_transition(sink, sink, bddtrue); + res->new_acc_edge(sink, sink, bddtrue); for (unsigned src = 0; src < n; ++src) { - // Keep track of all conditions on transition leaving state + // Keep track of all conditions on edge leaving state // SRC, so we can complete it. bdd missingcond = bddtrue; for (auto& t: res->out(src)) { - if (t.dst >= n) // Ignore transitions we added. + if (t.dst >= n) // Ignore edges we added. break; missingcond -= t.cond; acc_cond::mark_t curacc = t.acc; - // The original transition must not accept anymore. + // The original edge must not accept anymore. t.acc = 0U; - // Transition that were fully accepting are never cloned. + // Edge that were fully accepting are never cloned. if (oldacc.accepting(curacc)) continue; // Save t.cond and t.dst as the reference to t - // is invalided by calls to new_transition(). + // is invalided by calls to new_edge(). unsigned dst = t.dst; bdd cond = t.cond; @@ -84,30 +84,30 @@ namespace spot add += n; if (!oldacc.has(curacc, set)) { - // Clone the transition - res->new_acc_transition(src + add, dst + add, cond); + // Clone the edge + res->new_acc_edge(src + add, dst + add, cond); assert(dst + add < sink); // Using `t' is disallowed from now on as it is a - // reference to a transition that may have been + // reference to a edge that may have been // reallocated. - // At least one transition per cycle should have a + // At least one edge per cycle should have a // nondeterministic copy from the original clone. // We use state numbers to select it, as any cycle - // is guaranteed to have at least one transition + // is guaranteed to have at least one edge // with dst <= src. FIXME: Computing a feedback // arc set would be better. if (dst <= src) - res->new_transition(src, dst + add, cond); + res->new_edge(src, dst + add, cond); } } assert(add == num_sets * n); } // Complete the original automaton. if (missingcond != bddfalse) - res->new_transition(src, sink, missingcond); + res->new_edge(src, sink, missingcond); } - res->merge_transitions(); + res->merge_edges(); res->purge_dead_states(); return res; } @@ -137,7 +137,7 @@ namespace spot if (si.is_rejecting_scc(scc) && !si.is_trivial(scc)) acc = all_acc; - // Keep track of all conditions on transition leaving state + // Keep track of all conditions on edge leaving state // SRC, so we can complete it. bdd missingcond = bddtrue; for (auto& t: res->out(src)) @@ -151,12 +151,12 @@ namespace spot if (res->num_states() == sink) { res->new_state(); - res->new_acc_transition(sink, sink, bddtrue); + res->new_acc_edge(sink, sink, bddtrue); } - res->new_transition(src, sink, missingcond); + res->new_edge(src, sink, missingcond); } } - //res->merge_transitions(); + //res->merge_edges(); return res; } diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 81096dea9..00cda5d10 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -613,7 +613,7 @@ namespace spot // Compute the AP used in the hard way. bdd ap = bddtrue; - for (auto& t: ref->transitions()) + for (auto& t: ref->edges()) ap &= bdd_support(t.cond); // Count the number of atomic propositions @@ -1033,10 +1033,9 @@ namespace spot acc = i->second; } - last_aut_trans = a->new_transition(t->second.src, - t->second.dst, - t->second.cond, - acc); + last_aut_trans = a->new_edge(t->second.src, + t->second.dst, + t->second.cond, acc); last_sat_trans = &t->second; dout << v << '\t' << t->second << "δ\n"; @@ -1058,7 +1057,7 @@ namespace spot ta->second.dst == last_sat_trans->dst) { assert(!state_based); - auto& v = a->trans_data(last_aut_trans).acc; + auto& v = a->edge_data(last_aut_trans).acc; v |= ta->second.acc; } else if (state_based) @@ -1076,7 +1075,7 @@ namespace spot dout << pit.second << '\t' << pit.first << "C\n"; #endif - a->merge_transitions(); + a->merge_edges(); return a; } } diff --git a/src/twaalgos/dupexp.cc b/src/twaalgos/dupexp.cc index 6f580ce70..8236e517a 100644 --- a/src/twaalgos/dupexp.cc +++ b/src/twaalgos/dupexp.cc @@ -64,7 +64,7 @@ namespace spot const state*, int out, const twa_succ_iterator* si) { - out_->new_transition + out_->new_edge (in - 1, out - 1, si->current_condition(), si->current_acceptance_conditions()); } diff --git a/src/twaalgos/emptiness.cc b/src/twaalgos/emptiness.cc index 0af458d67..6cf6754cc 100644 --- a/src/twaalgos/emptiness.cc +++ b/src/twaalgos/emptiness.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement 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 // et Marie Curie. @@ -369,7 +369,7 @@ namespace spot p.first->second = res->new_state(); dst = p.first->second; - res->new_transition(src, dst, label, acc); + res->new_edge(src, dst, label, acc); src = dst; // Sum acceptance conditions. diff --git a/src/twaalgos/isunamb.cc b/src/twaalgos/isunamb.cc index 1033b049a..5b5f500e9 100644 --- a/src/twaalgos/isunamb.cc +++ b/src/twaalgos/isunamb.cc @@ -33,7 +33,7 @@ namespace spot auto prod = product(clean_a, clean_a); auto clean_p = scc_filter_states(prod); return clean_a->num_states() == clean_p->num_states() - && clean_a->num_transitions() == clean_p->num_transitions(); + && clean_a->num_edges() == clean_p->num_edges(); } bool check_unambiguous(const twa_graph_ptr& aut) diff --git a/src/twaalgos/isweakscc.cc b/src/twaalgos/isweakscc.cc index 4ee43a9a2..c79e0d371 100644 --- a/src/twaalgos/isweakscc.cc +++ b/src/twaalgos/isweakscc.cc @@ -43,7 +43,7 @@ namespace spot acc_cond::mark_t acc = 0U; for (;;) { - acc |= aut_->trans_storage(i->succ).acc; + acc |= aut_->edge_storage(i->succ).acc; if (i->s == start) break; ++i; diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index ef7bbbf48..77806ff24 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -1160,7 +1160,7 @@ namespace spot dest->destroy(); } - namer->new_transition(now, dest, label); + namer->new_edge(now, dest, label); } } @@ -2553,8 +2553,8 @@ namespace spot namer->new_state(t.dest); } - namer->new_transition(now, t.dest, t.cond, - d.bdd_to_mark(t.prom)); + namer->new_edge(now, t.dest, t.cond, + d.bdd_to_mark(t.prom)); if (seen) t.dest->destroy(); } diff --git a/src/twaalgos/mask.hh b/src/twaalgos/mask.hh index a4f444f8a..1628553a7 100644 --- a/src/twaalgos/mask.hh +++ b/src/twaalgos/mask.hh @@ -25,7 +25,7 @@ namespace spot { /// \brief Clone and mask an automaton. /// - /// Copy the transition of the automaton \a old, into the automaton + /// Copy the edge of the automaton \a old, into the automaton /// \a cpy, creating new states at the same time. The argument \a /// trans should behave as a function with the following prototype: /// @@ -33,9 +33,9 @@ namespace spot /// unsigned dst) /// /// It can modify either the condition or the acceptance sets of - /// the transitions. Set the condition to bddfalse to remove it + /// the edges. Set the condition to bddfalse to remove it /// (this will also remove the destination state and its descendants - /// if they are not reachable by another transition). + /// if they are not reachable by another edge). /// \param init The optional new initial state. template @@ -75,14 +75,14 @@ namespace spot trans(t.src, cond, acc, t.dst); if (cond != bddfalse) - cpy->new_transition(new_src, + cpy->new_edge(new_src, new_state(t.dst), cond, acc); } } } - /// \brief Copy an automaton and update each transitions. + /// \brief Copy an automaton and update each edge. /// /// Copy the states of the automaton \a old, into the automaton /// \a cpy. Each state in \a cpy will have the same id as the ones in \a old. @@ -93,7 +93,7 @@ namespace spot /// unsigned dst) /// /// It can modify either the condition or the acceptance sets of - /// the transitions. Set the condition to bddfalse to remove it. Note that + /// the edges. Set the condition to bddfalse to remove it. Note that /// all transtions will be processed. /// \param init The optional new initial state. template @@ -105,7 +105,7 @@ namespace spot cpy->new_states(old->num_states()); cpy->set_init_state(init); - for (auto& t: old->transitions()) + for (auto& t: old->edges()) { bdd cond = t.cond; acc_cond::mark_t acc = t.acc; @@ -114,7 +114,7 @@ namespace spot // equivilent in old and cpy. assert(t.src < cpy->num_states() && t.dst < cpy->num_states()); if (cond != bddfalse) - cpy->new_transition(t.src, t.dst, cond, acc); + cpy->new_edge(t.src, t.dst, cond, acc); } } @@ -133,10 +133,10 @@ namespace spot transform_copy(old, cpy, trans, old->get_init_state_number()); } - /// \brief Remove all transitions that are in some given acceptance sets. + /// \brief Remove all edges that are in some given acceptance sets. SPOT_API twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in, - acc_cond::mark_t to_remove); + acc_cond::mark_t to_remove); /// \brief Keep only the states as specified by \a to_keep. /// @@ -144,6 +144,6 @@ namespace spot /// state. The initial state will be set to \a init. SPOT_API twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in, - std::vector& to_keep, - unsigned int init); + std::vector& to_keep, + unsigned int init); } diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index a53ae4a17..7127f1b39 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -160,11 +160,11 @@ namespace spot dst->destroy(); if (i == state_num.end()) // Ignore useless destinations. continue; - res->new_acc_transition(src_num, i->second, - succit->current_condition(), accepting); + res->new_acc_edge(src_num, i->second, + succit->current_condition(), accepting); } } - res->merge_transitions(); + res->merge_edges(); if (res->num_states() > 0) { const state* init_state = a->get_init_state(); @@ -236,11 +236,11 @@ namespace spot int n; for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i) { - loop_a->new_transition(n - 1, n, i->label); + loop_a->new_edge(n - 1, n, i->label); i->s->destroy(); } assert(i != loop.end()); - loop_a->new_transition(n - 1, 0, i->label); + loop_a->new_edge(n - 1, 0, i->label); i->s->destroy(); assert(++i == loop.end()); diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index 5e8047ee0..6d173496a 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -44,7 +44,7 @@ namespace spot if (a->num_sets() == 0) { auto m = a->set_buchi(); - for (auto& t: a->transitions()) + for (auto& t: a->edges()) t.acc = m; } return a; diff --git a/src/twaalgos/powerset.cc b/src/twaalgos/powerset.cc index ea66f3e84..6a5a4ecb6 100644 --- a/src/twaalgos/powerset.cc +++ b/src/twaalgos/powerset.cc @@ -93,7 +93,7 @@ namespace spot typedef std::set sup_map; sup_map sup; // Record occurrences of all guards - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) sup.emplace(t.cond); for (auto& i: sup) allap &= bdd_support(i); @@ -206,14 +206,14 @@ namespace spot assert(pm.map_.size() == dst_num); pm.map_.emplace_back(std::move(ps)); } - res->new_transition(src_num, dst_num, num2bdd[c]); + res->new_edge(src_num, dst_num, num2bdd[c]); } } for (auto v: toclean) delete v; if (merge) - res->merge_transitions(); + res->merge_edges(); return res; } @@ -232,15 +232,15 @@ namespace spot { public: typedef dfs_stack::const_iterator cycle_iter; - typedef twa_graph_trans_data trans; - typedef std::set trans_set; - typedef std::vector set_set; + typedef twa_graph_edge_data trans; + typedef std::set edge_set; + typedef std::vector set_set; protected: const_twa_graph_ptr ref_; power_map& refmap_; - trans_set reject_; // set of rejecting transitions + edge_set reject_; // set of rejecting edges set_set accept_; // set of cycles that are accepting - trans_set all_; // all non rejecting transitions + edge_set all_; // all non rejecting edges unsigned threshold_; // maximum count of enumerated cycles unsigned cycles_left_; // count of cycles left to explore @@ -277,7 +277,7 @@ namespace spot return threshold_ != 0 && cycles_left_ == 0; } - bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const + bool is_cycle_accepting(cycle_iter begin, edge_set& ts) const { auto a = std::const_pointer_cast(aut_); @@ -289,8 +289,8 @@ namespace spot cycle_iter i; for (n = 1, i = begin; n <= loop_size; ++n, ++i) { - trans* t = &a->trans_data(i->succ); - loop_a->new_transition(n - 1, n % loop_size, t->cond); + trans* t = &a->edge_data(i->succ); + loop_a->new_edge(n - 1, n % loop_size, t->cond); if (reject_.find(t) == reject_.end()) ts.insert(t); } @@ -318,7 +318,7 @@ namespace spot } std::ostream& - print_set(std::ostream& o, const trans_set& s) const + print_set(std::ostream& o, const edge_set& s) const { o << "{ "; for (auto i: s) @@ -333,7 +333,7 @@ namespace spot cycle_iter i = dfs_.begin(); while (i->s != start) ++i; - trans_set ts; + edge_set ts; bool is_acc = is_cycle_accepting(i, ts); do ++i; @@ -387,7 +387,7 @@ namespace spot unsigned threshold_states, unsigned threshold_cycles) { power_map pm; - // Do not merge transitions in the deterministic automaton. If we + // Do not merge edges in the deterministic automaton. If we // add two self-loops labeled by "a" and "!a", we do not want // these to be merged as "1" before the acceptance has been fixed. auto det = tgba_powerset(aut, pm, false); @@ -397,7 +397,7 @@ namespace spot return nullptr; if (fix_dba_acceptance(det, aut, pm, threshold_cycles)) return nullptr; - det->merge_transitions(); + det->merge_edges(); return det; } diff --git a/src/twaalgos/product.cc b/src/twaalgos/product.cc index b4e1b6a01..b9a67c468 100644 --- a/src/twaalgos/product.cc +++ b/src/twaalgos/product.cc @@ -92,9 +92,9 @@ namespace spot if (cond == bddfalse) continue; auto dst = new_state(l.dst, r.dst); - res->new_transition(top.second, dst, cond, - res->acc().join(left->acc(), l.acc, - right->acc(), r.acc)); + res->new_edge(top.second, dst, cond, + res->acc().join(left->acc(), l.acc, + right->acc(), r.acc)); // If right is deterministic, we can abort immediately! } } diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc index aef74af41..30c2b2d3a 100644 --- a/src/twaalgos/randomgraph.cc +++ b/src/twaalgos/randomgraph.cc @@ -40,7 +40,7 @@ namespace spot random_deterministic_labels_rec(std::vector& labels, int *props, int props_n, bdd current, unsigned n) { - if (n > 1 && props_n >= 1) + if (n > 1 && props_n >= 1) { bdd ap = bdd_ithvar(*props); ++props; @@ -184,7 +184,7 @@ namespace spot labels = random_deterministic_labels(props, props_n, nsucc); // if nsucc > 2^props_n, we cannot produce nsucc deterministic - // transitions so we set it to labels.size() + // edges so we set it to labels.size() nsucc = labels.size(); } else @@ -214,7 +214,7 @@ namespace spot std::advance(i, index); // Link it from src. - res->new_transition(src, *i, l, m); + res->new_edge(src, *i, l, m); nodes_to_process.insert(*i); unreachable_nodes.erase(*i); break; @@ -229,7 +229,7 @@ namespace spot state_randomizer[index] = state_randomizer[possibilities]; state_randomizer[possibilities] = dst; - res->new_transition(src, dst, l, m); + res->new_edge(src, dst, l, m); auto j = unreachable_nodes.find(dst); if (j != unreachable_nodes.end()) { diff --git a/src/twaalgos/randomize.cc b/src/twaalgos/randomize.cc index 9e02862ea..bd5497861 100644 --- a/src/twaalgos/randomize.cc +++ b/src/twaalgos/randomize.cc @@ -27,9 +27,9 @@ namespace spot { void randomize(twa_graph_ptr& aut, bool randomize_states, - bool randomize_transitions) + bool randomize_edges) { - if (!randomize_states && !randomize_transitions) + if (!randomize_states && !randomize_edges) return; auto& g = aut->get_graph(); if (randomize_states) @@ -51,16 +51,16 @@ namespace spot aut->set_named_prop("state-names", nn); } } - if (randomize_transitions) + if (randomize_edges) { - g.remove_dead_transitions_(); - auto& v = g.transition_vector(); + g.remove_dead_edges_(); + auto& v = g.edge_vector(); mrandom_shuffle(v.begin() + 1, v.end()); } - typedef twa_graph::graph_t::trans_storage_t tr_t; - g.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) + typedef twa_graph::graph_t::edge_storage_t tr_t; + g.sort_edges_([](const tr_t& lhs, const tr_t& rhs) { return lhs.src < rhs.src; }); - g.chain_transitions_(); + g.chain_edges_(); } } diff --git a/src/twaalgos/randomize.hh b/src/twaalgos/randomize.hh index 548b218d3..c3c1d8083 100644 --- a/src/twaalgos/randomize.hh +++ b/src/twaalgos/randomize.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,10 +25,10 @@ namespace spot { /// \brief Randomize a TGBA /// - /// Make a random permutation of the state, and of the transitions + /// Make a random permutation of the state, and of the edges /// leaving this state. SPOT_API void randomize(twa_graph_ptr& aut, bool randomize_states = true, - bool randomize_transitions = true); + bool randomize_edges = true); } diff --git a/src/twaalgos/relabel.cc b/src/twaalgos/relabel.cc index f69ee624b..00330aa65 100644 --- a/src/twaalgos/relabel.cc +++ b/src/twaalgos/relabel.cc @@ -35,7 +35,7 @@ namespace spot bdd_setpair(pairs, oldv, newv); vars.push_back(oldv); } - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) t.cond = bdd_replace(t.cond, pairs); for (auto v: vars) d->unregister_variable(v, aut); diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index d84b5b9d9..bfafacaa5 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -289,8 +289,7 @@ namespace spot // Create the main copy for (auto s: states) for (auto& t: aut->out(s)) - res->new_transition(s, t.dst, t.cond, - (t.acc & main_sets) | main_add); + res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add); if (si.is_rejecting_scc(n)) continue; @@ -314,17 +313,17 @@ namespace spot if ((t.acc & r) || si.scc_of(t.dst) != n) continue; auto nd = state_map[t.dst]; - res->new_transition(ns, nd, t.cond, (t.acc & k) | a); + res->new_edge(ns, nd, t.cond, (t.acc & k) | a); // We need only one non-deterministic jump per // cycle. As an approximation, we only do // them on back-links. // - // The acceptance marks on these transition + // The acceptance marks on these edge // are useless, but we keep them to preserve // state-based acceptance if any. if (t.dst <= s) - res->new_transition(s, nd, t.cond, - (t.acc & main_sets) | main_add); + res->new_edge(s, nd, t.cond, + (t.acc & main_sets) | main_add); } } } diff --git a/src/twaalgos/safety.cc b/src/twaalgos/safety.cc index 07a5d5e38..c2b5677c4 100644 --- a/src/twaalgos/safety.cc +++ b/src/twaalgos/safety.cc @@ -46,7 +46,7 @@ namespace spot result = false; break; } - // The state should have only one transition that is a + // The state should have only one edge that is a // self-loop labelled by true. auto src = st.front(); auto out = aut->out(src); @@ -69,7 +69,7 @@ namespace spot throw std::runtime_error ("is_safety_mwdba() should be called on a Buchi automaton"); - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) if (!aut->acc().accepting(t.acc)) return false; return true; diff --git a/src/twaalgos/sbacc.cc b/src/twaalgos/sbacc.cc index 158a6b1a3..b1f9e6684 100644 --- a/src/twaalgos/sbacc.cc +++ b/src/twaalgos/sbacc.cc @@ -54,11 +54,11 @@ namespace spot return p.first->second; }; - // Find any transition going into the initial state, and use its + // Find any edge going into the initial state, and use its // acceptance as mark. acc_cond::mark_t init_acc = 0U; unsigned old_init = old->get_init_state_number(); - for (auto& t: old->transitions()) + for (auto& t: old->edges()) if (t.dst == old_init) { init_acc = t.acc; @@ -71,10 +71,10 @@ namespace spot auto one = todo.back(); todo.pop_back(); for (auto& t: old->out(one.first.first)) - res->new_transition(one.second, - new_state(t.dst, t.acc), - t.cond, - one.first.second); + res->new_edge(one.second, + new_state(t.dst, t.acc), + t.cond, + one.first.second); } return res; } diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc index c883996b0..baa16b654 100644 --- a/src/twaalgos/sccfilter.cc +++ b/src/twaalgos/sccfilter.cc @@ -36,7 +36,7 @@ namespace spot // state(src) return true iff s should be kept // trans(src, dst, cond, acc) returns a triplet // (keep, cond2, acc2) where keep is a Boolean stating if the - // transition should be kept, and cond2/acc2 + // edge should be kept, and cond2/acc2 // give replacement values for cond/acc struct id_filter { @@ -57,7 +57,7 @@ namespace spot out->copy_acceptance_of(this->si->get_aut()); } - // Accept all transitions, unmodified + // Accept all edges, unmodified filtered_trans trans(unsigned, unsigned, bdd cond, acc_cond::mark_t acc) { return filtered_trans{true, cond, acc}; @@ -124,7 +124,7 @@ namespace spot } }; - // Remove acceptance conditions from all transitions outside of + // Remove acceptance conditions from all edges outside of // non-accepting SCCs. template struct acc_filter_all: next_filter @@ -145,7 +145,7 @@ namespace spot if (keep) { unsigned u = this->si->scc_of(src); - // If the transition is between two SCCs, or in a + // If the edge is between two SCCs, or in a // non-accepting SCC. Remove the acceptance sets. if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst)) acc = 0U; @@ -155,7 +155,7 @@ namespace spot } }; - // Remove acceptance conditions from all transitions whose + // Remove acceptance conditions from all edges whose // destination is not an accepting SCCs. template struct acc_filter_some: next_filter @@ -296,7 +296,7 @@ namespace spot std::tie(want, cond, acc) = filter.trans(isrc, t.dst, t.cond, t.acc); if (want) - filtered->new_transition(osrc, odst, cond, acc); + filtered->new_edge(osrc, odst, cond, acc); } } if (!given_si) @@ -346,7 +346,7 @@ namespace spot res = scc_filter_apply>>(aut, given_si); } - res->merge_transitions(); + res->merge_edges(); res->prop_copy(aut, { false, // state-based acceptance is not preserved true, @@ -378,7 +378,7 @@ namespace spot suspvars, ignoredvars, early_susp); - res->merge_transitions(); + res->merge_edges(); res->prop_copy(aut, { false, // state-based acceptance is not preserved true, diff --git a/src/twaalgos/sepsets.cc b/src/twaalgos/sepsets.cc index e9d9051c0..a483eb6a4 100644 --- a/src/twaalgos/sepsets.cc +++ b/src/twaalgos/sepsets.cc @@ -84,8 +84,8 @@ namespace spot } } - // Fix the transitions - for (auto& t: aut->transitions()) + // Fix the edges + for (auto& t: aut->edges()) { if ((t.acc & common) == 0U) continue; diff --git a/src/twaalgos/simulation.cc b/src/twaalgos/simulation.cc index 1a04f5147..351a15b84 100644 --- a/src/twaalgos/simulation.cc +++ b/src/twaalgos/simulation.cc @@ -38,12 +38,12 @@ // the format of the acceptance condition, it doesn't allow easy // simplification. Instead of encoding them as: "a!b!c + !ab!c", we // use them as: "ab". We complement them because we want a -// simplification if the condition of the transition A implies the -// transition of B, and if the acceptance condition of A is included +// simplification if the condition of the edge A implies the +// edge of B, and if the acceptance condition of A is included // in the acceptance condition of B. To let the bdd makes the job, we // revert them. -// Then, to check if a transition i-dominates another, we'll use the bdd: +// Then, to check if a edge i-dominates another, we'll use the bdd: // "sig(transA) = cond(trans) & acc(trans) & implied(class(trans->state))" // Idem for sig(transB). The 'implied' // (represented by a hash table 'relation_' in the implementation) is @@ -65,8 +65,8 @@ // 3. Rename the class (to actualize the name in the previous_class and // in relation_). // 4. Building an automaton with the result, with the condition: -// "a transition in the original automaton appears in the simulated one -// iff this transition is included in the set of i-maximal neighbour." +// "a edge in the original automaton appears in the simulated one +// iff this edge is included in the set of i-maximal neighbour." // This function is `build_output'. // The automaton simulated is recomplemented to come back to its initial // state when the object Simulation is destroyed. @@ -96,13 +96,13 @@ namespace spot struct automaton_size { automaton_size() - : transitions(0), + : edges(0), states(0) { } automaton_size(const twa_graph_ptr& a) - : transitions(a->num_transitions()), + : edges(a->num_edges()), states(a->num_states()) { } @@ -110,12 +110,12 @@ namespace spot void set_size(const twa_graph_ptr& a) { states = a->num_states(); - transitions = a->num_transitions(); + edges = a->num_edges(); } inline bool operator!=(const automaton_size& r) { - return transitions != r.transitions || states != r.states; + return edges != r.edges || states != r.states; } inline bool operator<(const automaton_size& r) @@ -125,9 +125,9 @@ namespace spot if (states > r.states) return false; - if (transitions < r.transitions) + if (edges < r.edges) return true; - if (transitions > r.transitions) + if (edges > r.edges) return false; return false; @@ -140,15 +140,15 @@ namespace spot if (states > r.states) return true; - if (transitions < r.transitions) + if (edges < r.edges) return false; - if (transitions > r.transitions) + if (edges > r.edges) return true; return false; } - int transitions; + int edges; int states; }; @@ -207,7 +207,7 @@ namespace spot all_inf_ = all_inf; // Replace all the acceptance conditions by their complements. - // (In the case of Cosimulation, we also flip the transitions.) + // (In the case of Cosimulation, we also flip the edges.) if (Cosimulation) { a_ = make_twa_graph(in->get_dict()); @@ -239,7 +239,7 @@ namespace spot { acc = t.acc ^ all_inf; } - a_->new_transition(t.dst, s, t.cond, acc); + a_->new_edge(t.dst, s, t.cond, acc); } a_->set_init_state(init_state_number); } @@ -247,7 +247,7 @@ namespace spot else { a_ = make_twa_graph(in, twa::prop_set::all()); - for (auto& t: a_->transitions()) + for (auto& t: a_->edges()) t.acc ^= all_inf; } assert(a_->num_states() == size_a_); @@ -309,11 +309,11 @@ namespace spot for (auto& p: bdd_lstate_) { // If the signature of a state is bddfalse (no - // transitions) the class of this state is bddfalse + // edges) the class of this state is bddfalse // instead of an anonymous variable. It allows // simplifications in the signature by removing a - // transition which has as a destination a state with - // no outgoing transition. + // edge which has as a destination a state with + // no outgoing edge. if (p.first == bddfalse) for (auto s: p.second) previous_class_[s] = bddfalse; @@ -360,7 +360,7 @@ namespace spot bdd acc = mark_to_bdd(t.acc); // to_add is a conjunction of the acceptance condition, - // the label of the transition and the class of the + // the label of the edge and the class of the // destination and all the class it implies. bdd to_add = acc & t.cond & relation_[previous_class_[t.dst]]; @@ -426,11 +426,11 @@ namespace spot for (auto& p: bdd_lstate_) { // If the signature of a state is bddfalse (no - // transitions) the class of this state is bddfalse + // edges) the class of this state is bddfalse // instead of an anonymous variable. It allows // simplifications in the signature by removing a - // transition which has as a destination a state with - // no outgoing transition. + // edge which has as a destination a state with + // no outgoing edge. bdd acc = bddfalse; if (p.first != bddfalse) acc = *it_bdd; @@ -511,14 +511,14 @@ namespace spot accst.resize(res->num_states(), 0U); stat.states = bdd_lstate_.size(); - stat.transitions = 0; + stat.edges = 0; unsigned nb_satoneset = 0; unsigned nb_minato = 0; auto all_inf = all_inf_; // For each class, we will create - // all the transitions between the states. + // all the edges between the states. for (auto& p: bdd_lstate_) { // All states in p.second have the same class, so just @@ -565,11 +565,11 @@ namespace spot bdd cond_acc_dest; while ((cond_acc_dest = isop.next()) != bddfalse) { - ++stat.transitions; + ++stat.edges; ++nb_minato; - // Take the transition, and keep only the variable which + // Take the edge, and keep only the variable which // are used to represent the class. bdd dst = bdd_existcomp(cond_acc_dest, all_class_var_); @@ -584,7 +584,7 @@ namespace spot // Because we have complemented all the Inf // acceptance conditions on the input automaton, - // we must revert them to create a new transition. + // we must revert them to create a new edge. acc ^= all_inf; if (Cosimulation) @@ -592,18 +592,18 @@ namespace spot if (Sba) { // acc should be attached to src, or rather, - // in our transition-based representation) - // to all transitions leaving src. As we + // in our edge-based representation) + // to all edges leaving src. As we // can't do this here, store this in a table // so we can fix it later. accst[gb->get_state(src.id())] = acc; acc = 0U; } - gb->new_transition(dst.id(), src.id(), cond, acc); + gb->new_edge(dst.id(), src.id(), cond, acc); } else { - gb->new_transition(src.id(), dst.id(), cond, acc); + gb->new_edge(src.id(), dst.id(), cond, acc); } } } @@ -612,7 +612,7 @@ namespace spot res->set_init_state(gb->get_state(previous_class_ [a_->get_init_state_number()].id())); - res->merge_transitions(); // FIXME: is this really needed? + res->merge_edges(); // FIXME: is this really needed? // Mark all accepting state in a second pass, when // dealing with SBA in cosimulation. diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index e6179e620..99989d4ba 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -286,7 +286,7 @@ namespace spot get_all_ap(const const_twa_graph_ptr& a) { bdd res = bddtrue; - for (auto& i: a->transitions()) + for (auto& i: a->edges()) res &= bdd_support(i.cond); return res; } @@ -360,8 +360,8 @@ namespace spot (void)u; } - // Create the transition. - res->new_transition(src, dest, one, t.acc); + // Create the edge. + res->new_edge(src, dest, one, t.acc); if (src == dest) self_loop_needed = false; @@ -369,9 +369,9 @@ namespace spot } if (self_loop_needed && s.second != bddfalse) - res->new_transition(src, src, s.second, 0U); + res->new_edge(src, src, s.second, 0U); } - res->merge_transitions(); + res->merge_edges(); return res; } @@ -381,18 +381,18 @@ namespace spot if (atomic_propositions == bddfalse) atomic_propositions = get_all_ap(a); unsigned num_states = a->num_states(); - unsigned num_transitions = a->num_transitions(); + unsigned num_edges = a->num_edges(); std::vector selfloops(num_states, bddfalse); std::map, unsigned> newstates; // Record all the conditions for which we can selfloop on each // state. - for (auto& t: a->transitions()) + for (auto& t: a->edges()) if (t.src == t.dst) selfloops[t.src] |= t.cond; - for (unsigned t = 1; t <= num_transitions; ++t) + for (unsigned t = 1; t <= num_edges; ++t) { - auto& td = a->trans_storage(t); - if (a->is_dead_transition(td)) + auto& td = a->edge_storage(t); + if (a->is_dead_edge(td)) continue; unsigned src = td.src; @@ -401,11 +401,11 @@ namespace spot { bdd all = td.cond; // If there is a self-loop with the whole condition on - // either end of the transition, do not bother with it. + // either end of the edge, do not bother with it. if (bdd_implies(all, selfloops[src]) || bdd_implies(all, selfloops[dst])) continue; - // Do not use td in the loop because the new_transition() + // Do not use td in the loop because the new_edge() // might invalidate it. auto acc = td.acc; while (all != bddfalse) @@ -420,13 +420,13 @@ namespace spot if (p.second) p.first->second = a->new_state(); unsigned tmp = p.first->second; // intermediate state - unsigned i = a->new_transition(src, tmp, one, acc); - assert(i > num_transitions); - i = a->new_transition(tmp, tmp, one, 0U); - assert(i > num_transitions); + unsigned i = a->new_edge(src, tmp, one, acc); + assert(i > num_edges); + i = a->new_edge(tmp, tmp, one, 0U); + assert(i > num_edges); // No acceptance here to preserve the state-based property. - i = a->new_transition(tmp, dst, one, 0U); - assert(i > num_transitions); + i = a->new_edge(tmp, dst, one, 0U); + assert(i > num_edges); (void)i; } } @@ -437,7 +437,7 @@ namespace spot false, // deterministic false, // stutter inv. }); - a->merge_transitions(); + a->merge_edges(); return a; } @@ -474,7 +474,7 @@ namespace spot while (!todo.empty()) { - auto t1 = a->trans_storage(todo.back()); + auto t1 = a->edge_storage(todo.back()); todo.pop_back(); for (auto& t2 : a->out(t1.dst)) @@ -486,7 +486,7 @@ namespace spot acc_cond::mark_t acc = t1.acc | t2.acc; for (auto& t: dst2trans[t2.dst]) { - auto& ts = a->trans_storage(t); + auto& ts = a->edge_storage(t); if (acc == ts.acc) { if (!bdd_implies(cond, ts.cond)) @@ -516,9 +516,9 @@ namespace spot if (need_new_trans) { // Load t2.dst first, because t2 can be - // invalidated by new_transition(). + // invalidated by new_edge(). auto dst = t2.dst; - auto i = a->new_transition(state, dst, cond, acc); + auto i = a->new_edge(state, dst, cond, acc); dst2trans[dst].push_back(i); todo.push_back(i); } diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc index 2f1e412b3..d76896d29 100644 --- a/src/twaalgos/totgba.cc +++ b/src/twaalgos/totgba.cc @@ -95,7 +95,7 @@ namespace spot assert(nterms > 0); res->set_generalized_buchi(nterms); - for (auto& t: res->transitions()) + for (auto& t: res->edges()) { acc_cond::mark_t cur_m = t.acc; acc_cond::mark_t new_m = 0U;