diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 18c3cdcdb..ca48e7e69 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -224,16 +224,24 @@ namespace spot && sim->number_of_acceptance_conditions() > 1) tmpd = new tgba_tba_proxy(sim); - // This threshold is arbitrary. For producing Small automata, - // we assume that a deterministic automaton that is twice the - // size of the original will never get reduced to a smaller - // one. For Deterministic automata, we accept automata that - // are 4 times bigger. The larger the value, the more likely - // the cycle enumeration algorithm will encounter an automaton - // that takes *eons* to explore. const tgba* in = tmpd ? tmpd : sim; + + // These thresholds is arbitrary. + // + // For producing Small automata, we assume that a + // deterministic automaton that is twice the size of the + // original will never get reduced to a smaller one. We also + // do not want more than 2^13 cycles in an SCC. + // + // For Deterministic automata, we accept automata that + // are 8 times bigger, with no more that 2^15 cycle per SCC. + // The cycle threshold is the most important limit here. You + // may up it if you want to try producing larger automata. const tgba* tmp = - tba_determinize_check(in, (pref_ == Small) ? 2 : 4, f); + tba_determinize_check(in, + (pref_ == Small) ? 2 : 8, + 1 << ((pref_ == Small) ? 13 : 15), + f); if (tmp != 0 && tmp != in) { // There is no point in running the reverse simulation on diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 85870268f..d09631b1c 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -143,20 +143,25 @@ namespace spot protected: const tgba* ref_; power_map& refmap_; - trans_set reject_; // set of rejecting transitions - set_set accept_; // set of cycles that are accepting - trans_set all_; // all non rejecting transitions + trans_set reject_; // set of rejecting transitions + set_set accept_; // set of cycles that are accepting + trans_set all_; // all non rejecting transitions + unsigned threshold_; // maximum count of enumerated cycles + unsigned cycles_left_; // count of cycles left to explore public: - fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap) - : enumerate_cycles(sm), ref_(ref), refmap_(refmap) + fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap, + unsigned threshold) + : enumerate_cycles(sm), ref_(ref), refmap_(refmap), + threshold_(threshold) { } - void fix_scc(const int m) + bool fix_scc(const int m) { reject_.clear(); accept_.clear(); + cycles_left_ = threshold_; run(m); // std::cerr << "SCC #" << m << "\n"; @@ -176,6 +181,7 @@ namespace spot { (*i)->acceptance_conditions = acc; } + return threshold_ != 0 && cycles_left_ == 0; } bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const @@ -279,13 +285,17 @@ namespace spot } } - return true; + // Abort this algorithm if we have seen too much cycles, i.e., + // when cycle_left_ *reaches* 0. (If cycle_left_ == 0, that + // means we had no limit.) + return (cycles_left_ == 0) || --cycles_left_; } }; - static void + static bool fix_dba_acceptance(tgba_explicit_number* det, - const tgba* ref, power_map& refmap) + const tgba* ref, power_map& refmap, + unsigned threshold) { det->copy_acceptance_conditions_of(ref); @@ -294,36 +304,45 @@ namespace spot unsigned scc_count = sm.scc_count(); - fix_scc_acceptance fsa(sm, ref, refmap); + fix_scc_acceptance fsa(sm, ref, refmap, threshold); for (unsigned m = 0; m < scc_count; ++m) - fsa.fix_scc(m); + if (!sm.trivial(m)) + if (fsa.fix_scc(m)) + return true; + return false; } - } tgba_explicit_number* - tba_determinize(const tgba* aut, unsigned threshold) + tba_determinize(const tgba* aut, + unsigned threshold_states, unsigned threshold_cycles) { power_map pm; // Do not merge transitions in the deterministic automaton. If we // add two self-loops labeled by "a" and "!a", we do not want // these to be merged as "1" before the acceptance has been fixed. tgba_explicit_number* det = tgba_powerset(aut, pm, false); - if ((threshold > 0) - && (pm.map_.size() > pm.states.size() * threshold)) + + if ((threshold_states > 0) + && (pm.map_.size() > pm.states.size() * threshold_states)) + { + delete det; + return 0; + } + if (fix_dba_acceptance(det, aut, pm, threshold_cycles)) { delete det; return 0; } - fix_dba_acceptance(det, aut, pm); det->merge_transitions(); return det; } tgba* tba_determinize_check(const tgba* aut, - unsigned threshold, + unsigned threshold_states, + unsigned threshold_cycles, const ltl::formula* f, const tgba* neg_aut) { @@ -333,7 +352,8 @@ namespace spot if (aut->number_of_acceptance_conditions() > 1) return 0; - tgba_explicit_number* det = tba_determinize(aut, threshold); + tgba_explicit_number* det = + tba_determinize(aut, threshold_states, threshold_cycles); if (!det) return 0; diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 0f9fb4d6b..3c5bdb63c 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -123,11 +123,18 @@ namespace spot /// \endverbatim /// only adapted to work on TBA rather than BA. /// - /// If \a threshold is non null, abort the construction whenever it - /// would build an automaton that is more than \a threshold time - /// bigger (in term of states) than the original automaton. + /// If \a threshold_states is non null, abort the construction + /// whenever it would build an automaton that is more than \a + /// threshold_states time bigger (in term of states) than the + /// original automaton. + /// + /// If \a threshold_cycles is non null, abort the construction + /// whenever an SCC of the constructed automaton has more than \a + /// threshold_cycles cycles. SPOT_API tgba_explicit_number* - tba_determinize(const tgba* aut, unsigned threshold = 0); + tba_determinize(const tgba* aut, + unsigned threshold_states = 0, + unsigned threshold_cycles = 0); /// \brief Determinize a TBA and make sure it is correct. /// @@ -139,9 +146,14 @@ namespace spot /// /// \param aut the automaton to minimize /// - /// \param threshold if non null, abort the construction whenever it - /// would build an automaton that is more than \a threshold time - /// bigger (in term of states) than the original automaton. + /// \param threshold_states if non null, abort the construction + /// whenever it would build an automaton that is more than \a + /// threshold time bigger (in term of states) than the original + /// automaton. + /// + /// \param threshold_cycles can be used to abort the construction + /// if the number of cycles in a SCC of the constructed automaton + /// is bigger than the supplied value. /// /// \param f the formula represented by the original automaton /// @@ -153,7 +165,8 @@ namespace spot /// were supplied. SPOT_API tgba* tba_determinize_check(const tgba* aut, - unsigned threshold = 0, + unsigned threshold_states = 0, + unsigned threshold_cycles = 0, const ltl::formula* f = 0, const tgba* neg_aut = 0); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3d0e77323..301786329 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1451,7 +1451,7 @@ main(int argc, char** argv) && (!f || f->is_syntactic_recurrence())) { tm.start("determinization"); - determinized = tba_determinize(a, opt_determinize_threshold); + determinized = tba_determinize(a, 0, opt_determinize_threshold); tm.stop("determinization"); if (determinized) a = determinized; @@ -1713,7 +1713,7 @@ main(int argc, char** argv) { std::cout << "this is not an obligation property"; const spot::tgba* tmp = - tba_determinize_check(a, opt_o_threshold, f, 0); + tba_determinize_check(a, 0, opt_o_threshold, f, 0); if (tmp != 0 && tmp != a) { std::cout << ", but it is a recurrence property";