From 13673a1421a3cb26228a3e8f530138a2ade65b51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Jun 2014 19:19:06 +0200 Subject: [PATCH] sccfilter: implement a new version of tgba_digraph The new version currently supports removal of useless state as well as removal of acceptance sets from non-accepting SCCs (the two versions). It does not yet support simplifation of acceptance sets and removal of suspendable formulae. However the design, using filters that are composed before being applied, should make it easier to implement. * src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Implement the new scc_filter and supporting classes. * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Use it. The simulation now always return a tgba_digraph. * src/tgbatest/sim.test: Adjust. --- src/tgbaalgos/sccfilter.cc | 224 ++++++++++++++++++++++++++++++------ src/tgbaalgos/sccfilter.hh | 6 + src/tgbaalgos/simulation.cc | 42 +++---- src/tgbaalgos/simulation.hh | 21 ++-- src/tgbatest/sim.test | 4 +- 5 files changed, 224 insertions(+), 73 deletions(-) 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 <