diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index fc15d31db..f775b7b11 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -23,7 +23,6 @@ #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "ltlvisit/reduce.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/minimize.hh" @@ -221,7 +220,9 @@ main(int argc, char **argv) tm.start("reducing formula"); { - spot::ltl::formula* r = spot::ltl::reduce(f); + spot::ltl::ltl_simplifier_options opt(true, true, true, true, true); + spot::ltl::ltl_simplifier simp(opt); + spot::ltl::formula* r = simp.simplify(f); f->destroy(); f = r; } diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 987e525d6..62ece4878 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -32,7 +32,7 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/contain.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" #include "ltlvisit/tostring.hh" void @@ -94,26 +94,38 @@ main(int argc, char** argv) std::cout << std::endl; #endif #ifdef REDUC - spot::ltl::formula* tmp; - tmp = f1; - f1 = spot::ltl::reduce(f1); - tmp->destroy(); + { + spot::ltl::ltl_simplifier_options opt(true, true, true, false, false); + spot::ltl::ltl_simplifier simp(opt); + spot::ltl::formula* tmp; + tmp = f1; + f1 = simp.simplify(f1); + tmp->destroy(); + } spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif #ifdef REDUC_TAU - spot::ltl::formula* tmp; - tmp = f1; - f1 = spot::ltl::reduce_tau03(f1, false); - tmp->destroy(); + { + spot::ltl::ltl_simplifier_options opt(false, false, false, true, false); + spot::ltl::ltl_simplifier simp(opt); + spot::ltl::formula* tmp; + tmp = f1; + f1 = simp.simplify(f1); + tmp->destroy(); + } spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif #ifdef REDUC_TAUSTR - spot::ltl::formula* tmp; - tmp = f1; - f1 = spot::ltl::reduce_tau03(f1, true); - tmp->destroy(); + { + spot::ltl::ltl_simplifier_options opt(false, false, false, true, true); + spot::ltl::ltl_simplifier simp(opt); + spot::ltl::formula* tmp; + tmp = f1; + f1 = simp.simplify(f1); + tmp->destroy(); + } spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 62a89fcba..e7a0df1b5 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -31,7 +31,7 @@ #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/length.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" #include "ltlenv/defaultenv.hh" #include "misc/random.hh" @@ -97,6 +97,8 @@ main(int argc, char** argv) char* opt_pB = 0; int opt_r = 0; bool opt_u = false; + spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true); + spot::ltl::ltl_simplifier simp(simpopt); spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; @@ -308,7 +310,7 @@ main(int argc, char** argv) f = rf->generate(opt_f); if (opt_r) { - spot::ltl::formula* g = reduce(f); + spot::ltl::formula* g = simp.simplify(f); f->destroy(); if (spot::ltl::length(g) < opt_r) { diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 14eb66337..f20c8a1a2 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -28,14 +28,10 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/lunabbrev.hh" -#include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/nenoform.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" #include "ltlvisit/length.hh" -#include "ltlvisit/contain.hh" #include "ltlast/allnodes.hh" void @@ -52,6 +48,7 @@ main(int argc, char** argv) bool hidereduc = false; unsigned long sum_before = 0; unsigned long sum_after = 0; + spot::ltl::ltl_simplifier_options o(false, false, false, false, false); if (argc < 3) syntax(argv[0]); @@ -70,69 +67,81 @@ main(int argc, char** argv) --argc; } - int o = spot::ltl::Reduce_None; switch (atoi(argv[1])) { case 0: - o = spot::ltl::Reduce_Basics; + o.reduce_basics = true; break; case 1: - o = spot::ltl::Reduce_Syntactic_Implications; + o.synt_impl = true; break; case 2: - o = spot::ltl::Reduce_Eventuality_And_Universality; + o.event_univ = true; break; case 3: - o = spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Syntactic_Implications - | spot::ltl::Reduce_Eventuality_And_Universality; + o.reduce_basics = true; + o.synt_impl = true; + o.event_univ = true; break; case 4: - o = spot::ltl::Reduce_Basics | spot::ltl::Reduce_Syntactic_Implications; + o.reduce_basics = true; + o.synt_impl = true; break; case 5: - o = (spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Eventuality_And_Universality); + o.reduce_basics = true; + o.event_univ = true; break; case 6: - o = (spot::ltl::Reduce_Syntactic_Implications - | spot::ltl::Reduce_Eventuality_And_Universality); + o.synt_impl = true; + o.event_univ = true; break; case 7: - o = spot::ltl::Reduce_Containment_Checks; + o.containment_checks = true; break; case 8: - o = spot::ltl::Reduce_Containment_Checks_Stronger; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 9: - o = spot::ltl::Reduce_All; + o.reduce_basics = true; + o.synt_impl = true; + o.event_univ = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 10: - o = (spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Containment_Checks_Stronger); + o.reduce_basics = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 11: - o = (spot::ltl::Reduce_Syntactic_Implications - | spot::ltl::Reduce_Containment_Checks_Stronger); + o.synt_impl = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 12: - o = (spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Syntactic_Implications - | spot::ltl::Reduce_Containment_Checks_Stronger); + o.reduce_basics = true; + o.synt_impl = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 13: - o = (spot::ltl::Reduce_Eventuality_And_Universality - | spot::ltl::Reduce_Containment_Checks_Stronger); + o.event_univ = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; case 14: - o = (spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Eventuality_And_Universality - | spot::ltl::Reduce_Containment_Checks_Stronger); + o.reduce_basics = true; + o.event_univ = true; + o.containment_checks = true; + o.containment_checks_stronger = true; break; default: return 2; } + spot::ltl::ltl_simplifier* simp = new spot::ltl::ltl_simplifier(o); + spot::ltl::formula* f1 = 0; spot::ltl::formula* f2 = 0; @@ -191,25 +200,17 @@ main(int argc, char** argv) { spot::ltl::formula* ftmp1; - spot::ltl::formula* ftmp2; ftmp1 = f1; - f1 = unabbreviate_logic(f1); - ftmp2 = f1; - f1 = negative_normal_form(f1); + f1 = simp->negative_normal_form(f1, false, true); ftmp1->destroy(); - ftmp2->destroy(); - int length_f1_before = spot::ltl::length(f1); std::string f1s_before = spot::ltl::to_string(f1); ftmp1 = f1; - f1 = spot::ltl::reduce(f1, o); - ftmp2 = f1; - f1 = spot::ltl::unabbreviate_logic(f1); + f1 = simp->simplify(f1); ftmp1->destroy(); - ftmp2->destroy(); int length_f1_after = spot::ltl::length(f1); std::string f1s_after = spot::ltl::to_string(f1); @@ -218,13 +219,7 @@ main(int argc, char** argv) if (f2) { ftmp1 = f2; - f2 = unabbreviate_logic(f2); - ftmp2 = f2; - f2 = negative_normal_form(f2); - ftmp1->destroy(); - ftmp2->destroy(); - ftmp1 = f2; - f2 = unabbreviate_logic(f2); + f2 = simp->negative_normal_form(f2, false, true); ftmp1->destroy(); f2s = spot::ltl::to_string(f2); } @@ -278,6 +273,8 @@ main(int argc, char** argv) } end: + delete simp; + if (fin) { float before = sum_before; diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 116cdcb2a..488bc1e26 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -21,9 +21,10 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "reduce.hh" #include #include "simplify.hh" +#define SKIP_DEPRECATED_WARNING +#include "reduce.hh" namespace spot { diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index 7047666f4..628603be9 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -27,6 +27,13 @@ #include "ltlast/formula.hh" #include "ltlast/visitor.hh" +#if __GNUC__ +#ifndef SKIP_DEPRECATED_WARNING +#warning This file and its functions are deprecated. \ + The functionality moved to ltlvisit/simplify.hh +#endif +#endif + namespace spot { namespace ltl @@ -60,7 +67,14 @@ namespace spot /// \param opt a conjonction of spot::ltl::reduce_options specifying /// which optimizations to apply. /// \return the reduced formula + /// + /// \deprecated Use spot::ltl::ltl_simplifier instead. +#if __GNUC__ + formula* + reduce(const formula* f, int opt = Reduce_All) __attribute__ ((deprecated)); +#else formula* reduce(const formula* f, int opt = Reduce_All); +#endif /// @} /// \brief Check whether a formula is a pure eventuality. diff --git a/src/sanity/includes.test b/src/sanity/includes.test index a6fc795c8..5e84ef5d3 100755 --- a/src/sanity/includes.test +++ b/src/sanity/includes.test @@ -30,7 +30,7 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \ #include <$file> #include <$file> EOF - if $CXX $CPPFLAGS $CXXFLAGS -c incltest.cc; then + if $CXX $CPPFLAGS -DSKIP_DEPRECATED_WARNING $CXXFLAGS -c incltest.cc; then echo "PASS: $file" else echo "FAIL: $file" diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 0a470dd66..6d74ecfe3 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -27,7 +27,6 @@ #include "misc/minato.hh" #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/postfix.hh" @@ -1588,22 +1587,25 @@ namespace spot ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, - int reduce_ltl) + ltl_simplifier* simplifier) { - // Normalize the formula. We want all the negations on - // the atomic propositions. We also suppress logic - // abbreviations such as <=>, =>, or XOR, since they - // would involve negations at the BDD level. - formula* f1 = unabbreviate_logic(f); - formula* f2 = negative_normal_form(f1); - f1->destroy(); + formula* f2; // Simplify the formula, if requested. - if (reduce_ltl) + if (simplifier) { - formula* tmp = reduce(f2, reduce_ltl); - f2->destroy(); - f2 = tmp; + // This will normalize the formula regardless of the + // configuration of the simplifier. + f2 = simplifier->simplify(f); + } + else + { + // Otherwise, at least normalize the formula. We want all the + // negations on the atomic propositions. We also suppress + // logic abbreviations such as <=>, =>, or XOR, since they + // would involve negations at the BDD level. + ltl_simplifier s; + f2 = s.negative_normal_form(f, false, true); } typedef std::set set_type; @@ -1611,7 +1613,7 @@ namespace spot translate_dict d(dict); - // Compute the set of all promises that can possibly occurre + // Compute the set of all promises that can possibly occur // inside the formula. bdd all_promises = bddtrue; if (fair_loop_approx || unobs) @@ -1761,9 +1763,9 @@ namespace spot const formula* dest = d.conj_bdd_to_formula(dest_bdd); // Simplify the formula, if requested. - if (reduce_ltl) + if (simplifier) { - formula* tmp = reduce(dest, reduce_ltl); + formula* tmp = simplifier->simplify(dest); dest->destroy(); dest = tmp; // Ignore the arc if the destination reduces to false. diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 4c32a70a7..cfa82ec18 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -27,7 +27,7 @@ #include "ltlast/formula.hh" #include "tgba/tgbaexplicit.hh" #include "ltlvisit/apcollect.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" namespace spot { @@ -99,10 +99,10 @@ namespace spot /// formula are observable events, and \c unobs can be filled with /// additional unobservable events. /// - /// \param reduce_ltl If this parameter is set, the LTL formulae representing - /// each state of the automaton will be simplified using spot::ltl::reduce() - /// before computing the successor. \a reduce_ltl should specify the type - /// of reduction to apply as documented for spot::ltl::reduce(). + /// \param simpl If this parameter is set, the LTL formulae representing + /// each state of the automaton will be simplified + /// before computing the successor. \a simpl should be configured + /// for the type of reduction you want, see spot::ltl::ltl_simplifier. /// This idea is taken from the following paper. /// \verbatim /// @InProceedings{ thirioux.02.fmics, @@ -128,7 +128,7 @@ namespace spot bool branching_postponement = false, bool fair_loop_approx = false, const ltl::atomic_prop_set* unobs = 0, - int reduce_ltl = ltl::Reduce_None); + ltl::ltl_simplifier* simplifier = 0); } #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index be3729264..d3bcb0691 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -132,13 +132,8 @@ syntax(char* prog) << std::endl << "Options for Couvreur's FM algorithm (-f):" << std::endl - << " -fr1 use -r1 (see below) at each step of FM" << std::endl - << " -fr2 use -r2 (see below) at each step of FM" << std::endl - << " -fr3 use -r3 (see below) at each step of FM" << std::endl - << " -fr4 use -r4 (see below) at each step of FM" << std::endl - << " -fr5 use -r5 (see below) at each step of FM" << std::endl - << " -fr6 use -r6 (see below) at each step of FM" << std::endl - << " -fr7 use -r7 (see below) at each step of FM" << std::endl + << " -fr reduce formula at each step of FM" << std::endl + << " as specified with the -r{1..7} options" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -p branching postponement (implies -f)" << std::endl << " -U[PROPS] consider atomic properties of the formula as " @@ -291,7 +286,7 @@ main(int argc, char** argv) enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled; enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA } translation = TransFM; - int fm_red = spot::ltl::Reduce_None; + bool fm_red = false; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; bool file_opt = false; @@ -305,8 +300,9 @@ main(int argc, char** argv) bool accepting_run_replay = false; bool from_file = false; bool read_neverclaim = false; - int redopt = spot::ltl::Reduce_None; bool scc_filter = false; + bool simpltl = false; + spot::ltl::ltl_simplifier_options redopt(false, false, false, false, false); bool scc_filter_all = false; bool symbolic_scc_pruning = false; bool display_reduce_form = false; @@ -422,42 +418,10 @@ main(int argc, char** argv) { translation = TransFM; } - else if (!strcmp(argv[formula_index], "-fr1")) + else if (!strcmp(argv[formula_index], "-fr")) { + fm_red = true; translation = TransFM; - fm_red |= spot::ltl::Reduce_Basics; - } - else if (!strcmp(argv[formula_index], "-fr2")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_Eventuality_And_Universality; - } - else if (!strcmp(argv[formula_index], "-fr3")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_Syntactic_Implications; - } - else if (!strcmp(argv[formula_index], "-fr4")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Eventuality_And_Universality - | spot::ltl::Reduce_Syntactic_Implications; - } - else if (!strcmp(argv[formula_index], "-fr5")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_Containment_Checks; - } - else if (!strcmp(argv[formula_index], "-fr6")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger; - } - else if (!strcmp(argv[formula_index], "-fr7")) - { - translation = TransFM; - fm_red |= spot::ltl::Reduce_All; } else if (!strcmp(argv[formula_index], "-F")) { @@ -578,33 +542,45 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-r1")) { - redopt |= spot::ltl::Reduce_Basics; + simpltl = true; + redopt.reduce_basics = true; } else if (!strcmp(argv[formula_index], "-r2")) { - redopt |= spot::ltl::Reduce_Eventuality_And_Universality; + simpltl = true; + redopt.event_univ = true; } else if (!strcmp(argv[formula_index], "-r3")) { - redopt |= spot::ltl::Reduce_Syntactic_Implications; + simpltl = true; + redopt.synt_impl = true; } else if (!strcmp(argv[formula_index], "-r4")) { - redopt |= spot::ltl::Reduce_Basics - | spot::ltl::Reduce_Eventuality_And_Universality - | spot::ltl::Reduce_Syntactic_Implications; + simpltl = true; + redopt.reduce_basics = true; + redopt.event_univ = true; + redopt.synt_impl = true; } else if (!strcmp(argv[formula_index], "-r5")) { - redopt |= spot::ltl::Reduce_Containment_Checks; + simpltl = true; + redopt.containment_checks = true; } else if (!strcmp(argv[formula_index], "-r6")) { - redopt |= spot::ltl::Reduce_Containment_Checks_Stronger; + simpltl = true; + redopt.containment_checks = true; + redopt.containment_checks_stronger = true; } else if (!strcmp(argv[formula_index], "-r7")) { - redopt |= spot::ltl::Reduce_All; + simpltl = true; + redopt.reduce_basics = true; + redopt.event_univ = true; + redopt.synt_impl = true; + redopt.containment_checks = true; + redopt.containment_checks_stronger = true; } else if (!strcmp(argv[formula_index], "-R")) { @@ -794,6 +770,7 @@ main(int argc, char** argv) break; } } + if (f || from_file) { const spot::tgba_bdd_concrete* concrete = 0; @@ -835,10 +812,14 @@ main(int argc, char** argv) } else { - if (redopt != spot::ltl::Reduce_None) + spot::ltl::ltl_simplifier* simp = 0; + if (simpltl) + simp = new spot::ltl::ltl_simplifier(redopt); + + if (simp) { tm.start("reducing formula"); - spot::ltl::formula* t = spot::ltl::reduce(f, redopt); + spot::ltl::formula* t = simp->simplify(f); f->destroy(); tm.stop("reducing formula"); f = t; @@ -855,7 +836,7 @@ main(int argc, char** argv) post_branching, fair_loop_approx, unobservables, - fm_red); + fm_red ? simp : 0); break; case TransTAA: a = spot::ltl_to_taa(f, dict, containment); @@ -870,6 +851,8 @@ main(int argc, char** argv) } tm.stop("translating formula"); to_free = a; + + delete simp; } if (opt_monitor && !scc_filter) diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 0b26eeaa1..f9b7617b3 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -36,7 +36,7 @@ #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/length.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" @@ -488,7 +488,9 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string s) } spot::ltl::formula* -generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, +generate_formula(const spot::ltl::random_ltl& rl, + spot::ltl::ltl_simplifier& simp, + int opt_f, int opt_s, int opt_l = 0, bool opt_u = false) { static std::set unique; @@ -504,7 +506,7 @@ generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, f = rl.generate(opt_f); if (opt_l) { - spot::ltl::formula* g = reduce(f); + spot::ltl::formula* g = simp.simplify(f); f->destroy(); if (spot::ltl::length(g) < opt_l) { @@ -586,6 +588,9 @@ main(int argc, char** argv) spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true); + spot::ltl::ltl_simplifier simp(simpopt); + if (argc <= 1) syntax(argv[0]); @@ -848,7 +853,8 @@ main(int argc, char** argv) { if (opt_F) { - spot::ltl::formula* f = generate_formula(rl, opt_f, opt_ec_seed, + spot::ltl::formula* f = generate_formula(rl, simp, + opt_f, opt_ec_seed, opt_l, opt_u); if (!f) exit(1); diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc new file mode 100644 index 000000000..f60d79b84 --- /dev/null +++ b/src/tgbatest/reductgba.cc @@ -0,0 +1,179 @@ +// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include + +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/reductgba_sim.hh" +#include "tgba/tgbareduc.hh" + +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/ltl2tgba_lacim.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgba/bddprint.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgba/tgbatba.hh" +#include "tgbaalgos/magic.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/gtec/ce.hh" +#include "tgbaparse/public.hh" +#include "tgbaalgos/dupexp.hh" +#include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/sccfilter.hh" + +#include "misc/escape.hh" + +void +syntax(char* prog) +{ +#ifdef REDUCCMP + std::cerr << prog << " option file" << std::endl; +#else + std::cerr << prog << " option formula" << std::endl; +#endif + exit(2); +} + +int +main(int argc, char** argv) +{ + if (argc < 3) + syntax(argv[0]); + + int o = spot::Reduce_None; + switch (atoi(argv[1])) + { + case 0: + o = spot::Reduce_Scc; + break; + case 1: + o = spot::Reduce_quotient_Dir_Sim; + break; + case 2: + o = spot::Reduce_transition_Dir_Sim; + break; + case 3: + o = spot::Reduce_quotient_Del_Sim; + break; + case 4: + o = spot::Reduce_transition_Del_Sim; + break; + case 5: + o = spot::Reduce_quotient_Dir_Sim | + spot::Reduce_transition_Dir_Sim | + spot::Reduce_Scc; + break; + case 6: + o = spot::Reduce_quotient_Del_Sim | + spot::Reduce_transition_Del_Sim | + spot::Reduce_Scc; + break; + case 7: + // No Reduction + break; + default: + return 2; + } + + int exit_code = 0; + spot::direct_simulation_relation* rel_dir = 0; + spot::delayed_simulation_relation* rel_del = 0; + spot::tgba* automata = 0; + spot::tgba_reduc* automatareduc = 0; + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::bdd_dict* dict = new spot::bdd_dict(); + +#ifdef REDUCCMP + spot::tgba_parse_error_list pel; + automata = spot::tgba_parse(argv[2], pel, dict, env, env, false); + if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel)) + return 2; +#else + spot::ltl::parse_error_list p1; + spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env); + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) + return 2; + automata = spot::ltl_to_tgba_fm(f, dict, + false, true, + false, true); +#endif + + spot::dotty_reachable(std::cout, automata); + automatareduc = new spot::tgba_reduc(automata); + + if (o & spot::Reduce_quotient_Dir_Sim) + { + rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout); + automatareduc->quotient_state(rel_dir); + } + else if (o & spot::Reduce_quotient_Del_Sim) + { + std::cout << "get delayed" << std::endl; + rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout); + std::cout << "quotient state" << std::endl; + automatareduc->quotient_state(rel_del); + std::cout << "end" << std::endl; + } + + if (rel_dir != 0) + { + automatareduc->display_rel_sim(rel_dir, std::cout); + spot::free_relation_simulation(rel_dir); + } + + if (rel_del != 0) + { + automatareduc->display_rel_sim(rel_del, std::cout); + spot::free_relation_simulation(rel_del); + } + + spot::tgba* res = automatareduc; + + if (o & spot::Reduce_Scc) + { + res = spot::scc_filter(automatareduc); + delete automatareduc; + } + + spot::dotty_reachable(std::cout, res); + + delete res; + delete automata; +#ifndef REDUCCMP + if (f != 0) + f->destroy(); +#endif + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + + if (dict != 0) + delete dict; + + return exit_code; +} diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 8b1cb8afb..a5816e14a 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis @@ -139,7 +139,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula in FM" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -fr4 -F -f -t'" + Parameters = "--spot '../ltl2tgba -fr -r4 -F -f -t'" Enabled = no } @@ -147,7 +147,7 @@ Algorithm { Name = "Spot (Couvreur -- FM) reduction7 of formula in FM" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -fr7 -F -f -t'" + Parameters = "--spot '../ltl2tgba -fr -r7 -F -f -t'" Enabled = no } diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 22259cd2a..67db4b7b6 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -334,18 +334,22 @@ if not f: finish() # Formula simplifications -opt = spot.Reduce_None +simpopt = spot.ltl_simplifier_options(False, False, False, False, False) +dored = False for r in form.getlist('r'): + dored = True if r == 'br': - opt = opt + spot.Reduce_Basics + simpopt.reduce_basics = True elif r == 'si': - opt = opt + spot.Reduce_Syntactic_Implications + simpopt.synt_impl = True elif r == 'eu': - opt = opt + spot.Reduce_Eventuality_And_Universality + simpopt.event_univ = True elif r == 'lc': - opt = opt + spot.Reduce_Containment_Checks_Stronger -if opt != spot.Reduce_None: - f2 = spot.reduce(f, opt) + simpopt.containment_checks = True + simpopt.containment_checks_stronger = True +if dored: + simp = spot.ltl_simplifier(simpopt) + f2 = simp.simplify(f) f.destroy() f = f2 diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 6f24c98a4..1167a9393 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -66,7 +66,7 @@ #include "ltlvisit/dump.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/reduce.hh" +#include "ltlvisit/simplify.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" @@ -164,7 +164,7 @@ using namespace spot; %include "ltlvisit/dump.hh" %include "ltlvisit/lunabbrev.hh" %include "ltlvisit/nenoform.hh" -%include "ltlvisit/reduce.hh" +%include "ltlvisit/simplify.hh" %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh"