diff --git a/bench/ltl2tgba/tools.sim b/bench/ltl2tgba/tools.sim index 0438788e4..0935b3ea7 100644 --- a/bench/ltl2tgba/tools.sim +++ b/bench/ltl2tgba/tools.sim @@ -1,6 +1,6 @@ ## -*- coding: utf-8; mode: sh -*- -## Copyright (C) 2013 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -25,11 +25,9 @@ set dummy \ "$LTL2TGBA --lbtt -x simul=1 %f >%T" \ "$LTL2TGBA --lbtt -x simul=2 %f >%T" \ "$LTL2TGBA --lbtt -x simul=3 %f >%T" \ - "$LTL2TGBA --lbtt -x simul=4 %f >%T" \ "$LTL2TGBA --lbtt --ba -x simul=0 %f >%T" \ "$LTL2TGBA --lbtt --ba -x simul=1 %f >%T" \ "$LTL2TGBA --lbtt --ba -x simul=2 %f >%T" \ "$LTL2TGBA --lbtt --ba -x simul=3 %f >%T" \ - "$LTL2TGBA --lbtt --ba -x simul=4 %f >%T" \ --timeout=300 shift diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc index 7a1ab2a2f..52d02e690 100644 --- a/src/bin/spot-x.cc +++ b/src/bin/spot-x.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// 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. // @@ -86,15 +86,8 @@ with more states.") }, { DOC("simul", "Set to 0 to disable simulation-based reductions. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ -Set to 4 to apply only \"don't care\" direct simulation. Set to 5 to \ -iterate \"don't care\" direct simulation and reverse simulation. The \ -default is 3, except when option --low is specified, in which case the \ -default is 1.") }, - { DOC("simul-limit", "Can be set to a positive integer to cap the \ -number of \"don't care\" transitions considered by the \ -\"don't care\"-simulation algorithm. A negative value (the default) \ -does not enforce any limit. Note that if there are N \"don't care\" \ -transitions, the algorithm may potentially test 2^N configurations.") }, +The default is 3, except when option --low is specified, in which case \ +the default is 1.") }, { DOC("ba-simul", "Set to 0 to disable simulation-based reductions \ on the Büchi automaton (i.e., after degeneralization has been performed). \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index bf7f919f9..acffc2f4b 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -48,7 +48,6 @@ namespace spot degen_cache_ = opt->get("degen-lcache", 1); degen_lskip_ = opt->get("degen-lskip", 1); simul_ = opt->get("simul", -1); - simul_limit_ = opt->get("simul-limit", -1); scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); tba_determinisation_ = opt->get("tba-det", 0); @@ -87,10 +86,6 @@ namespace spot case 3: default: return iterated_simulations(a); - case 4: - return dont_care_simulation(a, simul_limit_); - case 5: - return dont_care_iterated_simulations(a, simul_limit_); } } diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 61f0e3660..674268ec3 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,7 +117,6 @@ namespace spot int degen_cache_; bool degen_lskip_; int simul_; - int simul_limit_; int scc_filter_; int ba_simul_; bool tba_determinisation_; diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 8c93279f3..a4101ea8f 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -71,18 +71,9 @@ // The automaton simulated is recomplemented to come back to its initial // state when the object Simulation is destroyed. // -// Obviously these functions are possibly cut into several little one. +// Obviously these functions are possibly cut into several little ones. // This is just the general development idea. -// How to use isop: -// I need all variable non_acceptance & non_class. -// bdd_support(sig(X)): All var -// bdd_support(sig(X)) - allacc - allclassvar - - -// TODO LIST: Play on the order of the selection in the -// dont_care_simulation. The good place to work is in add_to_map_imply. - namespace spot { @@ -102,49 +93,6 @@ namespace spot typedef std::map map_bdd_state; - // Our constraint: (state_src, state_dst) = to_add. - // We define the couple of state as the key of the constraint. - typedef std::pair constraint_key; - - // But we need a comparator for that key. - struct constraint_key_comparator - { - bool operator()(const constraint_key& l, - const constraint_key& r) const - { - if (l.first->compare(r.first) < 0) - return true; - else - if (l.first->compare(r.first) > 0) - return false; - - if (l.second->compare(r.second) < 0) - return true; - else - if (l.second->compare(r.second) > 0) - return false; - - return false; - } - }; - - // The full definition of the constraint. - typedef std::map map_constraint; - - typedef std::tuple constraint; - - // Helper to create the map of constraints to give to the - // simulation. - void add_to_map(const std::list& list, - map_constraint& feed_me) - { - for (auto& p: list) - feed_me.emplace(std::make_pair(std::get<0>(p), - std::get<1>(p)), - std::get<2>(p)); - } - // This class helps to compare two automata in term of // size. @@ -239,12 +187,10 @@ namespace spot return aut->acc().marks(res.begin(), res.end()); } - direct_simulation(const const_tgba_ptr& t, - const map_constraint* map_cst = 0) + direct_simulation(const const_tgba_ptr& t) : a_(0), po_size_(0), all_class_var_(bddtrue), - map_cst_(map_cst), original_(t) { // We need to do a dupexp for being able to run scc_info later. @@ -408,23 +354,7 @@ namespace spot for (auto& t: a_->out(src)) { - bdd acc = bddtrue; - - map_constraint::const_iterator it; - // Check if we have a constraint about this edge in the - // original automaton. - if (map_cst_ - && ((it = map_cst_ - ->find(std::make_pair(new_original_[src], - new_original_[t.dst]))) - != map_cst_->end())) - { - acc = it->second; - } - else - { - acc = mark_to_bdd(t.acc); - } + 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 @@ -792,523 +722,9 @@ namespace spot std::unique_ptr scc_info_; std::vector new_original_; - const map_constraint* map_cst_; - const_tgba_ptr original_; }; - // For now, we don't try to handle cosimulation. - class direct_simulation_dont_care: public direct_simulation - { - typedef std::vector > constraints; - typedef std::map, // Constraints list. - bdd_less_than>, - bdd_less_than> constraint_list; - typedef std::list > list_bdd_bdd; - - - public: - direct_simulation_dont_care(const const_tgba_ptr& t) - : direct_simulation(t) - { - // This variable is used in the new signature. - on_cycle_ = - bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, this)); - - // This one is used for the iteration on all the - // possibilities. Avoid computing two times "no constraints". - empty_seen_ = false; - - - // If this variable is set to true, we have a number limit of - // simulation to run. - has_limit_ = false; - - notap = bdd_support(all_proms_) & all_class_var_ & on_cycle_; - } - - // This function computes the don't care signature of the state - // src. This signature is similar to the classic one, excepts - // that if the transition is on a SCC, we add a on_cycle_ on it, - // otherwise we add !on_cycle_. This allows us to split the - // signature later. - bdd dont_care_compute_sig(unsigned src) - { - bdd res = bddfalse; - - unsigned scc = scc_info_->scc_of(src); - if (scc == -1U) // Unreachable - return bddfalse; - bool sccacc = scc_info_->is_accepting_scc(scc); - - for (auto& t: a_->out(src)) - { - bdd cl = previous_class_[t.dst]; - bdd acc; - - if (scc != scc_info_->scc_of(t.dst)) - acc = !on_cycle_; - else if (sccacc) - acc = on_cycle_ & mark_to_bdd(t.acc); - else - acc = on_cycle_ & all_proms_; - - bdd to_add = acc & t.cond & relation_[cl]; - res |= to_add; - } - - return res; - } - - // We used to have - // sig(s1) = (f1 | g1) - // sig(s2) = (f2 | g2) - // and we say that s2 simulates s1 if sig(s1)=>sig(s2). - // This amount to testing whether (f1|g1)=>(f2|g2), - // which is equivalent to testing both - // f1=>(f2|g2) and g1=>(f2|g2) - // separately. - // - // Now we have a slightly improved version of this rule. - // g1 and g2 are not on cycle, so they can make as many - // promises as we wish, if that helps. Adding promises - // to g2 will not help, but adding promises to g1 can. - // - // So we test whether - // f1=>(f2|g2) - // g1=>noprom(f2|g2) - // Where noprom(f2|g2) removes all promises from f2|g2. - // (g1 do not have promises, and neither do g2). - - bool could_imply_aux(bdd f1, bdd g1, bdd left_class, - bdd right, bdd right_class) - { - bdd f2g2 = bdd_exist(right, on_cycle_); - bdd f2g2n = bdd_exist(f2g2, all_proms_); - - bdd both = left_class & right_class; - int lc = bdd_var(left_class); - f1 = bdd_compose(f1, both, lc); - g1 = bdd_compose(g1, both, lc); - f2g2 = bdd_compose(f2g2, both, lc); - f2g2n = bdd_compose(f2g2n, both, lc); - - return bdd_implies(f1, f2g2) && bdd_implies(g1, f2g2n); - } - - bool could_imply(bdd left, bdd left_class, - bdd right, bdd right_class) - { - bdd f1 = bdd_relprod(left, on_cycle_, on_cycle_); - bdd g1 = bdd_relprod(left, !on_cycle_, on_cycle_); - - //bdd f1 = bdd_restrict(left, on_cycle_); - //bdd g1 = bdd_restrict(left, !on_cycle_); - return could_imply_aux(f1, g1, left_class, - right, right_class); - } - - void dont_care_update_po(const list_bdd_bdd& now_to_next, - map_bdd_bdd& relation) - { - // This loop follows the pattern given by the paper. - // foreach class do - // | foreach class do - // | | update po if needed - // | od - // od - - for (list_bdd_bdd::const_iterator it1 = now_to_next.begin(); - it1 != now_to_next.end(); - ++it1) - { - bdd accu = it1->second; - - bdd f1 = bdd_relprod(it1->first, on_cycle_, on_cycle_); - bdd g1 = bdd_relprod(it1->first, !on_cycle_, on_cycle_); - - // bdd f1 = bdd_restrict(it1->first_, on_cycle_); - // bdd g1 = bdd_restrict(it1->first_, !on_cycle_); - - for (list_bdd_bdd::const_iterator it2 = now_to_next.begin(); - it2 != now_to_next.end(); - ++it2) - { - // Skip the case managed by the initialization of accu. - if (it1 == it2) - continue; - - if (could_imply_aux(f1, g1, it1->second, - it2->first, it2->second)) - { - accu &= it2->second; - ++po_size_; - } - } - relation[it1->second] = accu; - } - } - -#define ISOP(bdd) #bdd" - " << bdd_format_isop(a_->get_dict(), bdd) - - inline bool is_out_scc(bdd b) - { - return bddfalse != bdd_relprod(b, !on_cycle_, on_cycle_); - // return bddfalse != bdd_restrict(b, !on_cycle_); - } - - // This method solves three kind of problems, where we have two - // conjunctions of variable (that corresponds to a particular - // transition), and where left could imply right. - // Three cases: - // - αP₁ ⇒ xβP₁ where x is unknown. - // - xβP₁ ⇒ αP₁ where x is unknown. - // - xαP₁ ⇒ yβP₁ where x, y are unknown. - void create_simple_constraint(bdd left, bdd right, - unsigned src_left, - unsigned src_right, - std::list& constraint) - { - assert(src_left != src_right); - // Determine which is the current case. - bool out_scc_left = is_out_scc(left); - bool out_scc_right = is_out_scc(right); - bdd dest_class = bdd_existcomp(left, all_class_var_); - assert(revert_relation_.find(dest_class) != revert_relation_.end()); - unsigned dst_left = revert_relation_[dest_class]; - dest_class = bdd_existcomp(right, all_class_var_); - unsigned dst_right = revert_relation_[dest_class]; - - assert(src_left != dst_left || src_right != dst_right); - - left = bdd_exist(left, all_class_var_ & on_cycle_); - right = bdd_exist(right, all_class_var_ & on_cycle_); - - if (!out_scc_left && out_scc_right) - { - bdd b = bdd_exist(right, notap); - bdd add = bdd_exist(left & b, bdd_support(b)); - - if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue) - { - assert(src_right != dst_right); - - constraint.emplace_back(new_original_[src_right], - new_original_[dst_right], - add); - } - } - else if (out_scc_left && !out_scc_right) - { - bdd b = bdd_exist(left, notap); - bdd add = bdd_exist(right & b, bdd_support(b)); - - if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue) - { - assert(src_left != dst_left); - - constraint.emplace_back(new_original_[src_left], - new_original_[dst_left], - add); - } - } - else if (out_scc_left && out_scc_right) - { - bdd b = bdd_exist(left, notap); - bdd add = bdd_exist(right & b, bdd_support(b)); - - if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue) - { - assert(src_left != dst_left && src_right != dst_right); - // FIXME: cas pas compris. - constraint.emplace_back(new_original_[src_left], - new_original_[dst_left], - add); - constraint.emplace_back(new_original_[src_right], - new_original_[dst_right], - add); - } - - } - else - SPOT_UNREACHABLE(); - } - - - // This function run over the signatures, and select the - // transitions that are out of a SCC and call the function - // create_simple_constraint to solve the problem. - - // NOTE: Currently, this may not be the most accurate method, - // because we check for equality in the destination part of the - // signature. We may just check the destination that can be - // implied instead. - std::list create_new_constraint(unsigned left, - unsigned right, - vector_state_bdd& state2sig) - { - bdd pcl = previous_class_[left]; - bdd pcr = previous_class_[right]; - - bdd sigl = state2sig[left]; - bdd sigr = state2sig[right]; - - std::list res; - - bdd ex = all_class_var_ & on_cycle_; - - bdd both = pcl & pcr; - int lc = bdd_var(pcl); -#define DEST(x) bdd_compose(bdd_existcomp(x, ex), both, lc) - - // Key is destination class, value is the signature part that - // led to this destination class. - map_bdd_bdd sigl_map; - { - minato_isop isop(sigl & on_cycle_); - bdd cond_acc_dest; - while ((cond_acc_dest = isop.next()) != bddfalse) - sigl_map[DEST(cond_acc_dest)] - |= cond_acc_dest; - } - { - minato_isop isop(sigl & !on_cycle_); - bdd cond_acc_dest; - while ((cond_acc_dest = isop.next()) != bddfalse) - sigl_map[DEST(cond_acc_dest)] - |= cond_acc_dest; - } - map_bdd_bdd sigr_map; - { - minato_isop isop2(sigr & on_cycle_); - bdd cond_acc_dest2; - while ((cond_acc_dest2 = isop2.next()) != bddfalse) - sigr_map[DEST(cond_acc_dest2)] - |= cond_acc_dest2; - } - { - minato_isop isop2(sigr & !on_cycle_); - bdd cond_acc_dest2; - while ((cond_acc_dest2 = isop2.next()) != bddfalse) - sigr_map[DEST(cond_acc_dest2)] - |= cond_acc_dest2; - } - - // Iterate over the transitions of both states. - for (auto lp: sigl_map) - for (auto rp: sigr_map) - // And create constraints if any of the transitions - // is out of the SCC and the left could imply the right. - if ((is_out_scc(lp.second) || is_out_scc(rp.second)) - && (bdd_exist(lp.first, on_cycle_) == - bdd_exist(rp.first, on_cycle_))) - create_simple_constraint(lp.second, rp.second, - left, right, res); - return res; - } - - tgba_digraph_ptr run() - { - // Iterate the simulation until the end. We just don't return - // an automaton. This allows us to get all the information - // about the states and their signature. - main_loop(); - - // Compute the don't care signatures, - map_bdd_lstate dont_care_bdd_lstate; - // Useful to keep track of who is who. - vector_state_bdd dont_care_state2sig(size_a_); - vector_state_bdd state2sig(size_a_); - - list_bdd_bdd dont_care_now_to_now; - map_bdd_state class2state; - list_bdd_bdd now_to_now; - bdd_lstate_.clear(); - - // Compute the don't care signature for all the states. - for (unsigned s = 0; s < size_a_; ++s) - { - bdd clas = previous_class_[s]; - bdd sig = dont_care_compute_sig(s); - dont_care_bdd_lstate[sig].push_back(s); - dont_care_state2sig[s] = sig; - dont_care_now_to_now.emplace_back(sig, clas); - class2state[clas] = s; - - sig = compute_sig(s); - bdd_lstate_[sig].push_back(s); - state2sig[s] = sig; - now_to_now.push_back(std::make_pair(sig, clas)); - } - - map_bdd_bdd dont_care_relation; - map_bdd_bdd relation; - update_po(now_to_now, relation); - dont_care_update_po(dont_care_now_to_now, dont_care_relation); - - constraint_list cc; - - for (auto p: relation) - revert_relation_[p.second] = class2state[p.first]; - - int number_constraints = 0; - relation_ = relation; - - - // make the diff between the two tables: imply and - // could_imply. - for (unsigned s = 0; s < size_a_; ++s) - { - bdd clas = previous_class_[s]; - assert(relation.find(clas) != relation.end()); - assert(dont_care_relation.find(clas) != dont_care_relation.end()); - - bdd care_rel = relation[clas]; - bdd dont_care_rel = dont_care_relation[clas]; - - if (care_rel == dont_care_rel) - continue; - - // If they are different we necessarily have - // dont_care_rel == care_rel & diff - bdd diff = bdd_exist(dont_care_rel, care_rel); - assert(dont_care_rel == (care_rel & diff)); - assert(diff != bddtrue); - - do - { - bdd cur_diff = bdd_ithvar(bdd_var(diff)); - cc[clas][cur_diff] - = create_new_constraint(s, - class2state[cur_diff], - dont_care_state2sig); - ++number_constraints; - diff = bdd_high(diff); - } - while (diff != bddtrue); - } - - - -#ifndef NDEBUG - for (auto& i: class2state) - assert(previous_class_[i.second] == i.first); -#endif - - tgba_digraph_ptr min = nullptr; - - map_constraint cstr; - - if (has_limit_) - rec(cc, cstr, min, limit_); - else - rec(cc, cstr, min); - - return min; - } - -#define ERASE(inner_map, bigger_map, it) \ - inner_map.erase(it); \ - if (inner_map.empty()) \ - bigger_map.erase(bigger_map.begin()) - - // Add and erase. - void add_to_map_imply(constraint_list& constraints, - map_constraint& cstr) - { - constraint_list::iterator it = constraints.begin(); - std::map, - bdd_less_than>::iterator it2 = it->second.begin(); - - add_to_map(it2->second, cstr); - - bdd implied_list = relation_[it2->first]; // it2->first: - // destination class. - - ERASE(it->second, constraints, it2); - if (constraints.empty()) - return; - it = constraints.begin(); - // At worst, implied_list is equal to it2->first. - while (implied_list != bddtrue) - { - bdd cur_implied = bdd_ithvar(bdd_var(implied_list)); - - std::map, - bdd_less_than>::iterator tmp - = it->second.find(cur_implied); - if (tmp != it->second.end()) - { - add_to_map(tmp->second, cstr); - ERASE(it->second, constraints, tmp); - if (constraints.empty()) - return; - } - - implied_list = bdd_high(implied_list); - } - } - - // Compute recursively all the combinations. - void rec(constraint_list constraints, - map_constraint cstr, - tgba_digraph_ptr& min, - int max_depth = std::numeric_limits::max()) - { - assert(max_depth > 0); - while (!constraints.empty()) - { - if (!--max_depth) - break; - add_to_map_imply(constraints, cstr); - rec(constraints, cstr, min, max_depth); - } - - if (empty_seen_ && cstr.empty()) - return; - else if (cstr.empty()) - empty_seen_ = true; - - direct_simulation dir_sim(original_, &cstr); - tgba_digraph_ptr tmp = dir_sim.run(); - automaton_size cur_size(tmp); - if (!min || min_size_ > cur_size) - { - min = tmp; - min_size_ = cur_size; - } - } - - void set_limit(int n) - { - has_limit_ = true; - limit_ = n; - } - - private: - // This bdd is used to differentiate parts of the signature that - // are in a SCC and those that are not. - bdd on_cycle_; - - map_bdd_bdd dont_care_relation_; - - map_bdd_state revert_relation_; - - automaton_size min_size_; - - bool empty_seen_; - - bool has_limit_; - int limit_; - - bdd notap; - }; - - } // End namespace anonymous. @@ -1383,34 +799,4 @@ namespace spot return iterated_simulations_(t); } - tgba_digraph_ptr - dont_care_simulation(const const_tgba_ptr& t, int limit) - { - direct_simulation sim(t); - direct_simulation_dont_care s(sim.run()); - if (limit > 0) - s.set_limit(limit); - return s.run(); - } - - - tgba_digraph_ptr - dont_care_iterated_simulations(const const_tgba_ptr& t, int limit) - { - tgba_digraph_ptr res = 0; - automaton_size prev; - automaton_size next; - - do - { - prev = next; - res = cosimulation(dont_care_simulation(res ? res : t, limit)); - res = scc_filter(res, true); - next.set_size(res); - } - while (prev != next); - - return res; - } - } // End namespace spot. diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 14ff73e33..c248b54e1 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -79,8 +79,8 @@ namespace spot /// one state are included in the prefixes leading to one, the former /// state can be merged into the latter. /// - /// Reverse simulation is discussed in the following paper, bu - /// following paper, but generalized to handle TGBA directly. + /// Reverse simulation is discussed in the following paper, + /// but generalized to handle TGBA directly. /** \verbatim @InProceedings{ somenzi.00.cav, author = {Fabio Somenzi and Roderick Bloem}, @@ -144,19 +144,6 @@ namespace spot iterated_simulations_sba(const const_tgba_ptr& automaton); /// @} - - - // FIXME: Remove: dont_care_*_simulation is broken since the move to - // bitset acceptance, has never been really used, and really useful - // (nor really well tested and understood), so we should remove it. - SPOT_API tgba_digraph_ptr - dont_care_simulation(const const_tgba_ptr& t, int limit = -1); - - SPOT_API tgba_digraph_ptr - dont_care_iterated_simulations(const const_tgba_ptr& t, int limit = -1); - - - /// @} } // End namespace spot. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 8a1e122c9..a3cb6c901 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de ## Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -138,8 +138,6 @@ TESTS = \ randpsl.test \ cycles.test -XFAIL_TESTS = sim.test - EXTRA_DIST = $(TESTS) distclean-local: diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 988aa2760..faa06e7be 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -210,8 +210,6 @@ syntax(char* prog) << std::endl << " -RIS iterate both direct and reverse simulations" << std::endl - << " -RDCS reduce the automaton with direct simulation" - << std::endl << " -Rm attempt to WDBA-minimize the automaton" << std::endl << std::endl << " -RM attempt to WDBA-minimize the automaton unless the " @@ -390,9 +388,6 @@ checked_main(int argc, char** argv) bool reduction_dir_sim = false; bool reduction_rev_sim = false; bool reduction_iterated_sim = false; - bool reduction_dont_care_sim = false; - int limit_dont_care_sim = 0; - bool reduction_iterated_dont_care_sim = false; bool opt_bisim_ta = false; bool ta_opt = false; bool tgta_opt = false; @@ -719,18 +714,6 @@ checked_main(int argc, char** argv) { reduction_iterated_sim = true; } - else if (!strncmp(argv[formula_index], "-RDCS", 5)) - { - reduction_dont_care_sim = true; - if (argv[formula_index][5] == '=') - limit_dont_care_sim = to_int(argv[formula_index] + 6); - } - else if (!strncmp(argv[formula_index], "-RDCIS", 6)) - { - reduction_iterated_dont_care_sim = true; - if (argv[formula_index][6] == '=') - limit_dont_care_sim = to_int(argv[formula_index] + 7); - } else if (!strcmp(argv[formula_index], "-rL")) { simpltl = true; @@ -1218,8 +1201,6 @@ checked_main(int argc, char** argv) // When the minimization succeed, simulation is useless. reduction_dir_sim = false; reduction_rev_sim = false; - reduction_iterated_dont_care_sim = false; - reduction_dont_care_sim = false; reduction_iterated_sim = false; assume_sba = true; } @@ -1242,14 +1223,6 @@ checked_main(int argc, char** argv) } - if (reduction_iterated_dont_care_sim) - { - tm.start("don't care iterated simulation"); - a = spot::dont_care_iterated_simulations(a, limit_dont_care_sim); - tm.stop("don't care iterated simulation"); - assume_sba = false; - } - if (reduction_iterated_sim) { tm.start("Reduction w/ iterated simulations"); @@ -1265,23 +1238,6 @@ checked_main(int argc, char** argv) tm.stop("SCC-filter post-sim"); } - if (reduction_dont_care_sim) - { - tm.start("don't care simulation"); - a = spot::dont_care_simulation(a, limit_dont_care_sim); - tm.stop("don't care simulation"); - - if (scc_filter) - { - auto aa = std::static_pointer_cast(a); - assert(aa); - tm.start("SCC-filter on don't care"); - a = spot::scc_filter(aa, true); - tm.stop("SCC-filter on don't care"); - } - assume_sba = false; - } - unsigned int n_acc = a->acc().num_sets(); if (echeck_inst && degeneralize_opt == NoDegen diff --git a/src/tgbatest/sim.test b/src/tgbatest/sim.test deleted file mode 100755 index b925b79cf..000000000 --- a/src/tgbatest/sim.test +++ /dev/null @@ -1,83 +0,0 @@ -#! /bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2013, 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 . - -. ./defs -set -e - -cat >in.tgba < out.tgba - -cat >expected.tgba < out.tgba - -cat >expected.tgba < out -cat >expected < out -run 0 ../ltl2tgba -R3f -x -RDCS -kt 'F(a & GFa)' > out2 -diff out out2 - - -f='FG((Fp0 & (!p0 R (F!p1 U !p1))) | (G!p0 & (p0 U (Gp1 R p1))))' -run 0 ../ltl2tgba -R3f -x -RDS -kt "$f" | grep -v sub > out -run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" | grep -v sub > out2 -diff out out2 - -run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" > out2 -cat >expected <