From 641db2d77d4fe86fce6e07c046d348539899fbf5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Aug 2006 15:41:00 +0000 Subject: [PATCH] * src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards. * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh: Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger flags, and call reduce_tau03. * src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the default. * src/ltlvisit/contain.cc: Style. * src/ltltest/reduc.cc: Simplify using the reduce() interface instead of reduce_tau03. * src/tgbatest/ltl2tgba.cc: Likewise. Add -fr5, -fr6, and -fr7 options. * src/tgbatest/spotlbtt.test: Remove cases using "-c", since its current implementation is not always correct (and apparently reduces less than -fr7). --- ChangeLog | 17 ++++++++++++++++ src/evtgbaparse/public.hh | 9 ++++++--- src/ltltest/reduc.cc | 28 ++++++++++---------------- src/ltlvisit/contain.cc | 5 +++-- src/ltlvisit/contain.hh | 2 +- src/ltlvisit/reduce.cc | 14 ++++++++++++- src/ltlvisit/reduce.hh | 6 +++++- src/tgbaparse/public.hh | 2 +- src/tgbatest/ltl2tgba.cc | 40 ++++++++++++++++++++++++-------------- src/tgbatest/spotlbtt.test | 33 +++++++++++++------------------ 10 files changed, 94 insertions(+), 62 deletions(-) diff --git a/ChangeLog b/ChangeLog index 71e8b5b56..0785e62f1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2006-08-16 Alexandre Duret-Lutz + + * src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards. + * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh: + Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger + flags, and call reduce_tau03. + * src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the + default. + * src/ltlvisit/contain.cc: Style. + * src/ltltest/reduc.cc: Simplify using the reduce() interface + instead of reduce_tau03. + * src/tgbatest/ltl2tgba.cc: Likewise. Add -fr5, -fr6, and -fr7 + options. + * src/tgbatest/spotlbtt.test: Remove cases using "-c", since its + current implementation is not always correct (and apparently + reduces less than -fr7). + 2006-08-01 Alexandre Duret-Lutz * src/evtgbatest/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, diff --git a/src/evtgbaparse/public.hh b/src/evtgbaparse/public.hh index 2fab20175..8893b3eb3 100644 --- a/src/evtgbaparse/public.hh +++ b/src/evtgbaparse/public.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// 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. // // This file is part of Spot, a model checking library. // @@ -23,6 +23,9 @@ # define SPOT_EVTGBAPARSE_PUBLIC_HH # include "evtgba/explicit.hh" +// Unfortunately Bison 2.3 uses the same guards in all parsers :( +# undef BISON_LOCATION_HH +# undef BISON_POSITION_HH # include "location.hh" # include # include diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 63e9d774b..1688a0e4b 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -43,9 +43,6 @@ syntax(char* prog) int main(int argc, char** argv) { - bool tau03 = false; - bool stronger = false; - if (argc < 3) syntax(argv[0]); @@ -61,11 +58,10 @@ main(int argc, char** argv) case 2: o = spot::ltl::Reduce_Eventuality_And_Universality; break; - case 9: - tau03 = stronger = true; - /* fall through */ case 3: - o = spot::ltl::Reduce_All; + o = spot::ltl::Reduce_Basics + | spot::ltl::Reduce_Syntactic_Implications + | spot::ltl::Reduce_Eventuality_And_Universality; break; case 4: o = spot::ltl::Reduce_Basics | spot::ltl::Reduce_Syntactic_Implications; @@ -78,11 +74,14 @@ main(int argc, char** argv) o = (spot::ltl::Reduce_Syntactic_Implications | spot::ltl::Reduce_Eventuality_And_Universality); break; - case 8: - stronger = true; - /* fall through */ case 7: - tau03 = true; + o = spot::ltl::Reduce_Containment_Checks; + break; + case 8: + o = spot::ltl::Reduce_Containment_Checks_Stronger; + break; + case 9: + o = spot::ltl::Reduce_All; break; default: return 2; @@ -127,13 +126,6 @@ main(int argc, char** argv) spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); - if (tau03) - { - ftmp1 = f1; - f1 = spot::ltl::reduce_tau03(f1, stronger); - spot::ltl::destroy(ftmp1); - } - int length_f1_after = spot::ltl::length(f1); std::string f1s_after = spot::ltl::to_string(f1); diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 51d5a7bfa..7b2694ee8 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -124,7 +124,7 @@ namespace spot bool language_containment_checker::equal(const formula* l, const formula* g) { - return contained(l,g) && contained(g,l); + return contained(l, g) && contained(g, l); } language_containment_checker::record_* @@ -143,7 +143,8 @@ namespace spot } - namespace { + namespace + { struct reduce_tau03_visitor : public clone_visitor { bool stronger; language_containment_checker* lcc; diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index f268b7320..ddfe02970 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -101,7 +101,7 @@ namespace spot /// If \a stronger is set, additional rules are used to further /// reduce some U, R, and X usages. /// \endverbatim - formula* reduce_tau03(const formula* f, bool stronger = false); + formula* reduce_tau03(const formula* f, bool stronger = true); } } diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index de9372a25..000827742 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -29,6 +29,7 @@ #include "simpfg.hh" #include "nenoform.hh" #include "ltlvisit/destroy.hh" +#include "contain.hh" namespace spot { @@ -331,6 +332,17 @@ namespace spot f2 = f1; } } + + + if (opt & (Reduce_Containment_Checks + | Reduce_Containment_Checks_Stronger)) + { + formula* f1 = reduce_tau03(f2, + opt & Reduce_Containment_Checks_Stronger); + destroy(f2); + f2 = f1; + } + return f2; } } diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index f4e7eccc0..3c6fcf850 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -44,6 +44,10 @@ namespace spot Reduce_Syntactic_Implications = 2, /// Etessami & Holzmann eventuality and universality reductions. Reduce_Eventuality_And_Universality = 4, + /// Tauriainen containment checks. + Reduce_Containment_Checks = 8, + /// Tauriainen containment checks (stronger version). + Reduce_Containment_Checks_Stronger = 16, /// All reductions. Reduce_All = -1U }; diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 2ccb56e5e..652ae6a28 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -23,7 +23,7 @@ # define SPOT_TGBAPARSE_PUBLIC_HH # include "tgba/tgbaexplicit.hh" - /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ +// Unfortunately Bison 2.3 uses the same guards in all parsers :( # undef BISON_LOCATION_HH # undef BISON_POSITION_HH # include "tgbaparse/location.hh" diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 87dc6997b..a0acb991b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -25,7 +25,6 @@ #include #include #include "ltlvisit/destroy.hh" -#include "ltlvisit/reduce.hh" #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/apcollect.hh" @@ -81,6 +80,9 @@ syntax(char* prog) << " -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 << " -F read the formula from the file" << std::endl << " -g graph the accepting run on the automaton (requires -e)" << std::endl @@ -167,8 +169,6 @@ main(int argc, char** argv) bool from_file = false; int reduc_aut = spot::Reduce_None; int redopt = spot::ltl::Reduce_None; - bool redtau = false; - bool stronger = false; bool display_reduce_form = false; bool display_rel_sim = false; bool display_parity_game = false; @@ -281,6 +281,23 @@ main(int argc, char** argv) fm_red |= spot::ltl::Reduce_Syntactic_Implications; } else if (!strcmp(argv[formula_index], "-fr4")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Basics + | spot::ltl::Reduce_Eventuality_And_Universality + | spot::ltl::Reduce_Syntactic_Implications; + } + else if (!strcmp(argv[formula_index], "-fr5")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Containment_Checks; + } + else if (!strcmp(argv[formula_index], "-fr6")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger; + } + else if (!strcmp(argv[formula_index], "-fr7")) { fm_opt = true; fm_red |= spot::ltl::Reduce_All; @@ -347,20 +364,21 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-r4")) { - redopt |= spot::ltl::Reduce_All; + redopt |= spot::ltl::Reduce_Basics + | spot::ltl::Reduce_Eventuality_And_Universality + | spot::ltl::Reduce_Syntactic_Implications; } else if (!strcmp(argv[formula_index], "-r5")) { - redtau = true; + redopt |= spot::ltl::Reduce_Containment_Checks; } else if (!strcmp(argv[formula_index], "-r6")) { - redtau = stronger = true; + redopt |= spot::ltl::Reduce_Containment_Checks_Stronger; } else if (!strcmp(argv[formula_index], "-r7")) { redopt |= spot::ltl::Reduce_All; - redtau = stronger = true; } else if (!strcmp(argv[formula_index], "-R")) { @@ -517,14 +535,6 @@ main(int argc, char** argv) spot::ltl::formula* t = spot::ltl::reduce(f, redopt); spot::ltl::destroy(f); f = t; - if (display_reduce_form && !redtau) - std::cout << spot::ltl::to_string(f) << std::endl; - } - if (redtau) - { - spot::ltl::formula* t = spot::ltl::reduce_tau03(f, stronger); - spot::ltl::destroy(f); - f = t; if (display_reduce_form) std::cout << spot::ltl::to_string(f) << std::endl; } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 8911ad7cd..06bac3982 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -1,7 +1,7 @@ #!/bin/sh -# 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. +# 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. # # This file is part of Spot, a model checking library. # @@ -68,14 +68,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM) containments" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -c -t'" - Enabled = yes -} - Algorithm { Name = "Spot (Couvreur -- FM), basic reduction of formula" @@ -116,15 +108,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM) containments + reduction of formula (pre reduction)" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -r7 -F -f -c -t'" - Enabled = yes -} - - Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula in FM" @@ -133,6 +116,16 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM) reduction7 of formula in FM" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot './ltl2tgba -fr7 -F -f -t'" + Enabled = yes +} + + + Algorithm { Name = "Spot (Couvreur -- FM), post reduction with direct simulation"