From 2fb436a174869bc76e4426f9810c361882765a2c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Oct 2014 18:21:37 +0200 Subject: [PATCH] Replace most uses of scc_map by scc_info. This involves reimplementing some algorithms using tgba_digraph, and implementing an explicit product that takes two tgba_digraphs and produces a tgba_digraph. * src/tgbaalgos/product.cc, src/tgbaalgos/product.hh: New files. * src/tgbaalgos/Makefile.am: Adjust. * src/bin/ltlcross.cc, src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh, src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh, src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Update to use scc_info and/or tgba_digraph. --- src/bin/ltlcross.cc | 85 ++++++------- src/tgba/tgba.cc | 31 +++++ src/tgba/tgba.hh | 14 +++ src/tgba/tgbasafracomplement.cc | 7 +- src/tgba/tgbasafracomplement.hh | 6 +- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/cycles.cc | 7 +- src/tgbaalgos/cycles.hh | 20 ++- src/tgbaalgos/degen.cc | 214 ++++++++++++-------------------- src/tgbaalgos/degen.hh | 4 +- src/tgbaalgos/isweakscc.cc | 46 +++---- src/tgbaalgos/isweakscc.hh | 29 ++--- src/tgbaalgos/minimize.cc | 37 +++--- src/tgbaalgos/minimize.hh | 4 +- src/tgbaalgos/powerset.cc | 23 ++-- src/tgbaalgos/powerset.hh | 7 +- src/tgbaalgos/product.cc | 108 ++++++++++++++++ src/tgbaalgos/product.hh | 45 +++++++ src/tgbaalgos/safety.cc | 67 ++++------ src/tgbaalgos/safety.hh | 14 +-- src/tgbaalgos/sccinfo.cc | 12 +- src/tgbaalgos/sccinfo.hh | 19 ++- src/tgbatest/complementation.cc | 27 ++-- src/tgbatest/emptchk.cc | 2 +- src/tgbatest/ltl2ta.test | 14 +-- src/tgbatest/ltl2tgba.cc | 33 +++-- src/tgbatest/randtgba.cc | 14 +-- 27 files changed, 497 insertions(+), 394 deletions(-) create mode 100644 src/tgbaalgos/product.cc create mode 100644 src/tgbaalgos/product.hh diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 89d63649a..b12747e9f 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -46,12 +46,10 @@ #include "ltlvisit/mutation.hh" #include "ltlvisit/relabel.hh" #include "tgbaalgos/lbtt.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/sccinfo.hh" -#include "tgbaalgos/scc.hh" -#include "tgbaalgos/dotty.hh" #include "tgbaalgos/isweakscc.hh" #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/word.hh" @@ -880,7 +878,7 @@ namespace string_to_tmp(string_ltl_wring, serial, filename_ltl_wring); } - spot::const_tgba_ptr + spot::const_tgba_digraph_ptr translate(unsigned int translator_num, char l, statistics_formula* fstats, bool& problem) { @@ -900,7 +898,7 @@ namespace const char* status_str = 0; - spot::const_tgba_ptr res = 0; + spot::const_tgba_digraph_ptr res = 0; if (timed_out) { // This is not considered to be a global error. @@ -1059,15 +1057,14 @@ namespace st->edges = s.transitions; st->transitions = s.sub_transitions; st->acc = res->acc().num_sets(); - spot::scc_map m(res); - m.build_map(); + spot::scc_info m(res); unsigned c = m.scc_count(); st->scc = c; st->nondetstates = spot::count_nondet_states(res); st->nondeterministic = st->nondetstates != 0; for (unsigned n = 0; n < c; ++n) { - if (!m.accepting(n)) + if (!m.is_accepting_scc(n)) ++st->nonacc_scc; else if (is_terminal_scc(m, n)) ++st->terminal_scc; @@ -1090,8 +1087,8 @@ namespace }; static bool - check_empty_prod(const spot::const_tgba_ptr& aut_i, - const spot::const_tgba_ptr& aut_j, + check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i, + const spot::const_tgba_digraph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { auto prod = spot::product(aut_i, aut_j); @@ -1145,7 +1142,7 @@ namespace } static bool - cross_check(const std::vector& maps, char l, unsigned p) + cross_check(const std::vector& maps, char l, unsigned p) { size_t m = maps.size(); if (verbose) @@ -1167,13 +1164,17 @@ namespace unsigned verified = 0; unsigned violated = 0; for (size_t i = 0; i < m; ++i) - if (spot::scc_map* m = maps[i]) + if (spot::scc_info* m = maps[i]) { // r == true iff the automaton i is accepting. bool r = false; unsigned c = m->scc_count(); - for (unsigned j = 0; (j < c) && !r; ++j) - r |= m->accepting(j); + for (unsigned j = 0; j < c; ++j) + if (m->is_accepting_scc(j)) + { + r = true; + break; + } res[i] = r; if (r) ++verified; @@ -1216,41 +1217,34 @@ namespace return false; } - typedef std::set state_set; + typedef std::set state_set; // Collect all the states of SSPACE that appear in the accepting SCCs - // of PROD. + // of PROD. (Trivial SCCs are considered accepting.) static void - states_in_acc(const spot::scc_map* m, - const spot::const_tgba_ptr& sspace, + states_in_acc(const spot::scc_info* m, state_set& s) { auto aut = m->get_aut(); + auto ps = static_cast + (aut->get_named_prop("product-states")); unsigned c = m->scc_count(); for (unsigned n = 0; n < c; ++n) - if (m->accepting(n)) + if (m->is_accepting_scc(n) || m->is_trivial(n)) for (auto i: m->states_of(n)) - { - spot::state* x = aut->project_state(i, sspace); - assert(x); - if (!s.insert(x).second) - x->destroy(); - } + // Get the projection on sspace. + s.insert((*ps)[i].second); } static bool - consistency_check(const spot::scc_map* pos, const spot::scc_map* neg, - const spot::const_tgba_ptr& sspace) + consistency_check(const spot::scc_info* pos, const spot::scc_info* neg) { // the states of SSPACE should appear in the accepting SCC of at // least one of POS or NEG. Maybe both. state_set s; - states_in_acc(pos, sspace, s); - states_in_acc(neg, sspace, s); - bool res = s.size() == states; - for (auto i: s) - i->destroy(); - return res; + states_in_acc(pos, s); + states_in_acc(neg, s); + return s.size() == states; } typedef @@ -1423,12 +1417,12 @@ namespace // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); - std::vector pos(m); - std::vector neg(m); + std::vector pos(m); + std::vector neg(m); // These store the complement of the above results, when we can // compute it easily. - std::vector comp_pos(m); - std::vector comp_neg(m); + std::vector comp_pos(m); + std::vector comp_neg(m); unsigned n = vstats.size(); @@ -1577,19 +1571,18 @@ namespace auto statespace = spot::random_graph(states, density, ap, dict); // Products of the state space with the positive automata. - std::vector pos_prod(m); + std::vector pos_prod(m); // Products of the state space with the negative automata. - std::vector neg_prod(m); + std::vector neg_prod(m); // Associated SCC maps. - std::vector pos_map(m); - std::vector neg_map(m); + std::vector pos_map(m); + std::vector neg_map(m); for (size_t i = 0; i < m; ++i) if (pos[i]) { auto p = spot::product(pos[i], statespace); pos_prod[i] = p; - spot::scc_map* sm = new spot::scc_map(p); - sm->build_map(); + auto sm = new spot::scc_info(p); pos_map[i] = sm; // Statistics @@ -1608,8 +1601,7 @@ namespace { auto p = spot::product(neg[i], statespace); neg_prod[i] = p; - spot::scc_map* sm = new spot::scc_map(p); - sm->build_map(); + auto sm = new spot::scc_info(p); neg_map[i] = sm; // Statistics @@ -1636,8 +1628,7 @@ namespace std::cerr << "info: consistency_check (P" << i << ",N" << i << "), state-space #" << p << '/' << products << '\n'; - if (!(consistency_check(pos_map[i], neg_map[i], - statespace))) + if (!(consistency_check(pos_map[i], neg_map[i]))) { ++problems; diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 310e6ebf1..6511f8c4c 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -22,6 +22,7 @@ #include "tgba.hh" #include "tgbaalgos/gtec/gtec.hh" +#include namespace spot { @@ -38,6 +39,10 @@ namespace spot if (last_support_conditions_input_) last_support_conditions_input_->destroy(); delete iter_cache_; + + // Destroy all named properties. + for (auto& np: named_prop_) + np.second.second(np.second.first); } bdd @@ -78,4 +83,30 @@ namespace spot return !couvreur99(shared_from_this())->check(); } + void + tgba::set_named_prop(std::string s, + void* val, std::function destructor) + { + auto p = named_prop_.emplace(std::piecewise_construct, + std::forward_as_tuple(s), + std::forward_as_tuple(val, destructor)); + if (!p.second) + { + p.first->second.second(p.first->second.first); + p.first->second = std::make_pair(val, destructor); + } + } + + void* + tgba::get_named_prop(std::string s) const + { + auto i = named_prop_.find(s); + if (i == named_prop_.end()) + return nullptr; + return i->second.first; + } + + + + } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 19d840681..72091ab18 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -27,6 +27,8 @@ #include "acc.hh" #include #include +#include +#include #include "misc/casts.hh" #include "misc/hash.hh" @@ -657,8 +659,20 @@ namespace spot bprop is; }; +#ifndef SWIG + // Dynamic properties, are given with a name and a destructor function. + std::unordered_map>> named_prop_; +#endif public: +#ifndef SWIG + void set_named_prop(std::string s, + void* val, std::function destructor); + void* get_named_prop(std::string s) const; +#endif + bool has_single_acc_set() const { return is.single_acc_set; diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index bf495204a..e92f7bfdb 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -570,7 +570,7 @@ namespace spot { public: static safra_tree_automaton* - create_safra_automaton(const const_tgba_ptr& a); + create_safra_automaton(const const_tgba_digraph_ptr& a); private: typedef std::set atomic_list_t; typedef std::set conjunction_list_t; @@ -585,7 +585,8 @@ namespace spot /// \brief The body of Safra's construction. safra_tree_automaton* - safra_determinisation::create_safra_automaton(const const_tgba_ptr& a) + safra_determinisation::create_safra_automaton + (const const_tgba_digraph_ptr& a) { // initialization. auto sba_aut = degeneralize(a); @@ -1074,7 +1075,7 @@ namespace spot // tgba_safra_complement ////////////////////////// - tgba_safra_complement::tgba_safra_complement(const const_tgba_ptr& a) + tgba_safra_complement::tgba_safra_complement(const const_tgba_digraph_ptr& a) : tgba(a->get_dict()), automaton_(a), safra_(safra_determinisation::create_safra_automaton(a)) { diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 93c33aad2..2e8682d01 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -50,7 +50,7 @@ namespace spot class SPOT_API tgba_safra_complement : public tgba { public: - tgba_safra_complement(const const_tgba_ptr& a); + tgba_safra_complement(const const_tgba_digraph_ptr& a); virtual ~tgba_safra_complement(); // tgba interface. @@ -67,7 +67,7 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; private: - const_tgba_ptr automaton_; + const_tgba_digraph_ptr automaton_; void* safra_; #if TRANSFORM_TO_TBA acc_cond::mark_t the_acceptance_cond_; @@ -82,7 +82,7 @@ namespace spot typedef std::shared_ptr const_tgba_safra_complement_ptr; inline tgba_safra_complement_ptr - make_safra_complement(const const_tgba_ptr& a) + make_safra_complement(const const_tgba_digraph_ptr& a) { return std::make_shared(a); } diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index e31120b86..095334fb4 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -53,6 +53,7 @@ tgbaalgos_HEADERS = \ neverclaim.hh \ postproc.hh \ powerset.hh \ + product.hh \ projrun.hh \ randomgraph.hh \ reachiter.hh \ @@ -100,6 +101,7 @@ libtgbaalgos_la_SOURCES = \ neverclaim.cc \ postproc.cc \ powerset.cc \ + product.cc \ projrun.cc \ randomgraph.cc \ reachiter.cc \ diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index c9e692d9a..df408d6cb 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -22,7 +22,7 @@ namespace spot { - enumerate_cycles::enumerate_cycles(const scc_map& map) + enumerate_cycles::enumerate_cycles(const scc_info& map) : aut_(map.get_aut()), sm_(map) { } @@ -84,12 +84,13 @@ namespace spot dfs_.push_back(e); } + // FIXME: Recode this algorithm using unsigned states. void enumerate_cycles::run(unsigned scc) { bool keep_going = true; - push_state(tag_state(sm_.one_state_of(scc)->clone())); + push_state(tag_state(aut_->state_from_number(sm_.one_state_of(scc)))); while (keep_going && !dfs_.empty()) { @@ -109,7 +110,7 @@ namespace spot // Ignore those that are not on the SCC, or destination // that have been "virtually" deleted from A(v). state* s = cur.succ->current_state(); - if ((sm_.scc_of_state(s) != scc) + if ((sm_.scc_of(aut_->state_number(s)) != scc) || (cur.ts->second.del.find(s) != cur.ts->second.del.end())) { s->destroy(); diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index c72158c47..387c65833 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -20,7 +20,7 @@ #ifndef SPOT_TGBAALGOS_CYCLES_HH # define SPOT_TGBAALGOS_CYCLES_HH -#include "scc.hh" +#include "sccinfo.hh" #include "misc/hash.hh" #include @@ -62,13 +62,11 @@ namespace spot /// dfs_ stack. Only the last portion of this stack may form a /// cycle. /// - /// The class constructor takes an scc_map that should already have - /// been built for its automaton. Calling run(n) will - /// enumerate all elementary cycles in SCC n. Each - /// time an SCC is found, the method cycle_found(s) is called with - /// the initial state s of the cycle: the cycle is constituted from - /// all the states that are on the \c dfs_ stack after \c s - /// (including \c s). + /// Calling run(n) will enumerate all elementary cycles + /// in SCC n. Each time an SCC is found, the method + /// cycle_found(s) is called with the initial state s of the cycle: + /// the cycle is constituted from all the states that are on the \c + /// dfs_ stack after \c s (including \c s). /// /// You should inherit from this class and redefine the /// cycle_found() method to perform any work you would like to do on @@ -112,9 +110,9 @@ namespace spot typedef hash_type::iterator tagged_state; // The automaton we are working on. - const_tgba_ptr aut_; + const_tgba_digraph_ptr aut_; // The SCC map built for aut_. - const scc_map& sm_; + const scc_info& sm_; // The DFS stack. Each entry contains a tagged state, an iterator // on the transitions leaving that state, and a Boolean f @@ -131,7 +129,7 @@ namespace spot dfs_stack dfs_; public: - enumerate_cycles(const scc_map& map); + enumerate_cycles(const scc_info& map); virtual ~enumerate_cycles() {} /// \brief Run in SCC scc, and call \a cycle_found() for any new diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index ebc7e1c1b..2b31cc45b 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -26,7 +26,7 @@ #include #include #include -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgba/bddprint.hh" //#define DEGEN_DEBUG @@ -38,32 +38,19 @@ namespace spot // A state in the degenalized automaton corresponds to a state in // the TGBA associated to a level. The level is just an index in // the list of acceptance sets. - typedef std::pair degen_state; + typedef std::pair degen_state; struct degen_state_hash { size_t operator()(const degen_state& s) const { - return s.first->hash() & wang32_hash(s.second); - } - }; - - struct degen_state_equal - { - bool - operator()(const degen_state& left, - const degen_state& right) const - { - if (left.second != right.second) - return false; - return left.first->compare(right.first) == 0; + return wang32_hash(s.first ^ wang32_hash(s.second)); } }; // Associate the degeneralized state to its number. - typedef std::unordered_map ds2num_map; + typedef std::unordered_map ds2num_map; // Queue of state to be processed. typedef std::deque queue_t; @@ -72,96 +59,64 @@ namespace spot // SCC -- we do not care about the other) of some state. class outgoing_acc { - const_tgba_ptr a_; - typedef std::pair cache_entry; - typedef std::unordered_map cache_t; - cache_t cache_; - const scc_map* sm_; + const_tgba_digraph_ptr a_; + typedef std::tuple cache_entry; + std::vector cache_; + const scc_info* sm_; - public: - outgoing_acc(const const_tgba_ptr& a, const scc_map* sm): a_(a), sm_(sm) + void fill_cache(unsigned s) { - } - - cache_t::const_iterator fill_cache(const state* s) - { - unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0; + unsigned s1 = sm_ ? sm_->scc_of(s) : 0; acc_cond::mark_t common = a_->acc().all_sets(); acc_cond::mark_t union_ = 0U; - for (auto it: a_->succ(s)) + bool has_acc_self_loop = false; + for (auto& t: a_->out(s)) { // Ignore transitions that leave the SCC of s. - const state* d = it->current_state(); - unsigned s2 = sm_ ? sm_->scc_of_state(d) : 0; - d->destroy(); + unsigned d = t.dst; + unsigned s2 = sm_ ? sm_->scc_of(d) : 0; if (s2 != s1) continue; - acc_cond::mark_t set = it->current_acceptance_conditions(); - common &= set; - union_ |= set; + common &= t.acc; + union_ |= t.acc; + + // an accepting self-loop? + has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc); } - cache_entry e(common, union_); - return cache_.emplace(s, e).first; + cache_[s] = std::make_tuple(common, union_, has_acc_self_loop); + } + + public: + outgoing_acc(const const_tgba_digraph_ptr& a, const scc_info* sm): + a_(a), cache_(a->num_states()), sm_(sm) + { + unsigned n = a->num_states(); + for (unsigned s = 0; s < n; ++s) + fill_cache(s); } // Intersection of all outgoing acceptance sets - acc_cond::mark_t common_acc(const state* s) + acc_cond::mark_t common_acc(unsigned s) { - cache_t::const_iterator i = cache_.find(s); - if (i == cache_.end()) - i = fill_cache(s); - return i->second.first; + assert(s < cache_.size()); + return std::get<0>(cache_[s]); } // Union of all outgoing acceptance sets - acc_cond::mark_t union_acc(const state* s) - { - cache_t::const_iterator i = cache_.find(s); - if (i == cache_.end()) - i = fill_cache(s); - return i->second.second; - } - }; - - - // Check whether a state has an accepting self-loop, with a catch. - class has_acc_loop - { - const_tgba_ptr a_; - typedef std::unordered_map cache_t; - cache_t cache_; - state_unicity_table& uniq_; - - public: - has_acc_loop(const const_tgba_ptr& a, state_unicity_table& uniq): - a_(a), - uniq_(uniq) + acc_cond::mark_t union_acc(unsigned s) { + assert(s < cache_.size()); + return std::get<1>(cache_[s]); } - bool check(const state* s) + // Has an accepting self-loop + bool has_acc_selfloop(unsigned s) { - auto p = cache_.emplace(s, false); - if (p.second) - { - for (auto it: a_->succ(s)) - { - // Look only for transitions that are accepting. - if (!a_->acc().accepting(it->current_acceptance_conditions())) - continue; - // Look only for self-loops. - const state* dest = uniq_(it->current_state()); - if (dest == s) - { - p.first->second = true; - break; - } - } - } - return p.first->second; + assert(s < cache_.size()); + return std::get<2>(cache_[s]); } }; @@ -196,7 +151,6 @@ namespace spot void print(int scc) { - std::vector::iterator i; std::cout << "Order_" << scc << ":\t"; for (auto i: order_) std::cout << i << ", "; @@ -234,7 +188,7 @@ namespace spot template tgba_digraph_ptr - degeneralize_aux(const const_tgba_ptr& a, bool use_z_lvl, + degeneralize_aux(const const_tgba_digraph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels) { @@ -274,14 +228,6 @@ namespace spot // Initialize scc_orders scc_orders orders(a->acc(), skip_levels); - // Make sure we always use the same pointer for identical states - // from the input automaton. - state_unicity_table uniq; - - // Accepting loop checker, for some heuristics. - has_acc_loop acc_loop(a, uniq); - - // These maps make it possible to convert degen_state to number // and vice-versa. ds2num_map ds2num; @@ -293,27 +239,27 @@ namespace spot typedef std::map tr_cache_t; tr_cache_t tr_cache; - // State level cache - typedef std::map lvl_cache_t; - lvl_cache_t lvl_cache; + // Read this early, because it might create a state if the + // automaton is empty. + degen_state s(a->get_init_state_number(), 0); + + // State->level cache + std::vector> lvl_cache(a->num_states()); // Compute SCCs in order to use any optimization. - scc_map m(a); + scc_info* m = nullptr; if (use_scc) - m.build_map(); + m = new scc_info(a); // Cache for common outgoing acceptances. - outgoing_acc outgoing(a, use_scc ? &m : 0); + outgoing_acc outgoing(a, m); queue_t todo; - const state* s0 = uniq(a->get_init_state()); - degen_state s(s0, 0); - // As a heuristic for building SBA, if the initial state has at // least one accepting self-loop, start the degeneralization on // the accepting level. - if (want_sba && acc_loop.check(s0)) + if (want_sba && 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 @@ -322,7 +268,7 @@ namespace spot { auto set = outgoing.common_acc(s.first); if (use_cust_acc_orders) - s.second = orders.next_level(m.initial(), s.second, set); + s.second = orders.next_level(m->initial(), s.second, set); else while (s.second < order.size() && set.has(order[s.second])) @@ -345,7 +291,7 @@ namespace spot // If such state exists level from chache is used. // If not, a new level (starting with 0) is computed. if (use_lvl_cache) - lvl_cache[s.first] = s.second; + lvl_cache[s.first] = std::make_pair(s.second, true); while (!todo.empty()) { @@ -363,19 +309,19 @@ namespace spot // Check SCC for state s int s_scc = -1; if (use_scc) - s_scc = m.scc_of_state(s.first); + s_scc = m->scc_of(s.first); - for (auto i: a->succ(s.first)) + for (auto& i: a->out(s.first)) { - degen_state d(uniq(i->current_state()), 0); + degen_state d(i.dst, 0); // Check whether the target SCC is accepting bool is_scc_acc; int scc; if (use_scc) { - scc = m.scc_of_state(d.first); - is_scc_acc = m.accepting(scc); + scc = m->scc_of(d.first); + is_scc_acc = m->is_accepting_scc(scc); } else { @@ -386,7 +332,7 @@ namespace spot } // The old level is slevel. What should be the new one? - auto acc = i->current_acceptance_conditions(); + auto acc = i.acc; auto otheracc = outgoing.common_acc(d.first); if (want_sba && is_acc) @@ -459,9 +405,9 @@ namespace spot // If lvl_cache is used and switching SCCs, use level // from cache if (use_lvl_cache && s_scc != scc - && lvl_cache.find(d.first) != lvl_cache.end()) + && lvl_cache[d.first].second) { - d.second = lvl_cache[d.first]; + d.second = lvl_cache[d.first].first; } else { @@ -490,7 +436,8 @@ namespace spot // state that has at least one accepting // self-loop, start the degeneralization on // the accepting level. - if (s_scc != scc && acc_loop.check(d.first)) + if (s_scc != scc + && outgoing.has_acc_selfloop(d.first)) { d.second = order.size(); } @@ -558,50 +505,47 @@ namespace spot if (use_lvl_cache) { - auto res = lvl_cache.emplace(d.first, d.second); - - if (!res.second) + auto lvl = d.second; + if (lvl_cache[d.first].second) { if (use_lvl_cache == 3) - res.first->second = - std::max(res.first->second, d.second); + lvl = std::max(lvl_cache[d.first].first, lvl); else if (use_lvl_cache == 2) - res.first->second = - std::min(res.first->second, d.second); + lvl = std::min(lvl_cache[d.first].first, lvl); } + lvl_cache[d.first] = std::make_pair(lvl, true); } } unsigned& t = tr_cache[dest * 2 + is_acc]; if (t == 0) // Create transition. - t = res->new_acc_transition(src, dest, - i->current_condition(), is_acc); + t = res->new_acc_transition(src, dest, i.cond, is_acc); else // Update existing transition. - res->trans_data(t).cond |= i->current_condition(); + res->trans_data(t).cond |= i.cond; } tr_cache.clear(); } #ifdef DEGEN_DEBUG - std::vector::iterator i; std::cout << "Orig. order: \t"; - for (i = order.begin(); i != order.end(); i++) + for (auto i: order) { - bdd_print_acc(std::cout, dict, *i); - std::cout << ", "; + std::cout << i << ", "; } - std::cout << std::endl; - orders.print(dict); + std::cout << '\n'; + orders.print(); #endif + delete m; + res->merge_transitions(); return res; } } tgba_digraph_ptr - degeneralize(const const_tgba_ptr& a, + degeneralize(const const_tgba_digraph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels) { @@ -616,7 +560,7 @@ namespace spot } tgba_digraph_ptr - degeneralize_tba(const const_tgba_ptr& a, + degeneralize_tba(const const_tgba_digraph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels) { diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 75808b238..2804fa601 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -49,13 +49,13 @@ namespace spot /// with transition-based acceptance. /// \@{ SPOT_API tgba_digraph_ptr - degeneralize(const const_tgba_ptr& a, bool use_z_lvl = true, + degeneralize(const const_tgba_digraph_ptr& a, bool use_z_lvl = true, bool use_cust_acc_orders = false, int use_lvl_cache = 1, bool skip_levels = true); SPOT_API tgba_digraph_ptr - degeneralize_tba(const const_tgba_ptr& a, bool use_z_lvl = true, + degeneralize_tba(const const_tgba_digraph_ptr& a, bool use_z_lvl = true, bool use_cust_acc_orders = false, int use_lvl_cache = 1, bool skip_levels = true); diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index f4c7dfa7e..63f609963 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -31,7 +31,7 @@ namespace spot public: bool result; - weak_checker(const scc_map& map) + weak_checker(const scc_info& map) : enumerate_cycles(map), result(true) { } @@ -65,10 +65,10 @@ namespace spot } bool - is_inherently_weak_scc(scc_map& map, unsigned scc) + is_inherently_weak_scc(scc_info& map, unsigned scc) { // If no cycle is accepting, the SCC is weak. - if (!map.accepting(scc)) + if (!map.is_accepting_scc(scc)) return true; // If the SCC is accepting, but one cycle is not, the SCC is not // weak. @@ -78,57 +78,43 @@ namespace spot } bool - is_weak_scc(scc_map& map, unsigned scc) + is_weak_scc(scc_info& map, unsigned scc) { // If no cycle is accepting, the SCC is weak. - if (!map.accepting(scc)) + if (!map.is_accepting_scc(scc)) return true; // If all transitions use the same acceptance set, the SCC is weak. - return map.useful_acc_of(scc).size() == 1; + return map.used_acc_of(scc).size() == 1; } bool - is_complete_scc(scc_map& map, unsigned scc) + is_complete_scc(scc_info& map, unsigned scc) { auto a = map.get_aut(); for (auto s: map.states_of(scc)) { - tgba_succ_iterator* it = a->succ_iter(s); - - // If a state has no successors, the SCC is not complete. - if (!it->first()) - { - a->release_iter(it); - return false; - } - - // Sum guards on all outgoing transitions. + bool has_succ = false; bdd sumall = bddfalse; - do + for (auto& t: a->out(s)) { - const state *next = it->current_state(); - // check it's the same scc - if (map.scc_of_state(next) == scc) - sumall |= it->current_condition(); - next->destroy(); + has_succ = true; + if (map.scc_of(t.dst) == scc) + sumall |= t.cond; if (sumall == bddtrue) break; } - while (it->next()); - a->release_iter(it); - - if (sumall != bddtrue) + if (!has_succ || sumall != bddtrue) return false; } return true; } bool - is_terminal_scc(scc_map& map, unsigned scc) + is_terminal_scc(scc_info& map, unsigned scc) { // If all transitions use all acceptance conditions, the SCC is weak. - return (map.accepting(scc) - && map.useful_acc_of(scc).size() == 1 + return (map.is_accepting_scc(scc) + && map.used_acc_of(scc).size() == 1 && is_complete_scc(map, scc)); } } diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index 3f7efbb27..85366de2b 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -20,7 +20,7 @@ #ifndef SPOT_TGBAALGOS_ISWEAKSCC_HH # define SPOT_TGBAALGOS_ISWEAKSCC_HH -#include "scc.hh" +#include "sccinfo.hh" namespace spot { @@ -36,15 +36,14 @@ namespace spot /// Note the terminal SCCs are also inherently weak with that /// definition. /// - /// The scc_map \a map should have been built already. The absence - /// of accepting cycle is easy to check (the scc_map can tell - /// whether the SCC is non-accepting already). Similarly, an SCC in - /// which all transitions belong to all acceptance sets is - /// necessarily weak. - /// For other accepting SCCs, this function enumerates all cycles in - /// the given SCC (it stops if it find a non-accepting cycle). + /// The absence of accepting cycle is easy to check (the scc_info + /// object can tell whether the SCC is non-accepting already). + /// Similarly, an SCC in which all transitions belong to all + /// acceptance sets is necessarily weak. For other accepting SCCs, + /// this function enumerates all cycles in the given SCC (it stops + /// if it find a non-accepting cycle). SPOT_API bool - is_inherently_weak_scc(scc_map& map, unsigned scc); + is_inherently_weak_scc(scc_info& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is weak. /// @@ -52,27 +51,21 @@ namespace spot /// are fully accepting (i.e., the belong to all acceptance sets). /// /// Note that terminal SCCs are also weak with that definition. - /// - /// The scc_map \a map should have been built already. SPOT_API bool - is_weak_scc(scc_map& map, unsigned scc); + is_weak_scc(scc_info& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is complete. /// /// An SCC is complete iff for all states and all label there exists /// a transition that stays into this SCC. - /// - /// The scc_map \a map should have been built already. SPOT_API bool - is_complete_scc(scc_map& map, unsigned scc); + is_complete_scc(scc_info& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is terminal. /// /// An SCC is terminal if it is weak, complete, and accepting. - /// - /// The scc_map \a map should have been built already. SPOT_API bool - is_terminal_scc(scc_map& map, unsigned scc); + is_terminal_scc(scc_info& map, unsigned scc); /// @} } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 04ea469af..22e73761b 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -41,7 +41,7 @@ #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/safety.hh" #include "tgbaalgos/sccfilter.hh" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/bfssteps.hh" #include "tgbaalgos/isdet.hh" @@ -183,7 +183,7 @@ namespace spot struct wdba_search_acc_loop : public bfs_steps { wdba_search_acc_loop(const const_tgba_ptr& det_a, - unsigned scc_n, scc_map& sm, + unsigned scc_n, scc_info& sm, power_map& pm, const state* dest) : bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest) { @@ -194,7 +194,8 @@ namespace spot filter(const state* s) { s = seen(s); - if (sm.scc_of_state(s) != scc_n) + if (sm.scc_of(std::static_pointer_cast(a_) + ->state_number(s)) != scc_n) return 0; return s; } @@ -206,7 +207,7 @@ namespace spot } unsigned scc_n; - scc_map& sm; + scc_info& sm; power_map& pm; const state* dest; state_unicity_table seen; @@ -215,12 +216,12 @@ namespace spot bool wdba_scc_is_accepting(const const_tgba_digraph_ptr& det_a, unsigned scc_n, - const const_tgba_ptr& orig_a, scc_map& sm, + const const_tgba_ptr& orig_a, scc_info& sm, power_map& pm) { // Get some state from the SCC #n. - const state* start = sm.one_state_of(scc_n)->clone(); + const state* start = det_a->state_from_number(sm.one_state_of(scc_n)); // Find a loop around START in SCC #n. wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start); @@ -478,7 +479,7 @@ namespace spot } - tgba_digraph_ptr minimize_monitor(const const_tgba_ptr& a) + tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a) { hash_set* final = new hash_set; hash_set* non_final = new hash_set; @@ -498,7 +499,7 @@ namespace spot return res; } - tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a) + tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a) { hash_set* final = new hash_set; hash_set* non_final = new hash_set; @@ -520,8 +521,7 @@ namespace spot // We also keep track of whether an SCC is useless // (i.e., it is not the start of any accepting word). - scc_map sm(det_a); - sm.build_map(); + scc_info sm(det_a); unsigned scc_count = sm.scc_count(); // SCC that have been marked as useless. std::vector useless(scc_count); @@ -537,8 +537,8 @@ namespace spot for (unsigned m = 0; m < scc_count; ++m) { bool is_useless = true; - bool transient = sm.trivial(m); - const scc_map::succ_type& succ = sm.succ(m); + bool transient = sm.is_trivial(m); + auto& succ = sm.succ(m); if (transient && succ.empty()) { @@ -552,11 +552,10 @@ namespace spot // Also SCCs are useless if all their successor are // useless. unsigned l = k; - for (scc_map::succ_type::const_iterator j = succ.begin(); - j != succ.end(); ++j) + for (auto& j: succ) { - is_useless &= useless[j->first]; - unsigned dj = d[j->first]; + is_useless &= useless[j.dst]; + unsigned dj = d[j.dst]; if (dj < l) l = dj; } @@ -586,10 +585,8 @@ namespace spot if (!is_useless) { hash_set* dest_set = (d[m] & 1) ? non_final : final; - const std::list& l = sm.states_of(m); - std::list::const_iterator il; - for (il = l.begin(); il != l.end(); ++il) - dest_set->insert((*il)->clone()); + for (auto s: sm.states_of(m)) + dest_set->insert(det_a->state_from_number(s)); } } } diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index 6e8ad4321..9d577d7f6 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -57,7 +57,7 @@ namespace spot /// \param a the automaton to convert into a minimal deterministic monitor /// \pre Dead SCCs should have been removed from \a a before /// calling this function. - SPOT_API tgba_digraph_ptr minimize_monitor(const const_tgba_ptr& a); + SPOT_API tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a); /// \brief Minimize a Büchi automaton in the WDBA class. /// @@ -93,7 +93,7 @@ namespace spot month = oct } \endverbatim */ - SPOT_API tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a); + SPOT_API tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a); /// \brief Minimize an automaton if it represents an obligation property. /// diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 01ae9edab..0e18a8ea9 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -28,7 +28,7 @@ #include "misc/hash.hh" #include "tgbaalgos/powerset.hh" #include "bdd.h" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/cycles.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgba/tgbaproduct.hh" @@ -42,8 +42,9 @@ namespace spot { + // FIXME: Redo this algorithm using the tgba_digraph interface. tgba_digraph_ptr - tgba_powerset(const const_tgba_ptr& aut, power_map& pm, bool merge) + tgba_powerset(const const_tgba_digraph_ptr& aut, power_map& pm, bool merge) { typedef power_map::power_state power_state; typedef std::map power_set; @@ -112,7 +113,7 @@ namespace spot } tgba_digraph_ptr - tgba_powerset(const const_tgba_ptr& aut) + tgba_powerset(const const_tgba_digraph_ptr& aut) { power_map pm; return tgba_powerset(aut, pm); @@ -130,7 +131,7 @@ namespace spot typedef std::set trans_set; typedef std::vector set_set; protected: - const_tgba_ptr ref_; + const_tgba_digraph_ptr ref_; power_map& refmap_; trans_set reject_; // set of rejecting transitions set_set accept_; // set of cycles that are accepting @@ -139,7 +140,7 @@ namespace spot unsigned cycles_left_; // count of cycles left to explore public: - fix_scc_acceptance(const scc_map& sm, const_tgba_ptr ref, + fix_scc_acceptance(const scc_info& sm, const_tgba_digraph_ptr ref, power_map& refmap, unsigned threshold) : enumerate_cycles(sm), ref_(ref), refmap_(refmap), threshold_(threshold) @@ -173,8 +174,7 @@ namespace spot bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const { - auto a = std::static_pointer_cast - (std::const_pointer_cast(aut_)); + auto a = std::const_pointer_cast(aut_); // Build an automaton representing this loop. auto loop_a = make_tgba_digraph(aut_->get_dict()); @@ -268,20 +268,19 @@ namespace spot static bool fix_dba_acceptance(tgba_digraph_ptr det, - const_tgba_ptr ref, power_map& refmap, + const_tgba_digraph_ptr ref, power_map& refmap, unsigned threshold) { det->copy_acceptance_conditions_of(ref); - scc_map sm(det); - sm.build_map(); + scc_info sm(det); unsigned scc_count = sm.scc_count(); fix_scc_acceptance fsa(sm, ref, refmap, threshold); for (unsigned m = 0; m < scc_count; ++m) - if (!sm.trivial(m)) + if (!sm.is_trivial(m)) if (fsa.fix_scc(m)) return true; return false; @@ -289,7 +288,7 @@ namespace spot } tgba_digraph_ptr - tba_determinize(const const_tgba_ptr& aut, + tba_determinize(const const_tgba_digraph_ptr& aut, unsigned threshold_states, unsigned threshold_cycles) { power_map pm; diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index c2dc0c1e6..8faecddd4 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -65,9 +65,10 @@ namespace spot /// transitions. //@{ SPOT_API tgba_digraph_ptr - tgba_powerset(const const_tgba_ptr& aut, power_map& pm, bool merge = true); + tgba_powerset(const const_tgba_digraph_ptr& aut, + power_map& pm, bool merge = true); SPOT_API tgba_digraph_ptr - tgba_powerset(const const_tgba_ptr& aut); + tgba_powerset(const const_tgba_digraph_ptr& aut); //@} @@ -107,7 +108,7 @@ namespace spot /// whenever an SCC of the constructed automaton has more than \a /// threshold_cycles cycles. SPOT_API tgba_digraph_ptr - tba_determinize(const const_tgba_ptr& aut, + tba_determinize(const const_tgba_digraph_ptr& aut, unsigned threshold_states = 0, unsigned threshold_cycles = 0); diff --git a/src/tgbaalgos/product.cc b/src/tgbaalgos/product.cc new file mode 100644 index 000000000..eba2f18a4 --- /dev/null +++ b/src/tgbaalgos/product.cc @@ -0,0 +1,108 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "product.hh" +#include "tgba/tgbagraph.hh" +#include +#include +#include "misc/hash.hh" + +namespace spot +{ + namespace + { + typedef std::pair product_state; + + struct product_state_hash + { + size_t + operator()(product_state s) const + { + return wang32_hash(s.first ^ wang32_hash(s.second)); + } + }; + } + + + tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, + const const_tgba_digraph_ptr& right, + unsigned left_state, + unsigned right_state) + { + std::unordered_map s2n; + std::deque> todo; + + assert(left->get_dict() == right->get_dict()); + auto res = make_tgba_digraph(left->get_dict()); + res->copy_ap_of(left); + res->copy_ap_of(right); + res->set_acceptance_conditions(left->acc().num_sets() + + right->acc().num_sets()); + + auto v = new product_states; + res->set_named_prop("product-states", v, [](void* vv) { + delete static_cast(vv); + }); + + auto new_state = + [&](unsigned left_state, unsigned right_state) -> unsigned + { + product_state x(left_state, right_state); + auto p = s2n.emplace(x, 0); + if (p.second) // This is a new state + { + p.first->second = res->new_state(); + todo.emplace_back(x, p.first->second); + assert(p.first->second == v->size()); + v->push_back(x); + } + return p.first->second; + }; + + new_state(left_state, right_state); + while (!todo.empty()) + { + auto top = todo.front(); + todo.pop_front(); + for (auto& l: left->out(top.first.first)) + for (auto& r: right->out(top.first.second)) + { + auto cond = l.cond & r.cond; + 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)); + // If right is deterministic, we can abort immediately! + } + } + + return res; + } + + tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, + const const_tgba_digraph_ptr& right) + { + return product(left, right, + left->get_init_state_number(), + right->get_init_state_number()); + } + +} diff --git a/src/tgbaalgos/product.hh b/src/tgbaalgos/product.hh new file mode 100644 index 000000000..b22c229dd --- /dev/null +++ b/src/tgbaalgos/product.hh @@ -0,0 +1,45 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#ifndef SPOT_TGBAALGOS_PRODUCT_HH +# define SPOT_TGBAALGOS_PRODUCT_HH + +#include "misc/common.hh" +#include "tgba/fwd.hh" +#include +#include + +namespace spot +{ + // The tgba constructed by product() below contain property named + // "product-states" with type product_states. + typedef std::vector> product_states; + + SPOT_API + tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, + const const_tgba_digraph_ptr& right); + + SPOT_API + tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, + const const_tgba_digraph_ptr& right, + unsigned left_state, + unsigned right_state); +} + +#endif // SPOT_TGBAALGOS_PRODUCT_HH diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 063547506..52f146f15 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -24,26 +24,23 @@ namespace spot { bool - is_guarantee_automaton(const const_tgba_ptr& aut, const scc_map* sm) + is_guarantee_automaton(const const_tgba_digraph_ptr& aut, + const scc_info* sm) { - // Create an scc_map of the user did not give one to us. + // Create an scc_info if the user did not give one to us. bool need_sm = !sm; if (need_sm) - { - scc_map* x = new scc_map(aut); - x->build_map(); - sm = x; - } + sm = new scc_info(aut); bool result = true; unsigned scc_count = sm->scc_count(); - for (unsigned scc = 0; (scc < scc_count) && result; ++scc) + for (unsigned scc = 0; scc < scc_count; ++scc) { - if (!sm->accepting(scc)) + if (!sm->is_accepting_scc(scc)) continue; // Accepting SCCs should have only one state. - const std::list& st = sm->states_of(scc); + auto& st = sm->states_of(scc); if (st.size() != 1) { result = false; @@ -51,50 +48,28 @@ namespace spot } // The state should have only one transition that is a // self-loop labelled by true. - const state* s = *st.begin(); - tgba_succ_iterator* it = aut->succ_iter(s); - it->first(); - assert(!it->done()); - state* dest = it->current_state(); - bdd cond = it->current_condition(); - result = (!it->next()) && (cond == bddtrue) && (!dest->compare(s)); - dest->destroy(); - aut->release_iter(it); + auto src = st.front(); + auto out = aut->out(src); + auto it = out.begin(); + assert(it != out.end()); + result = + (it->cond == bddtrue) && (it->dst == src) && (++it == out.end()); + if (!result) + break; } - // Free the scc_map if we created it. if (need_sm) delete sm; - return result; } - bool is_safety_mwdba(const const_tgba_ptr& aut) + bool is_safety_mwdba(const const_tgba_digraph_ptr& aut) { - state_unicity_table seen; // States already seen. - std::deque todo; // A queue of states yet to explore. - - todo.push_back(seen(aut->get_init_state())); - - bool all_accepting = true; - while (all_accepting && !todo.empty()) - { - const state* s = todo.front(); - todo.pop_front(); - - for (auto it: aut->succ(s)) - { - auto acc = it->current_acceptance_conditions(); - if (!aut->acc().accepting(acc)) - { - all_accepting = false; - break; - } - if (const state* d = seen.is_new(it->current_state())) - todo.push_back(d); - } - } - return all_accepting; + for (auto& t: aut->transitions()) + if (!aut->is_dead_transition(t)) + if (!aut->acc().accepting(t.acc)) + return false; + return true; } diff --git a/src/tgbaalgos/safety.hh b/src/tgbaalgos/safety.hh index f083a1d20..f2a58eb8e 100644 --- a/src/tgbaalgos/safety.hh +++ b/src/tgbaalgos/safety.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -20,7 +20,7 @@ #ifndef SPOT_TGBAALGOS_SAFETY_HH # define SPOT_TGBAALGOS_SAFETY_HH -#include "scc.hh" +#include "sccinfo.hh" namespace spot { @@ -43,11 +43,11 @@ namespace spot /// /// \param aut the automaton to check /// - /// \param sm an scc_map of the automaton if available (it will be - /// built otherwise. If you supply an scc_map you should call - /// build_map() before passing it to this function. + /// \param sm an scc_info object for the automaton if available (it + /// will be built otherwise). SPOT_API bool - is_guarantee_automaton(const const_tgba_ptr& aut, const scc_map* sm = 0); + is_guarantee_automaton(const const_tgba_digraph_ptr& aut, + const scc_info* sm = 0); /// \brief Whether a minimized WDBA represents a safety property. /// @@ -57,7 +57,7 @@ namespace spot /// /// \param aut the automaton to check SPOT_API bool - is_safety_mwdba(const const_tgba_ptr& aut); + is_safety_mwdba(const const_tgba_digraph_ptr& aut); } diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index d52d4fec3..8b6faa362 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -121,7 +121,7 @@ namespace spot node_.emplace_back(acc, triv); std::swap(node_.back().succ, root_.front().node.succ); std::swap(node_.back().states, root_.front().node.states); - node_.back().accepting = aut->acc().accepting(acc); + node_.back().accepting = !triv && aut->acc().accepting(acc); root_.pop_front(); // Record the transition between the SCC being popped // and the previous SCC. @@ -229,6 +229,16 @@ namespace spot } + std::set scc_info::used_acc_of(unsigned scc) const + { + std::set res; + for (auto src: states_of(scc)) + for (auto& t: aut_->out(src)) + if (scc_of(t.dst) == scc) + res.insert(t.acc); + return res; + } + std::vector> scc_info::used_acc() const { unsigned n = aut_->num_states(); diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 9616566c7..ec92a5761 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -45,12 +45,12 @@ namespace spot struct scc_node { scc_node(): - acc(0U), trivial(true) + acc(0U), trivial(true), accepting(false), useful(false) { } scc_node(acc_cond::mark_t acc, bool trivial): - acc(acc), trivial(trivial) + acc(acc), trivial(trivial), accepting(false), useful(false) { } @@ -104,6 +104,18 @@ namespace spot return node(scc).states; } + unsigned one_state_of(unsigned scc) const + { + return states_of(scc).front(); + } + + /// \brief Get number of the SCC containing the initial state. + unsigned initial() const + { + assert(scc_count() - 1 == scc_of(aut_->get_init_state_number())); + return scc_count() - 1; + } + const scc_succs& succ(unsigned scc) const { return node(scc).succ; @@ -138,6 +150,9 @@ namespace spot /// each accepting SCC. std::vector> used_acc() const; + std::set used_acc_of(unsigned scc) const; + + std::vector weak_sccs() const; bdd scc_ap_support(unsigned scc) const; diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index ed1437371..99325ad95 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -122,7 +122,7 @@ int main(int argc, char* argv[]) { spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; - spot::tgba_ptr a = spot::tgba_parse(file, pel, dict, env); + spot::tgba_digraph_ptr a = spot::tgba_parse(file, pel, dict, env); if (spot::format_tgba_parse_errors(std::cerr, file, pel)) return 2; @@ -147,15 +147,13 @@ int main(int argc, char* argv[]) } else if (print_formula) { - spot::tgba_ptr a; - spot::ltl::parse_error_list p1; const spot::ltl::formula* f1 = spot::ltl::parse(file, p1); if (spot::ltl::format_parse_errors(std::cerr, file, p1)) return 2; - a = spot::ltl_to_tgba_fm(f1, dict); + auto a = spot::ltl_to_tgba_fm(f1, dict); spot::tgba_ptr complement = 0; complement = spot::make_safra_complement(a); @@ -164,7 +162,7 @@ int main(int argc, char* argv[]) } else if (stats) { - spot::tgba_ptr a; + spot::tgba_digraph_ptr a; const spot::ltl::formula* f1 = 0; if (formula) @@ -211,10 +209,8 @@ int main(int argc, char* argv[]) if (formula) { - const spot::ltl::formula* nf1 = - spot::ltl::unop::instance(spot::ltl::unop::Not, - f1->clone()); - spot::tgba_ptr a2 = spot::ltl_to_tgba_fm(nf1, dict); + auto nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone()); + auto a2 = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba_statistics a_size = spot::stats_reachable(a2); std::cout << "Not Formula: " << a_size.states << ", " @@ -234,14 +230,11 @@ int main(int argc, char* argv[]) if (spot::ltl::format_parse_errors(std::cerr, file, p1)) return 2; - spot::tgba_ptr Af = spot::ltl_to_tgba_fm(f1, dict); - const spot::ltl::formula* nf1 = - spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone()); - spot::tgba_ptr Anf = spot::ltl_to_tgba_fm(nf1, dict); - - spot::tgba_ptr nAf = spot::make_safra_complement(Af); - spot::tgba_ptr nAnf = spot::make_safra_complement(Anf); - + auto Af = spot::ltl_to_tgba_fm(f1, dict); + auto nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone()); + auto Anf = spot::ltl_to_tgba_fm(nf1, dict); + auto nAf = spot::make_safra_complement(Af); + auto nAnf = spot::make_safra_complement(Anf); auto ec = spot::couvreur99(spot::product(nAf, nAnf)); auto res = ec->check(); spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc index 73211f592..8e46feb42 100644 --- a/src/tgbatest/emptchk.cc +++ b/src/tgbatest/emptchk.cc @@ -103,7 +103,7 @@ main(int argc, char** argv) { auto a = spot::ltl_to_taa(f, d); aut[0] = a; - aut[1] = spot::degeneralize_tba(a); + aut[1] = spot::degeneralize_tba(spot::tgba_dupexp_bfs(a)); } { auto a = spot::ltl_to_tgba_fm(f, d); diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 03a78f4ea..412bb5a41 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -400,15 +400,15 @@ in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) -TA -lv -sp | 45 | 676 | 9 -TA -lv -sp -RT | 35 | 566 | 4 -TA -DS | 54 | 722 | 26 --TA -DS -RT | 42 | 608 | 18 +-TA -DS -RT | 38 | 534 | 17 -TA -DS -lv | 55 | 800 | 19 --TA -DS -lv -RT | 44 | 702 | 13 +-TA -DS -lv -RT | 39 | 608 | 11 -TA -DS -sp | 54 | 776 | 18 --TA -DS -sp -RT | 43 | 678 | 12 +-TA -DS -sp -RT | 38 | 586 | 10 -TA -DS -lv -sp | 55 | 800 | 19 --TA -DS -lv -sp -RT | 44 | 702 | 13 --x -TA -DS -in | 55 | 694 | 11 --x -TA -DS -in -RT | 41 | 597 | 8 +-TA -DS -lv -sp -RT | 39 | 608 | 11 +-x -TA -DS -in | 55 | 696 | 11 +-x -TA -DS -in -RT | 42 | 603 | 8 in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TGTA | 69 | 1539 | XXX -TGTA -RT | 49 | 935 | XXX @@ -429,7 +429,7 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TA -DS -lv -sp | 125 | 3028 | 42 -TA -DS -lv -sp -RT | 97 | 2149 | 40 -x -TA -DS -in | 125 | 1838 | 25 --x -TA -DS -in -RT | 87 | 1296 | 25 +-x -TA -DS -in -RT | 90 | 1368 | 25 EOF sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 4729672d4..b4c12e763 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -54,7 +54,7 @@ #include "tgbaalgos/gtec/gtec.hh" #include "misc/timer.hh" #include "tgbaalgos/stats.hh" -#include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/sccinfo.hh" @@ -1286,14 +1286,14 @@ checked_main(int argc, char** argv) { if (degeneralize_opt == DegenTBA) { - a = spot::degeneralize_tba(a, degen_reset, degen_order, - degen_cache); + a = spot::degeneralize_tba(ensure_digraph(a), + degen_reset, degen_order, degen_cache); } else if (degeneralize_opt == DegenSBA) { tm.start("degeneralization"); - a = spot::degeneralize(a, degen_reset, degen_order, - degen_cache); + a = spot::degeneralize(ensure_digraph(a), + degen_reset, degen_order, degen_cache); tm.stop("degeneralization"); assume_sba = true; } @@ -1303,7 +1303,8 @@ checked_main(int argc, char** argv) && (!f || f->is_syntactic_recurrence())) { tm.start("determinization 2"); - auto determinized = tba_determinize(a, 0, opt_determinize_threshold); + auto determinized = tba_determinize(ensure_digraph(a), 0, + opt_determinize_threshold); tm.stop("determinization 2"); if (determinized) a = determinized; @@ -1312,7 +1313,7 @@ checked_main(int argc, char** argv) if (opt_monitor) { tm.start("Monitor minimization"); - a = minimize_monitor(a); + a = minimize_monitor(ensure_digraph(a)); tm.stop("Monitor minimization"); assume_sba = false; // All states are accepting, so double // circles in the dot output are @@ -1397,7 +1398,7 @@ checked_main(int argc, char** argv) if (opt_monitor) { tm.start("Monitor minimization"); - a = minimize_monitor(a); + a = minimize_monitor(ensure_digraph(a)); tm.stop("Monitor minimization"); assume_sba = false; // All states are accepting, so double // circles in the dot output are @@ -1509,7 +1510,7 @@ checked_main(int argc, char** argv) if (degeneralize_opt == DegenTBA) { tm.start("degeneralize product"); - a = spot::degeneralize_tba(a, + a = spot::degeneralize_tba(ensure_digraph(a), degen_reset, degen_order, degen_cache); @@ -1518,7 +1519,7 @@ checked_main(int argc, char** argv) else if (degeneralize_opt == DegenSBA) { tm.start("degeneralize product"); - a = spot::degeneralize(a, + a = spot::degeneralize(ensure_digraph(a), degen_reset, degen_order, degen_cache); @@ -1572,7 +1573,7 @@ checked_main(int argc, char** argv) // It is possible that we have applied other // operations to the automaton since its initial // degeneralization. Let's degeneralize again! - auto s = spot::degeneralize(a, degen_reset, + auto s = spot::degeneralize(ensure_digraph(a), degen_reset, degen_order, degen_cache); spot::never_claim_reachable(std::cout, s, f, spin_comments); } @@ -1621,8 +1622,8 @@ checked_main(int argc, char** argv) } else { - bool g = is_guarantee_automaton(a); - bool s = is_safety_mwdba(a); + bool g = is_guarantee_automaton(ensure_digraph(a)); + bool s = is_safety_mwdba(ensure_digraph(a)); if (g && !s) { std::cout << "this is a guarantee property (hence, " @@ -1649,8 +1650,7 @@ checked_main(int argc, char** argv) break; case 15: { - spot::scc_map m(a); - m.build_map(); + spot::scc_info m(ensure_digraph(a)); spot::enumerate_cycles c(m); unsigned max = m.scc_count(); for (unsigned n = 0; n < max; ++n) @@ -1662,8 +1662,7 @@ checked_main(int argc, char** argv) } case 16: { - spot::scc_map m(a); - m.build_map(); + spot::scc_info m(ensure_digraph(a)); unsigned max = m.scc_count(); for (unsigned n = 0; n < max; ++n) { diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index d543ebbbb..5e05c945c 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -46,7 +46,7 @@ #include "misc/random.hh" #include "misc/optionmap.hh" #include "tgbaalgos/degen.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "misc/timer.hh" #include "tgbaalgos/ltl2tgba_fm.hh" @@ -85,8 +85,8 @@ const char* default_algos[] = { std::vector ec_algos; spot::emptiness_check_ptr -cons_emptiness_check(int num, spot::const_tgba_ptr a, - const spot::const_tgba_ptr& degen, +cons_emptiness_check(int num, spot::const_tgba_digraph_ptr a, + const spot::const_tgba_digraph_ptr& degen, unsigned int n_acc) { auto inst = ec_algos[num].inst; @@ -579,8 +579,8 @@ main(int argc, char** argv) bool stop_on_first_difference = false; - spot::tgba_ptr formula = nullptr; - spot::tgba_ptr product = nullptr; + spot::tgba_digraph_ptr formula = nullptr; + spot::tgba_digraph_ptr product = nullptr; spot::option_map options; @@ -906,7 +906,7 @@ main(int argc, char** argv) spot::srand(opt_ec_seed); - spot::tgba_ptr a = + spot::tgba_digraph_ptr a = spot::random_graph(opt_n, opt_d, apf, dict, opt_n_acc, opt_a, opt_t); if (formula) @@ -925,7 +925,7 @@ main(int argc, char** argv) } else { - spot::tgba_ptr degen = nullptr; + spot::tgba_digraph_ptr degen = nullptr; if (opt_degen && real_n_acc > 1) degen = degeneralize_tba(a);