From 9db2b31484ac619d4988f130155c7a1189c25409 Mon Sep 17 00:00:00 2001 From: martinez Date: Fri, 14 May 2004 12:55:13 +0000 Subject: [PATCH] * src/ltlvisit/basereduc.cc (spot): Correct some mistakes. * src/ltlvisit/lunabbrev.cc (spot): Nothing change. * src/tgbatest/ltl2tgba.cc (main): More option to reduce formula. * src/tgbatest/spotlbtt.test: One more test. --- ChangeLog | 8 ++++ src/ltlvisit/basereduc.cc | 30 +++++++-------- src/ltlvisit/lunabbrev.cc | 78 ++------------------------------------ src/tgbatest/ltl2tgba.cc | 52 ++++++++++++++++++++++--- src/tgbatest/spotlbtt.test | 7 ++++ 5 files changed, 80 insertions(+), 95 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0ab844fb9..d0356aea5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2004-05-14 Thomas Martinez + + * src/ltlvisit/basereduc.cc (spot): Correct some mistakes. + * src/ltlvisit/lunabbrev.cc (spot): Nothing change. + * src/tgbatest/ltl2tgba.cc (main): More option to reduce + formula. + * src/tgbatest/spotlbtt.test: One more test. + 2004-05-14 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc (to_spin_string_visitor, diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc index 62e143b69..2b3eb54ce 100644 --- a/src/ltlvisit/basereduc.cc +++ b/src/ltlvisit/basereduc.cc @@ -89,8 +89,8 @@ namespace spot /* X(f1 | GF(f2)) = X(f1) | GF(F2) */ if (node_type(result_) == (node_type_form_visitor::Multop)) { if (dynamic_cast(result_)->size() == 2) { - if (is_GF(dynamic_cast(result_)->nth(0)) || - is_FG(dynamic_cast(result_)->nth(0))) { + if (is_GF(dynamic_cast(result_)->nth(0))) { + //|| is_FG(dynamic_cast(result_)->nth(0))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast(result_)->nth(1)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(0))); @@ -99,8 +99,8 @@ namespace spot spot::ltl::destroy(f); return; } - if (is_GF(dynamic_cast(result_)->nth(1)) || - is_FG(dynamic_cast(result_)->nth(1))) { + if (is_GF(dynamic_cast(result_)->nth(1))) { + //|| is_FG(dynamic_cast(result_)->nth(1))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast(result_)->nth(0)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(1))); @@ -137,8 +137,8 @@ namespace spot if (node_type(result_) == (node_type_form_visitor::Multop)) { if (dynamic_cast(result_)->op() == multop::And) { if (dynamic_cast(result_)->size() == 2) { - if (is_GF(dynamic_cast(result_)->nth(0)) || - is_FG(dynamic_cast(result_)->nth(0))) { + if (is_GF(dynamic_cast(result_)->nth(0))) { + //|| is_FG(dynamic_cast(result_)->nth(0))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast(result_)->nth(1)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(0))); @@ -146,8 +146,8 @@ namespace spot result_ = multop::instance(multop::And, res); return; } - if (is_GF(dynamic_cast(result_)->nth(1)) || - is_FG(dynamic_cast(result_)->nth(1))) { + if (is_GF(dynamic_cast(result_)->nth(1))) { + //|| is_FG(dynamic_cast(result_)->nth(1))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast(result_)->nth(0)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(1))); @@ -193,8 +193,8 @@ namespace spot if (node_type(result_) == (node_type_form_visitor::Multop)) { if (dynamic_cast(f)->op() == multop::Or) { if (dynamic_cast(result_)->size() == 2) { - if (is_GF(dynamic_cast(result_)->nth(0)) || - is_FG(dynamic_cast(result_)->nth(0))) { + if (is_GF(dynamic_cast(result_)->nth(0))) { + //|| is_FG(dynamic_cast(result_)->nth(0))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast(result_)->nth(1)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(0))); @@ -202,8 +202,8 @@ namespace spot result_ = multop::instance(multop::Or, res); return; } - if (is_GF(dynamic_cast(result_)->nth(1)) || - is_FG(dynamic_cast(result_)->nth(1))) { + if (is_GF(dynamic_cast(result_)->nth(1))) { + //|| is_FG(dynamic_cast(result_)->nth(1))) { multop::vec* res = new multop::vec; res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast(result_)->nth(0)))); res->push_back(basic_reduce_form(dynamic_cast(result_)->nth(1))); @@ -450,7 +450,7 @@ namespace spot break; } - /* GF(a) & GF(b) = GF(a & b)*/ + /* GF(a) | GF(b) = GF(a | b)*/ if (is_GF(*i)) { tmpGF->push_back(spot::ltl::basic_reduce_form(dynamic_cast(dynamic_cast(*i)->child())->child())); break; @@ -553,8 +553,8 @@ namespace spot multop::instance(mo->op(),tmpGF)))); if (tmpFG != NULL) if (tmpFG->size()) - tmpOther->push_back(unop::instance(unop::G, - unop::instance(unop::F, + tmpOther->push_back(unop::instance(unop::F, + unop::instance(unop::G, multop::instance(mo->op(),tmpFG)))); result_ = multop::instance(op, tmpOther); diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 0a8afba15..e075bb020 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -22,58 +22,14 @@ #include "ltlast/allnodes.hh" #include "ltlvisit/clone.hh" #include "lunabbrev.hh" -//#include "reducform.hh" +#include "reducform.hh" #include namespace spot { namespace ltl { - - class node_type_form_visitor : public const_visitor - { - public: - enum type { Atom, Const, Unop, Binop, Multop }; - - node_type_form_visitor(){} - - type - result() const { return result_;} - - void - visit(const atomic_prop* ap){ - if (ap == NULL); - result_ = node_type_form_visitor::Atom; - } - - void - visit(const constant* c){ - if (c == NULL); - result_ = node_type_form_visitor::Const; - } - - void - visit(const unop* uo){ - if (uo == NULL); - result_ = node_type_form_visitor::Unop; - } - - void - visit(const binop* bo){ - if (bo == NULL); - result_ = node_type_form_visitor::Binop; - } - - void - visit(const multop* mo){ - if (mo == NULL); - result_ = node_type_form_visitor::Multop; - } - - protected: - type result_; - }; - + unabbreviate_logic_visitor::unabbreviate_logic_visitor() { } @@ -82,37 +38,11 @@ namespace spot { } - /* - void - unabbreviate_logic_visitor::visit(unop* uo) - { - formula* f = uo->child(); - switch (uo->op()) - { - case unop::Not: - case unop::X: - result_ = unop::instance(uo->op(),recurse(f)); - return; - case unop::F: - result_ = binop::instance(binop::U,constant::true_instance(),recurse(f)); - return; - case unop::G: - result_ = binop::instance(binop::R,constant::false_instance(),recurse(f)); - return; - } - // Unreachable code. - assert(0); - } - */ - void unabbreviate_logic_visitor::visit(binop* bo) { formula* f1 = recurse(bo->first()); formula* f2 = recurse(bo->second()); - - node_type_form_visitor v; - const_cast(f1)->accept(v); switch (bo->op()) { @@ -145,7 +75,7 @@ namespace spot /* true U f2 == F(f2) */ case binop::U: - if ( v.result() == node_type_form_visitor::Const ) + if ( node_type(f1) == node_type_form_visitor::Const ) if ( ((constant*)f1)->val() == constant::True ) { result_ = unop::instance(unop::F,f2); return; @@ -155,7 +85,7 @@ namespace spot /* false R f2 == G(f2) */ case binop::R: - if ( v.result() == node_type_form_visitor::Const ) + if ( node_type(f1) == node_type_form_visitor::Const ) if ( ((constant*)f1)->val() == constant::False ) { result_ = unop::instance(unop::G,f2); return; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1c7b3b1dc..0a27e44a2 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -93,7 +93,15 @@ syntax(char* prog) << std::endl << " -y do not merge states with same symbolic representation " << "(implies -f)" << std::endl - << " -z to reduce formula " + << " -r1 to reduce formula using basic rewriting" + << std::endl + << " -r2 to reduce formula using class of eventuality and " + << "and universality" + << std::endl + << " -r3 to reduce formula using implication between " + << "two formula" + << std::endl + << " -r4 to reduce formula using all rules" << std::endl; exit(2); } @@ -116,7 +124,10 @@ main(int argc, char** argv) bool magic_many = false; bool expect_counter_example = false; bool from_file = false; - bool reduc = false; + bool reduc_r1 = false; + bool reduc_r2 = false; + bool reduc_r3 = false; + bool reduc_r4 = false; bool post_branching = false; bool fair_loop_approx = false; @@ -254,9 +265,25 @@ main(int argc, char** argv) fm_opt = true; fm_symb_merge_opt = false; } - else if (!strcmp(argv[formula_index], "-z")) + else if (!strcmp(argv[formula_index], "-r1")) { - reduc = true; + 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 if (!strcmp(argv[formula_index], "-rd")) + { + reduc_rd = true; } else { @@ -322,8 +349,20 @@ main(int argc, char** argv) { spot::ltl::formula* ftmp = f; - if (reduc) + if (reduc_r4) f = spot::ltl::reduce(f); + else { + if (reduc_r1 | reduc_r2 | reduc_r3) { + spot::ltl::option o = spot::ltl::BRI; + if (reduc_r1) + o = spot::ltl::Base; + if (reduc_r2) + o = spot::ltl::EventualUniversal; + if (reduc_r3) + o = spot::ltl::Inf; + f = spot::ltl::reduce(f, o); + } + } if (fm_opt) to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, @@ -333,8 +372,9 @@ main(int argc, char** argv) else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); - if (reduc) + if (reduc_r1 || reduc_r2 || reduc_r3 || reduc_r4) { spot::ltl::destroy(ftmp); + } } spot::tgba_tba_proxy* degeneralized = 0; diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index d409a4692..cdd00503f 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -28,6 +28,13 @@ echo 'This test can take as long as 15 minutes on a 2GHz Pentium 4.' set -e cat > config <