diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 9efab7da9..fdb41d909 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -609,50 +609,198 @@ namespace spot return ret; } - tgba_digraph* scc_filter_states(const tgba_digraph* aut, scc_info* given_si) + ////////////////////////////////////////////////////////////////////// + + namespace { - // Compute scc_info if not supplied. - scc_info* si = given_si; - if (!si) - si = new scc_info(aut); - // Renumber all useful states. - unsigned in_n = aut->num_states(); // Number of input states. - unsigned out_n = 0; // Number of output states. - std::vector inout; // Associate old states to new ones. - inout.reserve(in_n); - for (unsigned i = 0; i < in_n; ++i) - if (si->is_useful_state(i)) - inout.push_back(out_n++); - else - inout.push_back(-1U); + typedef std::tuple filtered_trans; - // scc_info is not useful anymore. - if (!given_si) - delete si; - bdd_dict* bd = aut->get_dict(); - tgba_digraph* filtered = new tgba_digraph(bd); - bd->register_all_variables_of(aut, filtered); - filtered->copy_acceptance_conditions_of(aut); - const tgba_digraph::graph_t& ing = aut->get_graph(); - tgba_digraph::graph_t& outg = filtered->get_graph(); - outg.new_states(out_n); - for (unsigned isrc = 0; isrc < in_n; ++isrc) + // SCC filters are objects with two methods: + // 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 + // give replacement values for cond/acc + struct id_filter + { + scc_info* si; + id_filter(scc_info* si) + : si(si) { - unsigned osrc = inout[isrc]; - if (osrc >= out_n) - continue; - for (auto& t: ing.out(isrc)) - { - unsigned odst = inout[t.dst]; - if (odst >= out_n) - continue; - outg.new_transition(osrc, odst, t.cond, t.acc); - } } - filtered->set_init_state(aut->get_init_state_number()); - return filtered; + + // Accept all states + bool state(unsigned) + { + return true; + } + + // Accept all transitions, unmodified + filtered_trans trans(unsigned, unsigned, bdd cond, bdd acc) + { + return filtered_trans{true, cond, acc}; + } + }; + + // Remove useless states. + struct state_filter: id_filter + { + state_filter(scc_info* si) + : id_filter(si) + { + } + + bool state(unsigned s) + { + return si->is_useful_state(s); + } + }; + + // Remove acceptance conditions from all transitions outside of + // non-accepting SCCs. + struct acc_filter_all: id_filter + { + acc_filter_all(scc_info* si) + : id_filter(si) + { + } + + filtered_trans trans(unsigned src, unsigned dst, + bdd cond, bdd acc) + { + unsigned u = si->scc_of(src); + // If the transition is between two SCCs, or in a + // non-accepting SCC. Remove the acceptance sets. + if (!si->is_accepting_scc(u) || u != si->scc_of(dst)) + acc = bddfalse; + + return filtered_trans(true, cond, acc); + } + }; + + // Remove acceptance conditions from all transitions whose + // destination is not an accepting SCCs. + struct acc_filter_some: id_filter + { + acc_filter_some(scc_info* si) + : id_filter(si) + { + } + + filtered_trans trans(unsigned, unsigned dst, + bdd cond, bdd acc) + { + if (!si->is_accepting_scc(si->scc_of(dst))) + acc = bddfalse; + return filtered_trans(true, cond, acc); + } + }; + + template + struct compose_filters + { + F1 f1; + F2 f2; + + compose_filters(scc_info* si) + : f1(si), f2(si) + { + } + + bool state(unsigned s) + { + return f1.state(s) && f2.state(s); + } + + filtered_trans trans(unsigned src, unsigned dst, + bdd cond, bdd acc) + { + auto res = f1.trans(src, dst, cond, acc); + if (!std::get<0>(res)) + return res; + return f2.trans(src, dst, std::get<1>(res), std::get<2>(res)); + } + }; + + template + tgba_digraph* scc_filter_apply(const tgba_digraph* aut, scc_info* given_si) + { + // Compute scc_info if not supplied. + scc_info* si = given_si; + if (!si) + si = new scc_info(aut); + + + F filter(si); + + // Renumber all useful states. + unsigned in_n = aut->num_states(); // Number of input states. + unsigned out_n = 0; // Number of output states. + std::vector inout; // Associate old states to new ones. + inout.reserve(in_n); + for (unsigned i = 0; i < in_n; ++i) + if (filter.state(i)) + inout.push_back(out_n++); + else + inout.push_back(-1U); + + bdd_dict* bd = aut->get_dict(); + tgba_digraph* filtered = new tgba_digraph(bd); + bd->register_all_variables_of(aut, filtered); + filtered->copy_acceptance_conditions_of(aut); + const tgba_digraph::graph_t& ing = aut->get_graph(); + tgba_digraph::graph_t& outg = filtered->get_graph(); + outg.new_states(out_n); + for (unsigned isrc = 0; isrc < in_n; ++isrc) + { + unsigned osrc = inout[isrc]; + if (osrc >= out_n) + continue; + for (auto& t: ing.out(isrc)) + { + unsigned odst = inout[t.dst]; + if (odst >= out_n) + continue; + bool want; + bdd cond; + bdd acc; + std::tie(want, cond, acc) = + filter.trans(isrc, t.dst, t.cond, t.acc); + if (want) + outg.new_transition(osrc, odst, cond, acc); + } + } + if (!given_si) + delete si; + // If the initial state has been filtered out, we don't attempt + // to fix it. + auto init = inout[aut->get_init_state_number()]; + if (init < out_n) + filtered->set_init_state(init); + return filtered; + } + + + } + + tgba_digraph* + scc_filter_states(const tgba_digraph* aut, scc_info* given_si) + { + return scc_filter_apply(aut, given_si); + } + + tgba_digraph* + scc_filter(const tgba_digraph* aut, bool remove_all_useless, + scc_info* given_si) + { + if (remove_all_useless) + return scc_filter_apply>(aut, given_si); + else + return scc_filter_apply>(aut, given_si); } } diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index e24b424d3..08a08cf14 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -67,11 +67,17 @@ namespace spot /// (i.e., transitions leaving accepting states are all marked as /// accepting) may destroy this property. Use scc_filter_states() /// instead. + /// @{ SPOT_API tgba* scc_filter(const tgba* aut, bool remove_all_useless = false, scc_map* given_sm = 0, bdd susp = bddtrue, bool early_susp = false, bdd ignored = bddtrue); + SPOT_API tgba_digraph* + scc_filter(const tgba_digraph* aut, bool remove_all_useless = false, + scc_info* given_si = 0); + /// @} + /// \brief Prune unaccepting SCCs. /// /// This is an abridged version of scc_filter(), that only remove diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 614c22465..505a7d2c7 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -1309,28 +1309,28 @@ namespace spot } // End namespace anonymous. - tgba* + tgba_digraph* simulation(const tgba* t) { direct_simulation simul(t); return simul.run(); } - tgba* + tgba_digraph* simulation_sba(const tgba* t) { direct_simulation simul(t); return simul.run(); } - tgba* + tgba_digraph* cosimulation(const tgba* t) { direct_simulation simul(t); return simul.run(); } - tgba* + tgba_digraph* cosimulation_sba(const tgba* t) { direct_simulation simul(t); @@ -1339,21 +1339,19 @@ namespace spot template - tgba* + tgba_digraph* iterated_simulations_(const tgba* t) { - tgba* res = const_cast (t); + tgba_digraph* res = 0; automaton_size prev; automaton_size next; do { prev = next; - direct_simulation simul(res); + direct_simulation simul(res ? res : t); tgba_digraph* after_simulation = simul.run(); - - if (res != t) - delete res; + delete res; if (simul.result_is_deterministic()) { @@ -1376,53 +1374,51 @@ namespace spot return res; } - tgba* + tgba_digraph* iterated_simulations(const tgba* t) { return iterated_simulations_(t); } - tgba* + tgba_digraph* iterated_simulations_sba(const tgba* t) { return iterated_simulations_(t); } - tgba* + tgba_digraph* dont_care_simulation(const tgba* t, int limit) { direct_simulation sim(t); - tgba* tmp = sim.run(); + tgba_digraph* tmp = sim.run(); direct_simulation_dont_care s(tmp); if (limit > 0) s.set_limit(limit); - tgba* res = s.run(); + tgba_digraph* res = s.run(); delete tmp; return res; } - tgba* + tgba_digraph* dont_care_iterated_simulations(const tgba* t, int limit) { - tgba* res = const_cast (t); + tgba_digraph* res = 0; automaton_size prev; automaton_size next; do { prev = next; - - tgba* after_simulation = dont_care_simulation(res, limit); - - if (res != t) - delete res; + tgba_digraph* after_simulation = + dont_care_simulation(res ? res : t, limit); + delete res; direct_simulation cosimul(after_simulation); - tgba* after_cosimulation = cosimul.run(); + tgba_digraph* after_cosimulation = cosimul.run(); delete after_simulation; next = cosimul.get_stat(); diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 70fe017b6..9eaa5cbe9 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,6 +21,7 @@ # define SPOT_TGBAALGOS_SIMULATION_HH # include "misc/common.hh" +# include "tgba/tgbagraph.hh" namespace spot { @@ -69,8 +70,8 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba* simulation(const tgba* automaton); - SPOT_API tgba* simulation_sba(const tgba* automaton); + SPOT_API tgba_digraph* simulation(const tgba* automaton); + SPOT_API tgba_digraph* simulation_sba(const tgba* automaton); /// @} /// @{ @@ -120,8 +121,8 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba* cosimulation(const tgba* automaton); - SPOT_API tgba* cosimulation_sba(const tgba* automaton); + SPOT_API tgba_digraph* cosimulation(const tgba* automaton); + SPOT_API tgba_digraph* cosimulation_sba(const tgba* automaton); /// @} /// @{ @@ -139,15 +140,15 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba* iterated_simulations(const tgba* automaton); - SPOT_API tgba* iterated_simulations_sba(const tgba* automaton); + SPOT_API tgba_digraph* iterated_simulations(const tgba* automaton); + SPOT_API tgba_digraph* iterated_simulations_sba(const tgba* automaton); /// @} - SPOT_API tgba* + SPOT_API tgba_digraph* dont_care_simulation(const tgba* t, int limit = -1); - SPOT_API tgba* + SPOT_API tgba_digraph* dont_care_iterated_simulations(const tgba* t, int limit = -1); diff --git a/src/tgbatest/sim.test b/src/tgbatest/sim.test index d0907ed5c..515273134 100755 --- a/src/tgbatest/sim.test +++ b/src/tgbatest/sim.test @@ -45,8 +45,8 @@ run 0 ../ltl2tgba -RDCIS -b XXXXGFa > out.tgba cat >expected.tgba <