From 4635ce44a96dae343e20a93719fc70fadf96c408 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Feb 2016 09:50:48 +0100 Subject: [PATCH] determinize: add some doc * spot/twaalgos/determinize.hh: Add documentaion and rename options. * spot/twaalgos/determinize.cc: Rename options as well. --- spot/twaalgos/determinize.cc | 36 +++++++++++------------ spot/twaalgos/determinize.hh | 55 ++++++++++++++++++++++++++++++++++-- 2 files changed, 70 insertions(+), 21 deletions(-) diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index aa61ce8e7..a042f61d9 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -70,8 +70,8 @@ namespace spot const std::vector& is_connected, std::unordered_map& bdd2num, std::vector& all_bdds, - bool scc_opt, - bool use_bisimulation, + bool use_scc, + bool use_simulation, bool use_stutter) const; // Compute successor for transition ap safra_state @@ -80,8 +80,8 @@ namespace spot const scc_info& scc, const std::map& implications, const std::vector& is_connected, - bool scc_opt, - bool use_bisimulation) const; + bool use_scc, + bool use_simulation) const; // scc_id has to be an accepting SCC. This function tries to find a node // who lives in that SCC and if it does, we return the brace_id of that SCC. unsigned find_scc_brace_id(unsigned scc_id, const scc_info& scc); @@ -268,8 +268,8 @@ namespace spot const scc_info& scc, const std::map& implications, const std::vector& is_connected, - bool scc_opt, - bool use_bisimulation) const + bool use_scc, + bool use_simulation) const { safra_state ss = safra_state(nb_braces_.size()); for (auto& node: nodes_) @@ -280,7 +280,7 @@ namespace spot continue; // Check if we are leaving the SCC, if so we delete all the // braces as no cycles can be found with that node - if (scc_opt && scc.scc_of(node.first) != scc.scc_of(t.dst)) + if (use_scc && scc.scc_of(node.first) != scc.scc_of(t.dst)) if (scc.is_accepting_scc(scc.scc_of(t.dst))) { // Find scc_id in the safra state currently being @@ -304,7 +304,7 @@ namespace spot assert(ss.nb_braces_.size() == ss.is_green_.size()); } } - if (use_bisimulation) + if (use_simulation) ss.merge_redundant_states(implications, scc, is_connected); ss.ungreenify_last_brace(); ss.color_ = ss.finalize_construction(); @@ -320,8 +320,8 @@ namespace spot std::unordered_map& bdd2num, std::vector& all_bdds, - bool scc_opt, - bool use_bisimulation, + bool use_scc, + bool use_simulation, bool use_stutter) const { for (auto& ap: all_bdds) @@ -340,7 +340,7 @@ namespace spot // insert should never fail assert(pair.second); ss = ss.compute_succ(aut, ap, scc, implications, is_connected, - scc_opt, use_bisimulation); + use_scc, use_simulation); colors.push_back(ss.color_); stop = safra2id.find(ss) != safra2id.end(); } @@ -356,7 +356,7 @@ namespace spot } else ss = compute_succ(aut, ap, scc, implications, is_connected, - scc_opt, use_bisimulation); + use_scc, use_simulation); unsigned bdd_idx = bdd2num[ap]; res.emplace_back(ss, bdd_idx); } @@ -608,13 +608,13 @@ namespace spot twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& a, - bool pretty_print, bool scc_opt, - bool use_bisimulation, bool use_stutter) + bool pretty_print, bool use_scc, + bool use_simulation, bool use_stutter) { // Degeneralize twa_graph_ptr aut = spot::degeneralize_tba(a); std::map implications; - if (use_bisimulation) + if (use_simulation) { aut = spot::scc_filter(aut); aut = simulation(aut, &implications); @@ -674,8 +674,8 @@ namespace spot // Required to create new edges from 2 safra-state power_set seen; auto init_state = aut->get_init_state_number(); - bool start_accepting = scc.is_accepting_scc(scc.scc_of(init_state)) || - !scc_opt; + bool start_accepting = + !use_scc || scc.is_accepting_scc(scc.scc_of(init_state)); safra_state init(init_state, true, start_accepting); unsigned num = res->new_state(); res->set_init_state(num); @@ -691,7 +691,7 @@ namespace spot 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, use_scc, use_simulation, use_stutter); for (auto s: succs) { diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index db9234b7b..a4ea68a1f 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -23,10 +23,59 @@ namespace spot { + /// \ingroup twa_algorithms + /// \brief Determinize a TGBA + /// + /// The main algorithm works only with automata using Büchi acceptance + /// (preferably transition-based). If generalized Büchi is input, it + /// will be automatically degeneralized first. + /// + /// The output will be a deterministic automaton using parity acceptance. + /// + /// This procedure is based on an algorithm by Roman Redziejowski + /// (Fundamenta Informaticae 119, 3-4 (2012)). Redziejowski's + /// algorithm is similar to Piterman's improvement of Safra's + /// algorithm, except it is presented on transition-based acceptance + /// and use simpler notations. We implement three additional + /// optimizations (they can be individually disabled) based on + /// + /// - knowledge about SCCs of the input automaton + /// - knowledge about simulation relations in the input automaton + /// - knowledge about stutter-invariance of the input automaton + /// + /// The last optimization is an idea described by Joachim Klein & + /// Christel Baier (CIAA'07) and implemented in ltl2dstar. In fact, + /// ltl2dstar even has a finer version (letter-based stuttering) + /// that is not implemented here. + /// + /// \param aut the automaton to determinize + /// + /// \param pretty_print whether to decorate states with names + /// showing the paths they track (this only + /// makes sense if the input has Büchi + /// acceptance already, otherwise the input + /// automaton will be degeneralized and the + /// names will refer to the states in the + /// degeneralized automaton). + /// + /// \param use_scc whether to simplify the construction based on + /// the SCCs in the input automaton. + /// + /// \param use_simulation whether to simplify the construction based + /// on simulation relations between states in + /// the original automaton. + /// + /// \param use_stutter whether to simplify the construction when the + /// input automaton is known to be + /// stutter-invariant. (The stutter-invariant + /// flag of the input automaton is used, so it + /// might be worth to call + /// spot::check_stutter_invariance() first if + /// possible.) SPOT_API twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& aut, bool pretty_print = false, - bool scc_opt = false, - bool use_bisimulation = false, - bool use_stutter = false); + bool use_scc = true, + bool use_simulation = true, + bool use_stutter = true); }