From 07ab225cc416245cf788d5f148cc34fb0bab4223 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Jul 2013 10:35:23 +0200 Subject: [PATCH] dba_determinize: Add a threshold argument. * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh (dba_determinize, dba_determinize_check): Add a threshold argument. * src/tgbatest/ltl2tgba.cc (-O, -RQ): Accept a threshold argument. --- src/tgbaalgos/powerset.cc | 14 ++++++++++++-- src/tgbaalgos/powerset.hh | 15 +++++++++++++-- src/tgbatest/ltl2tgba.cc | 23 +++++++++++++++++------ 3 files changed, 42 insertions(+), 10 deletions(-) diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 997142eb9..85870268f 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -303,13 +303,19 @@ namespace spot } tgba_explicit_number* - tba_determinize(const tgba* aut) + tba_determinize(const tgba* aut, unsigned threshold) { 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)) + { + delete det; + return 0; + } fix_dba_acceptance(det, aut, pm); det->merge_transitions(); return det; @@ -317,6 +323,7 @@ namespace spot tgba* tba_determinize_check(const tgba* aut, + unsigned threshold, const ltl::formula* f, const tgba* neg_aut) { @@ -326,7 +333,10 @@ namespace spot if (aut->number_of_acceptance_conditions() > 1) return 0; - tgba_explicit_number* det = tba_determinize(aut); + tgba_explicit_number* det = tba_determinize(aut, threshold); + + if (!det) + return 0; if (neg_aut == 0) { diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index afb4245e9..0f9fb4d6b 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -122,8 +122,12 @@ 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. SPOT_API tgba_explicit_number* - tba_determinize(const tgba* aut); + tba_determinize(const tgba* aut, unsigned threshold = 0); /// \brief Determinize a TBA and make sure it is correct. /// @@ -134,15 +138,22 @@ namespace spot /// \a neg_aut is not given, it will be built from \a f. /// /// \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 f the formula represented by the original automaton + /// /// \param neg_aut an automaton representing the negation of \a aut /// /// \return a new tgba if the automaton could be determinized, \a aut if /// the automaton cannot be determinized, 0 if we do not know if the /// determinization is correct because neither \a f nor \a neg_aut /// were supplied. - tgba* + SPOT_API tgba* tba_determinize_check(const tgba* aut, + unsigned threshold = 0, const ltl::formula* f = 0, const tgba* neg_aut = 0); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d425968f2..3d0e77323 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -337,11 +337,13 @@ to_int(const char* s) char* endptr; int res = strtol(s, &endptr, 10); if (*endptr) - return -1; + { + std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl; + exit(1); + } return res; } - int main(int argc, char** argv) { @@ -389,6 +391,8 @@ main(int argc, char** argv) bool opt_reduce = false; bool opt_minimize = false; bool opt_determinize = false; + unsigned opt_determinize_threshold = 0; + unsigned opt_o_threshold = 0; bool opt_dbacomp = false; bool reject_bigger = false; bool opt_bisim_ta = false; @@ -649,10 +653,12 @@ main(int argc, char** argv) output = 8; spin_comments = true; } - else if (!strcmp(argv[formula_index], "-O")) + else if (!strncmp(argv[formula_index], "-O", 2)) { output = 14; opt_minimize = true; + if (argv[formula_index][2] != 0) + opt_o_threshold = to_int(argv[formula_index] + 2); } else if (!strcmp(argv[formula_index], "-p")) { @@ -793,9 +799,11 @@ main(int argc, char** argv) opt_minimize = true; reject_bigger = true; } - else if (!strcmp(argv[formula_index], "-RQ")) + else if (!strncmp(argv[formula_index], "-RQ", 3)) { opt_determinize = true; + if (argv[formula_index][3] != 0) + opt_determinize_threshold = to_int(argv[formula_index] + 3); } else if (!strcmp(argv[formula_index], "-RT")) { @@ -1443,8 +1451,10 @@ main(int argc, char** argv) && (!f || f->is_syntactic_recurrence())) { tm.start("determinization"); - a = determinized = tba_determinize(a); + determinized = tba_determinize(a, opt_determinize_threshold); tm.stop("determinization"); + if (determinized) + a = determinized; } spot::tgba* complemented = 0; @@ -1702,7 +1712,8 @@ main(int argc, char** argv) if (minimized == 0) { std::cout << "this is not an obligation property"; - const spot::tgba* tmp = tba_determinize_check(a, f); + const spot::tgba* tmp = + tba_determinize_check(a, opt_o_threshold, f, 0); if (tmp != 0 && tmp != a) { std::cout << ", but it is a recurrence property";