From cd71286fb57305bd72a1a00f6a220840ba9c3ddd Mon Sep 17 00:00:00 2001 From: Alexandre Lewkowicz Date: Fri, 5 Feb 2016 15:42:22 +0100 Subject: [PATCH] safra: Add stutter-invarience optimisation * spot/twaalgos/safra.cc, spot/twaalgos/safra.hh: Here. * tests/core/safra.cc: Add option. --- spot/twaalgos/safra.cc | 56 ++++++++++++++++++++++++++++++++++++------ spot/twaalgos/safra.hh | 6 +++-- tests/core/safra.cc | 10 ++++++-- 3 files changed, 61 insertions(+), 11 deletions(-) diff --git a/spot/twaalgos/safra.cc b/spot/twaalgos/safra.cc index 8e7809289..12a41bae2 100644 --- a/spot/twaalgos/safra.cc +++ b/spot/twaalgos/safra.cc @@ -240,15 +240,44 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, std::unordered_map& bdd2num, std::vector& all_bdds, bool scc_opt, - bool use_bisimulation) const + bool use_bisimulation, + bool use_stutter) const { for (auto& ap: all_bdds) { - safra_state ss = compute_succ(aut, ap, scc, implications, is_connected, - scc_opt, use_bisimulation); + safra_state ss = *this; + + if (use_stutter && aut->prop_stutter_invariant()) + { + std::vector colors; + unsigned int counter = 0; + std::map safra2id; + bool stop = false; + while (!stop) + { + auto pair = safra2id.insert({ss, counter++}); + // insert should never fail + assert(pair.second); + ss = ss.compute_succ(aut, ap, scc, implications, is_connected, + scc_opt, use_bisimulation); + colors.push_back(ss.color_); + stop = safra2id.find(ss) != safra2id.end(); + } + // Add color of final transition that loops back + colors.push_back(ss.color_); + unsigned int loop_start = safra2id[ss]; + for (auto& min: safra2id) + { + if (min.second >= loop_start && ss < min.first) + ss = min.first; + } + ss.color_ = *std::min_element(colors.begin(), colors.end()); + } + else + ss = compute_succ(aut, ap, scc, implications, is_connected, + scc_opt, use_bisimulation); unsigned bdd_idx = bdd2num[ap]; res.emplace_back(ss, bdd_idx); - } } @@ -455,6 +484,18 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, bool safra_state::operator<(const safra_state& other) const { + if (nodes_ == other.nodes_) + { + for (auto& n: nodes_) + { + auto it = other.nodes_.find(n.first); + assert(it != other.nodes_.end()); + if (nesting_cmp(n.second, it->second)) + return true; + } + return false; + } + return nodes_ < other.nodes_; } @@ -487,7 +528,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, bool pretty_print, bool scc_opt, bool use_bisimulation, - bool complete) + bool complete, bool use_stutter) { // Degeneralize twa_graph_ptr aut = spot::degeneralize_tba(a); @@ -569,11 +610,12 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, unsigned src_num = seen.find(curr)->second; todo.pop_front(); curr.compute_succs(aut, succs, scc, implications, is_connected, - bdd2num, num2bdd, scc_opt, use_bisimulation); + bdd2num, num2bdd, scc_opt, use_bisimulation, + use_stutter); for (auto s: succs) { // Don't construct sink state as complete does a better job at this - if (s.first.nodes_.size() == 0) + if (s.first.nodes_.empty()) continue; auto i = seen.find(s.first); unsigned dst_num; diff --git a/spot/twaalgos/safra.hh b/spot/twaalgos/safra.hh index 592ee3623..4205f0ce1 100644 --- a/spot/twaalgos/safra.hh +++ b/spot/twaalgos/safra.hh @@ -63,7 +63,8 @@ namespace spot std::unordered_map& bdd2num, std::vector& all_bdds, bool scc_opt, - bool use_bisimulation) const; + bool use_bisimulation, + bool use_stutter) const; // Compute successor for transition ap safra_state compute_succ(const const_twa_graph_ptr& aut, @@ -107,5 +108,6 @@ namespace spot bool pretty_print = false, bool scc_opt = false, bool use_bisimulation = false, - bool complete = false); + bool complete = false, + bool use_stutter = false); } diff --git a/tests/core/safra.cc b/tests/core/safra.cc index 15de7a24f..60e0aa006 100644 --- a/tests/core/safra.cc +++ b/tests/core/safra.cc @@ -41,6 +41,9 @@ int help() std::cerr << "\t-H\toutput hoa format\n"; std::cerr << "\t-b\treduce result using bisimulation\n"; std::cerr << "\t--scc_opt\tUse an SCC-based Safra\n"; + std::cerr << "\t--bisim_opt\tUse Simulation info to reduce macro-states " + "size\n"; + std::cerr << "\t--stutter\tStutter-invarience optimisation\n"; return 1; } @@ -55,6 +58,7 @@ int main(int argc, char* argv[]) bool out_hoa = false; bool pretty_print = false; bool complete = false; + bool use_stutter = false; char* input = nullptr; if (argc <= 2) @@ -90,6 +94,8 @@ int main(int argc, char* argv[]) scc_opt = true; else if (!strncmp(argv[i], "--bisim_opt", 10)) use_bisim = true; + else if (!strncmp(argv[i], "--stutter", 9)) + use_stutter = true; else { std::cerr << "Warning: " << argv[i] << " not used\n"; @@ -112,7 +118,7 @@ int main(int argc, char* argv[]) trans.set_pref(spot::postprocessor::Deterministic); auto tmp = trans.run(f); res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt, - use_bisim, complete); + use_bisim, complete, use_stutter); } else if (in_hoa) { @@ -120,7 +126,7 @@ int main(int argc, char* argv[]) if (aut->format_errors(std::cerr)) return 2; res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt, - use_bisim, complete); + use_bisim, complete, use_stutter); } res->merge_edges();