diff --git a/ChangeLog b/ChangeLog index 4b461d577..07f841064 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2004-05-25 Alexandre Duret-Lutz + * src/ltlvisit/reducform.hh (option): Rename as ... + (reduce_options): ... this, and use it as a bit field so + option can be combined easily. + (reduce): Adjust argument. + (reduce_form): Remove, not needed anymore. + * src/ltlvisit/reducform.cc, src/ltltest/reduc.cc, + src/tgbatest/ltl2tgba.cc: Adjust. + * src/sanity/style.test: Catch {.*{ and }.*}. * src/sanity/80columns.test: Untabify files. * iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines. diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index f4a9dbc3d..d7b72c96f 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -44,29 +44,31 @@ main(int argc, char** argv) if (argc < 3) syntax(argv[0]); - spot::ltl::option o; + int o = spot::ltl::Reduce_None; switch (atoi(argv[1])) { case 0: - o = spot::ltl::Base; + o = spot::ltl::Reduce_Basics; break; case 1: - o = spot::ltl::Inf; + o = spot::ltl::Reduce_Syntactic_Implications; break; case 2: - o = spot::ltl::EventualUniversal; + o = spot::ltl::Reduce_Eventuality_And_Universality; break; case 3: - o = spot::ltl::BRI; + o = spot::ltl::Reduce_All; break; case 4: - o = spot::ltl::InfBase; + o = spot::ltl::Reduce_Basics | spot::ltl::Reduce_Syntactic_Implications; break; case 5: - o = spot::ltl::EventualUniversalBase; + o = (spot::ltl::Reduce_Basics + | spot::ltl::Reduce_Eventuality_And_Universality); break; case 6: - o = spot::ltl::InfEventualUniversal; + o = (spot::ltl::Reduce_Syntactic_Implications + | spot::ltl::Reduce_Eventuality_And_Universality); break; default: return 2; diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index 455fdfc91..ed15ae029 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -36,9 +36,9 @@ namespace spot { public: - reduce_form_visitor(option o) + reduce_form_visitor(int opt) + : opt_(opt) { - this->o = o; } virtual ~reduce_form_visitor() @@ -61,17 +61,7 @@ namespace spot void visit(constant* c) { - switch (c->val()) - { - case constant::True: - result_ = constant::true_instance(); - return; - case constant::False: - result_ = constant::false_instance(); - return; - } - /* Unreachable code. */ - assert(0); + result_ = c; } void @@ -90,14 +80,16 @@ namespace spot return; case unop::F: - /* If f is class of eventuality then F(f)=f. */ - if (!is_eventual(result_) || o == Inf || o == InfBase) + /* If f is a pure eventuality formula then F(f)=f. */ + if (!(opt_ & Reduce_Eventuality_And_Universality) + || !is_eventual(result_)) result_ = unop::instance(unop::F, result_); return; case unop::G: - /* If f is class of universality then G(f)=f. */ - if (!is_universal(result_) || o == Inf || o == InfBase) + /* If f is a pure universality formula then G(f)=f. */ + if (!(opt_ & Reduce_Eventuality_And_Universality) + || !is_universal(result_)) result_ = unop::instance(unop::G, result_); return; } @@ -110,9 +102,9 @@ namespace spot { formula* f2 = recurse(bo->second()); - /* If b is of class eventuality then a U b = b. - If b is of class universality then a R b = b. */ - if ((o != Inf) && (o != InfBase) + /* If b is a pure eventuality formula then a U b = b. + If b is a pure universality formula a R b = b. */ + if ((opt_ & Reduce_Eventuality_And_Universality) && ((is_eventual(f2) && ((bo->op()) == binop::U)) || (is_universal(f2) && ((bo->op()) == binop::R)))) { @@ -122,7 +114,7 @@ namespace spot /* case of implies */ formula* f1 = recurse(bo->first()); - if (o != EventualUniversal && o != EventualUniversalBase) + if (opt_ & Reduce_Syntactic_Implications) { bool inf = inf_form(f1, f2); bool infinv = inf_form(f2, f1); @@ -206,7 +198,7 @@ namespace spot for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); - if (o != EventualUniversal && o != EventualUniversalBase) + if (opt_ & Reduce_Syntactic_Implications) { switch (mo->op()) { @@ -297,82 +289,52 @@ namespace spot formula* recurse(formula* f) { - return reduce_form(f, o); + return reduce(f, opt_); } protected: formula* result_; - option o; + int opt_; }; formula* - reduce_form(const formula* f, option o) + reduce(const formula* f, int opt) { - formula* ftmp1 = NULL; - formula* ftmp2 = NULL; - reduce_form_visitor v(o); + formula* f1; + formula* f2; - if (o == BRI || o == InfBase || - o == EventualUniversalBase) + f1 = unabbreviate_logic(f); + f2 = negative_normal_form(f1); + destroy(f1); + + if (opt & Reduce_Basics) { - ftmp1 = basic_reduce_form(f); - const_cast(ftmp1)->accept(v); - ftmp2 = basic_reduce_form(v.result()); - destroy(ftmp1); - destroy(v.result()); - - return ftmp2; + f1 = basic_reduce_form(f2); + destroy(f2); + f2 = f1; } - else + if (opt & (Reduce_Syntactic_Implications + | Reduce_Eventuality_And_Universality)) { - const_cast(f)->accept(v); - return v.result(); + reduce_form_visitor v(opt); + f2->accept(v); + f1 = v.result(); + destroy(f2); + f2 = f1; + + // Run basic_reduce_form again. + // + // Consider `F b & g' were g is an eventual formula rewritten + // as `g = F c' Then basic_reduce_form with rewrite it + // as F(b & c). + if (opt & Reduce_Basics) + { + f1 = basic_reduce_form(f2); + destroy(f2); + f2 = f1; + } } - - /* unreachable code */ - assert(0); - } - - formula* - reduce(const formula* f, option o) - { - formula* ftmp1; - formula* ftmp2; - formula* ftmp3; - - ftmp1 = unabbreviate_logic(f); - ftmp2 = negative_normal_form(ftmp1); - - switch (o) - { - case Base: - ftmp3 = basic_reduce_form(ftmp2); - break; - case Inf: - ftmp3 = reduce_form(ftmp2, o); - break; - case InfBase: - ftmp3 = reduce_form(ftmp2, o); - break; - case EventualUniversal: - ftmp3 = reduce_form(ftmp2, o); - break; - case EventualUniversalBase: - ftmp3 = reduce_form(ftmp2, o); - break; - case InfEventualUniversal: - ftmp3 = reduce_form(ftmp2, o); - break; - case BRI: - ftmp3 = reduce_form(ftmp2, o); - break; - default: - assert(0); - } - destroy(ftmp1); - destroy(ftmp2); - - return ftmp3; + return f2; } } } diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh index 3151f6349..84dcfd1f4 100644 --- a/src/ltlvisit/reducform.hh +++ b/src/ltlvisit/reducform.hh @@ -29,13 +29,15 @@ namespace spot { namespace ltl { - enum option {Base, - Inf, - InfBase, - EventualUniversal, - EventualUniversalBase, - InfEventualUniversal, - BRI}; + + enum reduce_options + { + Reduce_None = 0, + Reduce_Basics = 1, + Reduce_Syntactic_Implications = 2, + Reduce_Eventuality_And_Universality = 4, + Reduce_All = -1U + }; /// \brief Reduce a formula \a f using Basic rewriting, implies /// relation, and class of eventuality and univerality formula. @@ -47,15 +49,11 @@ namespace spot /// Inf for spot::ltl::reduce_inf_form, /// EventualUniversal for spot::ltl::reduce_eventuality_universality_form, /// BRI for spot::ltl::reduce_form. - formula* reduce(const formula* f, option opt = BRI); + formula* reduce(const formula* f, int opt = Reduce_All); /// Implement basic rewriting. formula* basic_reduce_form(const formula* f); - /// Implement rewritings rules using implies relation, - /// and class of eventuality and univerality formula. - formula* reduce_form(const formula* f, option o = BRI); - /// Detect easy case of implies. /// True if f1 < f2, false otherwise. bool inf_form(const formula* f1, const formula* f2); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 89ecd3d32..85a77e712 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -120,10 +120,7 @@ main(int argc, char** argv) bool magic_many = false; bool expect_counter_example = false; bool from_file = false; - bool reduc_r1 = false; - bool reduc_r2 = false; - bool reduc_r3 = false; - bool reduc_r4 = false; + int redopt = spot::ltl::Reduce_None; bool post_branching = false; bool fair_loop_approx = false; @@ -223,6 +220,22 @@ main(int argc, char** argv) { output = 1; } + else if (!strcmp(argv[formula_index], "-r1")) + { + redopt |= spot::ltl::Reduce_Basics; + } + else if (!strcmp(argv[formula_index], "-r2")) + { + redopt |= spot::ltl::Reduce_Syntactic_Implications; + } + else if (!strcmp(argv[formula_index], "-r3")) + { + redopt |= spot::ltl::Reduce_Eventuality_And_Universality; + } + else if (!strcmp(argv[formula_index], "-r4")) + { + redopt |= spot::ltl::Reduce_All; + } else if (!strcmp(argv[formula_index], "-R")) { output = 3; @@ -261,22 +274,6 @@ main(int argc, char** argv) fm_opt = true; fm_symb_merge_opt = false; } - else if (!strcmp(argv[formula_index], "-r1")) - { - reduc_r1 = true; - } - else if (!strcmp(argv[formula_index], "-r2")) - { - reduc_r2 = true; - } - else if (!strcmp(argv[formula_index], "-r3")) - { - reduc_r3 = true; - } - else if (!strcmp(argv[formula_index], "-r4")) - { - reduc_r4 = true; - } else { break; @@ -339,29 +336,11 @@ main(int argc, char** argv) } else { - - spot::ltl::formula* ftmp = f; - if (reduc_r4) + if (redopt != spot::ltl::Reduce_None) { - f = spot::ltl::reduce(f); - } - else if (reduc_r1 | reduc_r2 | reduc_r3) - { - spot::ltl::option o = spot::ltl::BRI; - if (reduc_r1 & !reduc_r2 & !reduc_r3) - o = spot::ltl::Base; - if (!reduc_r1 & reduc_r2 & !reduc_r3) - o = spot::ltl::EventualUniversal; - if (reduc_r1 & reduc_r2 & !reduc_r3) - o = spot::ltl::EventualUniversalBase; - if (!reduc_r1 & !reduc_r2 & reduc_r3) - o = spot::ltl::Inf; - if (reduc_r1 & !reduc_r2 & reduc_r3) - o = spot::ltl::InfBase; - if (!reduc_r1 & reduc_r2 & reduc_r3) - o = spot::ltl::InfEventualUniversal; - - f = spot::ltl::reduce(f, o); + spot::ltl::formula* t = spot::ltl::reduce(f, redopt); + spot::ltl::destroy(f); + f = t; } if (fm_opt) @@ -371,11 +350,6 @@ main(int argc, char** argv) fair_loop_approx); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); - - if (reduc_r1 || reduc_r2 || reduc_r3 || reduc_r4) - { - spot::ltl::destroy(ftmp); - } } spot::tgba_tba_proxy* degeneralized = 0;