From 4cd10c3dfcc62c096328a86ec6b60bff3e5d0d42 Mon Sep 17 00:00:00 2001 From: martinez Date: Thu, 13 May 2004 16:00:15 +0000 Subject: [PATCH] * src/ltlvisit/Makefile.am: Copyright 2004. * src/ltltest/inf.test: More test. * src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot): Use dynamic_cast. * src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh, src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option to choose which rules applies to simplify the formula. --- ChangeLog | 10 ++ src/ltltest/inf.test | 24 +++ src/ltltest/reduc.cc | 42 +++-- src/ltltest/reduc.test | 39 ++-- src/ltlvisit/Makefile.am | 2 +- src/ltlvisit/basereduc.cc | 270 ++++++++++++++-------------- src/ltlvisit/forminf.cc | 143 ++++++++------- src/ltlvisit/reducform.cc | 370 ++++++++++++++++++-------------------- src/ltlvisit/reducform.hh | 49 ++--- 9 files changed, 489 insertions(+), 460 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8036d8b26..abc4a6f9a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2004-05-13 Thomas Martinez + + * src/ltlvisit/Makefile.am: Copyright 2004. + * src/ltltest/inf.test: More test. + * src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot): + Use dynamic_cast. + * src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh, + src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option + to choose which rules applies to simplify the formula. + 2004-05-13 Alexandre Duret-Lutz * src/ltltest/reduc.test: Typo. diff --git a/src/ltltest/inf.test b/src/ltltest/inf.test index a889bf4ed..d01dd6449 100755 --- a/src/ltltest/inf.test +++ b/src/ltltest/inf.test @@ -26,6 +26,27 @@ . ./defs || exit 1 # +run 1 ./inf 'Xa' 'X(b U a)' +run 1 ./inf 'XXa' 'XX(b U a)' + +run 1 ./inf '(e R f)' '(g U f)' +run 1 ./inf '( X(a + b))' '( X((a + b)+(c)+(d)))' +run 1 ./inf '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)' + +run 0 ./inf 'Xa' 'XX(b U a)' +run 0 ./inf 'XXa' 'X(b U a)' + +run 0 ./inf '( X(a + b))' '( X(X(a + b)+(c)+(d)))' +run 0 ./inf '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)' + +run 0 ./inf 'a' 'b' +run 0 ./inf 'a' 'b + c' +run 0 ./inf 'a + b' 'a' +run 0 ./inf 'a' 'a * c' +run 0 ./inf 'a * b' 'c' +run 0 ./inf 'a' 'a U b' +run 0 ./inf 'a' 'a R b' +run 0 ./inf 'a R b' 'a' run 1 ./inf '1' '1' run 1 ./inf '0' '0' @@ -52,6 +73,9 @@ run 1 ./inf 'a' 'a R 1' run 1 ./inf 'a R b' 'b' run 1 ./inf 'a R b' '1' +run 1 ./inf 'Xa' 'X(b U a)' +run 1 ./inf 'X(a R b)' 'Xb' + run 1 ./inf 'a U b' '1 U b' run 1 ./inf 'a R b' '1 R b' diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 656afc2a9..665c31763 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -34,30 +34,45 @@ void syntax(char* prog) { - std::cerr << prog << " formula1 (formula2)?" << std::endl; + std::cerr << prog << " option formula1 (formula2)?" << std::endl; exit(2); } -typedef spot::ltl::formula* ptrfunct(const spot::ltl::formula*); - int main(int argc, char** argv) { - if (argc < 2) + if (argc < 3) syntax(argv[0]); + spot::ltl::option o; + switch(atoi(argv[1])){ + case 0: + o = spot::ltl::Base; + break; + case 1: + o = spot::ltl::Inf; + break; + case 2: + o = spot::ltl::EventualUniversal; + break; + case 3: + o = spot::ltl::BRI; + break; + default: return 2; + } + spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1); spot::ltl::formula* f2 = NULL; - if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) return 2; - if (argc == 3){ + if (argc == 4){ spot::ltl::parse_error_list p2; - f2 = spot::ltl::parse(argv[2], p2); - if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) + f2 = spot::ltl::parse(argv[3], p2); + if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2)) return 2; } @@ -78,7 +93,7 @@ main(int argc, char** argv) std::string f1s_before = spot::ltl::to_string(f1); ftmp1 = f1; - f1 = spot::ltl::reduce(f1); + f1 = spot::ltl::reduce(f1,o); ftmp2 = f1; f1 = spot::ltl::unabbreviate_logic(f1); spot::ltl::destroy(ftmp1); @@ -134,13 +149,6 @@ main(int argc, char** argv) if (length_f1_after < length_f1_before) exit_code = 0; } - /* - spot::ltl::dump(std::cout, f1); std::cout << std::endl; - if (f2 != NULL) - spot::ltl::dump(std::cout, f2); std::cout << std::endl; - */ - - spot::ltl::destroy(f1); if (f2 != NULL) spot::ltl::destroy(f2); diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test index 4f2eda9f9..d01898701 100755 --- a/src/ltltest/reduc.test +++ b/src/ltltest/reduc.test @@ -23,30 +23,37 @@ # Check for the reduc visitor. -. ./defs || exit 1 +#. ./defs || exit 1 set -e -FICH=${1-$srcdir/formules.ltl} +#FICH=${1-$srcdir/formules.ltl} +FICH=${1-formules.ltl} ##################################### -rm -f result.data - -cat $FICH | -while read f; do - if [ -n "$f" ] && [ "$f" != "####" ]; then - ./reduc "$f" >> result.data - fi -done - -test $? == 0 || exit 1 - +for opt in 0 1 2 3 + do + rm -f result.data + + cat $FICH | + while read f; do + if [ -n "$f" ] && [ "$f" != "####" ]; then + ./reduc $opt "$f" >> result.data + fi + done + + test $? == 0 || exit 1 + ##################################### - -perl -ne 'BEGIN { $sum1 = 0; $sum2 = 0; } + + perl -ne 'BEGIN { $sum1 = 0; $sum2 = 0; } /^(\d+)\s+(\d+)/; $sum1 += $1; $sum2 += $2; -END { print $sum2 * 100 / $sum1; print "\n"; } +END { print 100 - ($sum2 * 100 / $sum1); print "\n"; } ' < result.data + +done + +##################################### diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index c6f61a505..c994ed011 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc index e7660fd9f..62e143b69 100644 --- a/src/ltlvisit/basereduc.cc +++ b/src/ltlvisit/basereduc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -33,9 +33,9 @@ namespace spot class basic_reduce_form_visitor : public visitor { public: - + basic_reduce_form_visitor(){} - + virtual ~basic_reduce_form_visitor(){} formula* @@ -43,14 +43,14 @@ namespace spot { return result_; } - + void visit(atomic_prop* ap) { formula* f = ap->ref(); result_ = f; } - + void visit(constant* c) { @@ -64,7 +64,7 @@ namespace spot return; } } - + void visit(unop* uo) { @@ -77,35 +77,35 @@ namespace spot return; case unop::X: - /* X(true) = true + /* X(true) = true X(false) = false */ if (node_type(result_) == (node_type_form_visitor::Const)) return; - + /* XGF(f) = GF(f) */ if (is_GF(result_)) return; /* X(f1 & GF(f2)) = X(f1) & GF(F2) */ /* X(f1 | GF(f2)) = X(f1) | GF(F2) */ if (node_type(result_) == (node_type_form_visitor::Multop)) { - if (spot::ltl::nb_term_multop(result_) == 2) { - if (is_GF(((multop*)result_)->nth(0)) || - is_FG(((multop*)result_)->nth(0))) { + if (dynamic_cast(result_)->size() == 2) { + 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(((multop*)result_)->nth(1)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); + 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))); f = result_; - result_ = multop::instance(((multop*)(result_))->op(), res); + result_ = multop::instance(dynamic_cast(result_)->op(), res); spot::ltl::destroy(f); return; } - if (is_GF(((multop*)result_)->nth(1)) || - is_FG(((multop*)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(((multop*)result_)->nth(0)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); + 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))); f = result_; - result_ = multop::instance(((multop*)(result_))->op(), res); + result_ = multop::instance(dynamic_cast(result_)->op(), res); spot::ltl::destroy(f); return; } @@ -114,43 +114,43 @@ namespace spot result_ = unop::instance(unop::X, result_); return; - - case unop::F: - - /* F(true) = true + + case unop::F: + + /* F(true) = true F(false) = false */ if (node_type(result_) == (node_type_form_visitor::Const)) return; - + /* FX(a) = XF(a) */ if (node_type(result_) == (node_type_form_visitor::Unop)) - if ( ((unop*)(result_))->op() == unop::X ){ + if (dynamic_cast(result_)->op() == unop::X){ f = result_; result_ = unop::instance(unop::X, unop::instance(unop::F, - basic_reduce_form(((unop*)(result_))->child()) )); + basic_reduce_form(dynamic_cast(result_)->child()) )); spot::ltl::destroy(f); return; } - + /* F(f1 & GF(f2)) = F(f1) & GF(F2) */ if (node_type(result_) == (node_type_form_visitor::Multop)) { - if ( ((multop*)(result_))->op() == multop::And ) { - if (spot::ltl::nb_term_multop(result_) == 2) { - if (is_GF(((multop*)result_)->nth(0)) || - is_FG(((multop*)result_)->nth(0))) { + 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))) { multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); + 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))); spot::ltl::destroy(result_); result_ = multop::instance(multop::And, res); return; } - if (is_GF(((multop*)result_)->nth(1)) || - is_FG(((multop*)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(((multop*)result_)->nth(0)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); + 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))); spot::ltl::destroy(result_); result_ = multop::instance(multop::And, res); return; @@ -163,50 +163,50 @@ namespace spot return; case unop::G: - - /* G(true) = true + + /* G(true) = true G(false) = false */ if (node_type(result_) == (node_type_form_visitor::Const)) return; /* G(a R b) = G(b) */ if (node_type(result_) == node_type_form_visitor::Binop) - if ( ((binop*)(result_))->op() == binop::R ){ + if (dynamic_cast(result_)->op() == binop::R){ f = result_; - result_ = unop::instance(unop::G, basic_reduce_form(((binop*)(result_))->second())); + result_ = unop::instance(unop::G, basic_reduce_form(dynamic_cast(result_)->second())); spot::ltl::destroy(f); return; } - + /* GX(a) = XG(a) */ if (node_type(result_) == (node_type_form_visitor::Unop)) - if ( ((unop*)(result_))->op() == unop::X ){ + if ( dynamic_cast(result_)->op() == unop::X ){ f = result_; result_ = unop::instance(unop::X, unop::instance(unop::G, - basic_reduce_form(((unop*)(result_))->child()) )); + basic_reduce_form(dynamic_cast(result_)->child()))); spot::ltl::destroy(f); return; } /* G(f1 | GF(f2)) = G(f1) | GF(F2) */ if (node_type(result_) == (node_type_form_visitor::Multop)) { - if ( ((multop*)(f))->op() == multop::Or ) { - if (spot::ltl::nb_term_multop(result_) == 2) { - if (is_GF(((multop*)result_)->nth(0)) || - is_FG(((multop*)result_)->nth(0))) { + 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))) { multop::vec* res = new multop::vec; - res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(1)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); + 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))); spot::ltl::destroy(result_); result_ = multop::instance(multop::Or, res); return; } - if (is_GF(((multop*)result_)->nth(1)) || - is_FG(((multop*)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(((multop*)result_)->nth(0)))); - res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); + 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))); spot::ltl::destroy(result_); result_ = multop::instance(multop::Or, res); return; @@ -221,7 +221,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(binop* bo) { @@ -233,24 +233,24 @@ namespace spot switch (bo->op()) { case binop::Xor: - result_ = binop::instance(binop::Xor, - basic_reduce_form(f1), + result_ = binop::instance(binop::Xor, + basic_reduce_form(f1), basic_reduce_form(f2)); return; case binop::Equiv: - result_ = binop::instance(binop::Equiv, - basic_reduce_form(f1), + result_ = binop::instance(binop::Equiv, + basic_reduce_form(f1), basic_reduce_form(f2)); return; case binop::Implies: - result_ = binop::instance(binop::Implies, - basic_reduce_form(f1), + result_ = binop::instance(binop::Implies, + basic_reduce_form(f1), basic_reduce_form(f2)); return; case binop::U: f2 = basic_reduce_form(f2); - - /* a U false = false + + /* a U false = false a U true = true */ if (node_type(f2) == (node_type_form_visitor::Const)) { result_ = f2; @@ -262,11 +262,11 @@ namespace spot /* X(a) U X(b) = X(a U b) */ if ( node_type(f1) == (node_type_form_visitor::Unop) && node_type(f2) == (node_type_form_visitor::Unop)) { - if ( (((unop*)(f1))->op() == unop::X) - && (((unop*)(f2))->op() == unop::X) ) { + if ((dynamic_cast(f1)->op() == unop::X) + && (dynamic_cast(f2)->op() == unop::X)) { ftmp = binop::instance(binop::U, - basic_reduce_form(((unop*)(f1))->child()), - basic_reduce_form(((unop*)(f2))->child())); + basic_reduce_form(dynamic_cast(f1)->child()), + basic_reduce_form(dynamic_cast(f2)->child())); result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); spot::ltl::destroy(f1); spot::ltl::destroy(f2); @@ -277,10 +277,10 @@ namespace spot result_ = binop::instance(binop::U, f1, f2); return; - case binop::R: + case binop::R: f2 = basic_reduce_form(f2); - /* a R false = false + /* a R false = false a R true = true */ if (node_type(f2) == (node_type_form_visitor::Const)) { result_ = f2; @@ -288,15 +288,15 @@ namespace spot } f1 = basic_reduce_form(f1); - + /* X(a) R X(b) = X(a R b) */ - if ( node_type(f1) == (node_type_form_visitor::Unop) - && node_type(f2) == (node_type_form_visitor::Unop)) { - if ( (((unop*)(f1))->op() == unop::X) - && (((unop*)(f2))->op() == unop::X) ) { + if (node_type(f1) == (node_type_form_visitor::Unop) + && node_type(f2) == (node_type_form_visitor::Unop)) { + if ((dynamic_cast(f1)->op() == unop::X) + && (dynamic_cast(f2)->op() == unop::X)) { ftmp = binop::instance(bo->op(), - basic_reduce_form(((unop*)(f1))->child()), - basic_reduce_form(((unop*)(f2))->child())); + basic_reduce_form(dynamic_cast(f1)->child()), + basic_reduce_form(dynamic_cast(f2)->child())); result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); spot::ltl::destroy(f1); spot::ltl::destroy(f2); @@ -311,7 +311,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(multop* mo) { @@ -330,12 +330,12 @@ namespace spot multop::vec* tmpOther = new multop::vec; - formula* ftmp = NULL; - + formula* ftmp = NULL; + for (unsigned i = 0; i < mos; ++i) res->push_back(basic_reduce_form(mo->nth(i))); - + switch (op) { case multop::And: @@ -344,17 +344,17 @@ namespace spot if (*i == NULL) continue; switch (node_type(*i)) { - case node_type_form_visitor::Unop: + case node_type_form_visitor::Unop: /* Xa & Xb = X(a & b)*/ - if (((unop*)(*i))->op() == unop::X) { - tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) ); + if (dynamic_cast(*i)->op() == unop::X) { + tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*i)->child())); break; - } + } /* FG(a) & FG(b) = FG(a & b)*/ if (is_FG(*i)) { - tmpFG->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) ); + tmpFG->push_back(spot::ltl::basic_reduce_form(dynamic_cast(dynamic_cast(*i)->child())->child())); break; } tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); @@ -368,19 +368,19 @@ namespace spot case node_type_form_visitor::Binop: /* (a U b) & (c U b) = (a & c) U b */ - if (((binop*)(*i))->op() == binop::U) { - ftmp = ((binop*)(*i))->second(); + if (dynamic_cast(*i)->op() == binop::U) { + ftmp = dynamic_cast(*i)->second(); tmpUright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) + for (multop::vec::iterator j = i; j != res->end(); j++) { if (*j == NULL) continue; - if (node_type(*j) == node_type_form_visitor::Binop) + if (node_type(*j) == node_type_form_visitor::Binop) { - if (((binop*)(*j))->op() == binop::U) + if (dynamic_cast(*j)->op() == binop::U) { - if (ftmp == ((binop*)(*j))->second()) + if (ftmp == dynamic_cast(*j)->second()) { - tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() )); + tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*j)->first() )); if (j != i) { spot::ltl::destroy(*j); *j = NULL; @@ -394,21 +394,21 @@ namespace spot basic_reduce_form(ftmp))); break; } - + /* (a R b) & (a R c) = a R (b & c) */ - if (((binop*)(*i))->op() == binop::R) { - ftmp = ((binop*)(*i))->first(); + if (dynamic_cast(*i)->op() == binop::R) { + ftmp = dynamic_cast(*i)->first(); tmpRright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) + for (multop::vec::iterator j = i; j != res->end(); j++) { if (*j == NULL) continue; - if (node_type(*j) == node_type_form_visitor::Binop) + if (node_type(*j) == node_type_form_visitor::Binop) { - if (((binop*)(*j))->op() == binop::R) + if (dynamic_cast(*j)->op() == binop::R) { - if (ftmp == ((binop*)(*j))->first()) + if (ftmp == dynamic_cast(*j)->first()) { - tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() )); + tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*j)->second() )); if (j != i) { spot::ltl::destroy(*j); *j = NULL; @@ -424,56 +424,56 @@ namespace spot } tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); break; - default: + default: tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); break; } spot::ltl::destroy(*i); } - + delete(tmpGF); tmpGF = NULL; break; - + case multop::Or: - + for (multop::vec::iterator i = res->begin(); i != res->end(); i++) { if (*i == NULL) continue; switch (node_type(*i)) { - - case node_type_form_visitor::Unop: + + case node_type_form_visitor::Unop: /* Xa | Xb = X(a | b)*/ - if (((unop*)(*i))->op() == unop::X) { - tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) ); + if (dynamic_cast(*i)->op() == unop::X) { + tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*i)->child())); break; } /* GF(a) & GF(b) = GF(a & b)*/ if (is_GF(*i)) { - tmpGF->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) ); + tmpGF->push_back(spot::ltl::basic_reduce_form(dynamic_cast(dynamic_cast(*i)->child())->child())); break; } tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); break; case node_type_form_visitor::Binop: - + /* (a U b) | (a U c) = a U (b | c) */ - if (((binop*)(*i))->op() == binop::U) { - ftmp = ((binop*)(*i))->first(); + if (dynamic_cast(*i)->op() == binop::U) { + ftmp = dynamic_cast(*i)->first(); tmpUright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) + for (multop::vec::iterator j = i; j != res->end(); j++) { if (*j == NULL) continue; - if (node_type(*j) == node_type_form_visitor::Binop) + if (node_type(*j) == node_type_form_visitor::Binop) { - if (((binop*)(*j))->op() == binop::U) + if (dynamic_cast(*j)->op() == binop::U) { - if (ftmp == ((binop*)(*j))->first()) + if (ftmp == dynamic_cast(*j)->first()) { - tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() )); + tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*j)->second())); if (j != i) { spot::ltl::destroy(*j); *j = NULL; @@ -487,21 +487,21 @@ namespace spot multop::instance(multop::Or,tmpUright))); break; } - + /* (a R b) | (c R b) = (a | c) R b */ - if (((binop*)(*i))->op() == binop::R) { - ftmp = ((binop*)(*i))->second(); + if (dynamic_cast(*i)->op() == binop::R) { + ftmp = dynamic_cast(*i)->second(); tmpRright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) + for (multop::vec::iterator j = i; j != res->end(); j++) { if (*j == NULL) continue; - if (node_type(*j) == node_type_form_visitor::Binop) + if (node_type(*j) == node_type_form_visitor::Binop) { - if (((binop*)(*j))->op() == binop::R) + if (dynamic_cast(*j)->op() == binop::R) { - if (ftmp == ((binop*)(*j))->second()) + if (ftmp == dynamic_cast(*j)->second()) { - tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() )); + tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast(*j)->first())); if (j != i) { spot::ltl::destroy(*j); *j = NULL; @@ -517,35 +517,35 @@ namespace spot } tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); break; - default: + default: tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); break; } spot::ltl::destroy(*i); } - + delete(tmpFG); tmpFG = NULL; break; } - - + + res->clear(); delete(res); - + if (tmpX->size()) tmpOther->push_back(unop::instance(unop::X,multop::instance(mo->op(),tmpX))); else delete(tmpX); - + if (tmpU->size()) tmpOther->push_back(multop::instance(mo->op(),tmpU)); else delete(tmpU); - + if (tmpR->size()) tmpOther->push_back(multop::instance(mo->op(),tmpR)); else delete(tmpR); - + if (tmpGF != NULL) if (tmpGF->size()) tmpOther->push_back(unop::instance(unop::G, @@ -556,13 +556,13 @@ namespace spot tmpOther->push_back(unop::instance(unop::G, unop::instance(unop::F, multop::instance(mo->op(),tmpFG)))); - + result_ = multop::instance(op, tmpOther); return; } - + protected: formula* result_; }; diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/forminf.cc index 88e1c6735..92d6f57df 100644 --- a/src/ltlvisit/forminf.cc +++ b/src/ltlvisit/forminf.cc @@ -35,10 +35,10 @@ namespace spot bool is_GF(const formula* f) { - if ((const unop*)f != NULL) - if (((const unop*)f)->op() == unop::G) - if ((const unop*)(((const unop*)f)->child()) != NULL) - if (((const unop*)((const unop*)f)->child())->op() == unop::F) + if (node_type(f) == node_type_form_visitor::Unop) + if (dynamic_cast(f)->op() == unop::G) + if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop) + if (dynamic_cast(dynamic_cast(f)->child())->op() == unop::F) return true; return false; } @@ -46,24 +46,14 @@ namespace spot bool is_FG(const formula* f) { - if ((const unop*)f != NULL) - if (((const unop*)f)->op() == unop::F) - if ((const unop*)(((const unop*)f)->child()) != NULL) - if (((const unop*)((const unop*)f)->child())->op() == unop::G) + if (node_type(f) == node_type_form_visitor::Unop) + if (dynamic_cast(f)->op() == unop::F) + if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop) + if (dynamic_cast(dynamic_cast(f)->child())->op() == unop::G) return true; return false; } - int - nb_term_multop(const formula* f) - { - if ((const multop*)f == NULL) return -1; - - unsigned mos = ((const multop*)(f))->size(); - return mos; - } - - node_type_form_visitor::node_type_form_visitor(){} node_type_form_visitor::type @@ -102,7 +92,7 @@ namespace spot node_type_form_visitor::type node_type(const formula* f) { node_type_form_visitor v; - if (f == NULL) std::cout << "f == NULL !!!!!!!!" << std::endl; + assert(f != NULL); const_cast(f)->accept(v); return v.result(); } @@ -113,7 +103,7 @@ namespace spot form_eventual_universal_visitor() { - eventual = false; // faux au départ + eventual = false; universal = false; } @@ -179,12 +169,12 @@ namespace spot return; case binop::U: if (node_type(f1) == node_type_form_visitor::Const) - if (((const constant*)f1)->val() == constant::True) + if (dynamic_cast(f1)->val() == constant::True) eventual = true; return; case binop::R: - if (node_type(f1) != node_type_form_visitor::Const) - if (((const constant*)f1)->val() == constant::False) + if (node_type(f1) == node_type_form_visitor::Const) + if (dynamic_cast(f1)->val() == constant::False) universal = true; return; } @@ -201,13 +191,13 @@ namespace spot eventual = true; universal = true; for (unsigned i = 0; i < mos; ++i){ - if ( !(recurse_ev(mo->nth(i))) ){ + if (!(recurse_ev(mo->nth(i)))){ eventual = false; break; } } for (unsigned i = 0; i < mos; ++i){ - if ( !(recurse_un(mo->nth(i))) ){ + if (!(recurse_un(mo->nth(i)))){ universal = false; break; } @@ -259,25 +249,13 @@ namespace spot inf_form_right_recurse_visitor(const formula *f) { this->f = f; - result_ = false; // faux au départ + result_ = false; } virtual ~inf_form_right_recurse_visitor() { } - /* - bool special_case(const formula* f2,binop::operator op) - { - const binop* b = (const binop*)f; - const binop* b2 = (const binop*)f2; - if ((b != NULL) && (b2 != NULL) && - (b->op() == b2_>op() == op)) - if (inf_form(b2->first(),b->first()) - && inf_form(b2->second(),b->second()) ) - return true; - return false; - } - */ + int result() const { @@ -287,7 +265,7 @@ namespace spot void visit(const atomic_prop* ap) { - if ((const atomic_prop*)f == ap) + if (dynamic_cast(f) == ap) result_ = true; } @@ -312,18 +290,24 @@ namespace spot const formula* tmp = NULL; switch (uo->op()) { - case unop::Not:// à gérer !! + case unop::Not: + if (uo == f) + result_ = true; return; - case unop::X:// à gérer !! + case unop::X: + if (node_type(f) == node_type_form_visitor::Unop) + if (dynamic_cast(f)->op() == unop::X) { + result_ = inf_form(dynamic_cast(f)->child(),f1); + } return; case unop::F: - // F(a) = true U a + /* F(a) = true U a */ result_ = inf_form(f,f1); return; case unop::G: - // G(a) = false R a + /* G(a) = false R a */ tmp = constant::false_instance(); - if ( inf_form(f,tmp) ) + if (inf_form(f,tmp)) result_ = true; spot::ltl::destroy(tmp); return; @@ -344,11 +328,11 @@ namespace spot case binop::Implies: return; case binop::U: - if ( (inf_form(f,f2)) ) + if ((inf_form(f,f2))) result_ = true; return; case binop::R: - if ( (inf_form(f,f1)) && (inf_form(f,f2)) ) + if ((inf_form(f,f1)) && (inf_form(f,f2))) result_ = true; return; } @@ -366,13 +350,13 @@ namespace spot { case multop::And: for (unsigned i = 0; (i < mos) ; ++i) - if ( !(inf_form(f,mo->nth(i))) ) + if (!(inf_form(f,mo->nth(i)))) return; result_ = true; break; case multop::Or: for (unsigned i = 0; i < mos && !result_; ++i) - if ( (inf_form(f,mo->nth(i))) ) + if ((inf_form(f,mo->nth(i)))) result_ = true; break; } @@ -388,7 +372,7 @@ namespace spot } protected: - bool result_; // true si f < f1, false sinon. + bool result_; /* true if f < f1, false otherwise. */ const formula* f; }; @@ -412,14 +396,23 @@ namespace spot { if ((node_type(f) == node_type_form_visitor::Binop) && (node_type(f2) == node_type_form_visitor::Binop)) - if (((const binop*)f)->op() == ((const binop*)f2)->op()) - if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first()) - && inf_form(((const binop*)f2)->second(), - ((const binop*)f)->second())) + if (dynamic_cast(f)->op() == dynamic_cast(f2)->op()) + if (inf_form(dynamic_cast(f2)->first(),dynamic_cast(f)->first()) + && inf_form(dynamic_cast(f2)->second(),dynamic_cast(f)->second())) return true; return false; } + bool nodeX() + { + /* + if (node_type(f) == node_type_form_visitor::Unop) + if (dynamic_cast(f)->op() == unop::X) + return true; + */ + return false; + } + int result() const { @@ -429,6 +422,7 @@ namespace spot void visit(const atomic_prop* ap) { + if (this->nodeX()) return; inf_form_right_recurse_visitor v(ap); const_cast(f)->accept(v); result_ = v.result(); @@ -437,6 +431,7 @@ namespace spot void visit(const constant* c) { + if (this->nodeX()) return; inf_form_right_recurse_visitor v(c); switch (c->val()) { @@ -466,32 +461,34 @@ namespace spot return; case unop::X: if (node_type(f) == node_type_form_visitor::Unop) - if (((const unop*)f)->op() == unop::X) { - result_ = inf_form(f1,((const unop*)f)->child()); + if (dynamic_cast(f)->op() == unop::X) { + result_ = inf_form(f1,dynamic_cast(f)->child()); } return; case unop::F: - // F(a) = true U a + if (this->nodeX()) return; + /* F(a) = true U a */ tmp = binop::instance(binop::U,constant::true_instance(),clone(f1)); if (this->special_case(tmp)){ result_ = true; spot::ltl::destroy(tmp); return; } - if ( inf_form(tmp,f) ) + if (inf_form(tmp,f)) result_ = true; spot::ltl::destroy(tmp); return; case unop::G: - // F(a) = false R a + if (this->nodeX()) return; + /* F(a) = false R a */ tmp = binop::instance(binop::R, - constant::false_instance(), clone(f1)); + constant::false_instance(),clone(f1)); if (this->special_case(tmp)){ result_ = true; spot::ltl::destroy(tmp); return; } - if ( inf_form(f1,f) ) + if (inf_form(f1,f)) result_ = true; spot::ltl::destroy(tmp); return; @@ -503,6 +500,7 @@ namespace spot void visit(const binop* bo) { + if (this->nodeX()) return; if (this->special_case(bo)) { @@ -519,11 +517,11 @@ namespace spot case binop::Implies: return; case binop::U: - if ( (inf_form(f1,f)) && (inf_form(f2,f)) ) + if ((inf_form(f1,f)) && (inf_form(f2,f))) result_ = true; return; case binop::R: - if ( (inf_form(f2,f)) ) + if ((inf_form(f2,f))) result_ = true; return; } @@ -534,19 +532,20 @@ namespace spot void visit(const multop* mo) { - if (mo == NULL); + if (this->nodeX()) return; + multop::type op = mo->op(); unsigned mos = mo->size(); switch (op) { case multop::And: for (unsigned i = 0; (i < mos) && !result_ ; ++i) - if ( (inf_form(mo->nth(i),f)) ) + if ((inf_form(mo->nth(i),f))) result_ = true; break; case multop::Or: for (unsigned i = 0; i < mos ; ++i) - if ( !(inf_form(mo->nth(i),f)) ) + if (!(inf_form(mo->nth(i),f))) return; result_ = true; break; @@ -554,21 +553,21 @@ namespace spot } protected: - bool result_; // true if f1 < f, 1 otherwise. + bool result_; /* true if f1 < f, 1 otherwise. */ const formula* f; }; bool inf_form(const formula* f1, const formula* f2) { - // f1 and f2 are unabbreviate + /* f1 and f2 are unabbreviate */ if (f1 == f2) return true; inf_form_left_recurse_visitor v1(f2); inf_form_right_recurse_visitor v2(f1); - if ( (node_type(f1) == node_type_form_visitor::Const) && - (node_type(f2) == node_type_form_visitor::Const) ) - if ( (((const constant*)f2)->val() == constant::True) || - (((const constant*)f1)->val() == constant::False) ) + if ((node_type(f1) == node_type_form_visitor::Const) && + (node_type(f2) == node_type_form_visitor::Const)) + if ((dynamic_cast(f2)->val() == constant::True) || + (dynamic_cast(f1)->val() == constant::False)) { return true; } diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index b8897c066..bed16b20c 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -32,19 +32,13 @@ namespace spot namespace ltl { - - //class unabbreviate_FG_visitor::unabbreviate_logic_visitor() - class reduce_form_visitor : public visitor { public: - reduce_form_visitor() + reduce_form_visitor(option o) { - /* - eventuality_ = false; - universality_ = false; - */ + this->o = o; } virtual ~reduce_form_visitor() @@ -57,20 +51,6 @@ namespace spot return result_; } - /* - bool - is_eventuality() - { - return eventuality_; - } - - bool - is_universality() - { - return universality_; - } - */ - void visit(atomic_prop* ap) { @@ -111,14 +91,14 @@ namespace spot case unop::F: /* if f is class of eventuality then F(f)=f */ - if (!is_eventual(result_)) { + if (!is_eventual(result_) || (o == Inf)) { result_ = unop::instance(unop::F, result_); } return; case unop::G: /* if f is class of universality then G(f)=f */ - if (!is_universal(result_)) { + if (!is_universal(result_) || (o == Inf)) { result_ = unop::instance(unop::G, result_); } return; @@ -134,86 +114,85 @@ namespace spot /* if b is of class eventuality then a U b = b if b is of class universality then a R b = b */ - if ( ( is_eventual(f2) && ( (bo->op()) == binop::U )) || - ( is_universal(f2) && ( (bo->op()) == binop::R )) ) - { - result_ = f2; - return; - } - + if (o != Inf) { + if ((is_eventual(f2) && ((bo->op()) == binop::U)) || + (is_universal(f2) && ((bo->op()) == binop::R))) + { + result_ = f2; + return; + } + } /* case of implies */ formula* f1 = recurse(bo->first()); - bool inf = inf_form(f1,f2); - bool infinv = inf_form(f2,f1); - //binop* ftmp = NULL; - bool infnegleft = infneg_form(f2,f1,0); - bool infnegright = infneg_form(f2,f1,1); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - result_ = binop::instance(bo->op(), f1, f2); - return; + if (o != EventualUniversal) { + bool inf = inf_form(f1,f2); + bool infinv = inf_form(f2,f1); + bool infnegleft = infneg_form(f2,f1,0); + bool infnegright = infneg_form(f2,f1,1); - case binop::U: - /* a < b => a U b = b */ - if (inf) - { - result_ = f2; - spot::ltl::destroy(f1); - return; - } - /* !b < a => a U b = Fb */ - if (infnegleft) - { - result_ = unop::instance(unop::F, f2); - spot::ltl::destroy(f1); - return; - } - /* a < b => a U (b U c) = (b U c) */ - if (node_type(f2) == node_type_form_visitor::Binop) - if (((binop*)f2)->op() == binop::U) - if (inf_form(f1,((binop*)f2)->first())){ + switch (bo->op()) + { + case binop::Xor: + case binop::Equiv: + case binop::Implies: + break;; + + case binop::U: + /* a < b => a U b = b */ + if (inf) + { result_ = f2; spot::ltl::destroy(f1); return; } - result_ = binop::instance(binop::U, - f1, f2); - return; + /* !b < a => a U b = Fb */ + if (infnegleft) + { + result_ = unop::instance(unop::F, f2); + spot::ltl::destroy(f1); + return; + } + /* a < b => a U (b U c) = (b U c) */ + if (node_type(f2) == node_type_form_visitor::Binop) + if (dynamic_cast(f2)->op() == binop::U) + if (inf_form(f1,dynamic_cast(f2)->first())) + { + result_ = f2; + spot::ltl::destroy(f1); + return; + } + break; - case binop::R: - /* b < a => a R b = b */ - if (infinv) - { - result_ = f2; - spot::ltl::destroy(f1); - return; - } - /* b < !a => a R b = Gb */ - if (infnegright) - { - result_ = unop::instance(unop::G, f2); - spot::ltl::destroy(f1); - return; - } - /* b < a => a R (b R c) = b R c */ - if (node_type(f2) == node_type_form_visitor::Binop) - if (((binop*)f2)->op() == binop::R) - if (inf_form(((binop*)f2)->first(),f1)){ + case binop::R: + /* b < a => a R b = b */ + if (infinv) + { result_ = f2; spot::ltl::destroy(f1); return; } + /* b < !a => a R b = Gb */ + if (infnegright) + { + result_ = unop::instance(unop::G, f2); + spot::ltl::destroy(f1); + return; + } + /* b < a => a R (b R c) = b R c */ + if (node_type(f2) == node_type_form_visitor::Binop) + if (dynamic_cast(f2)->op() == binop::R) + if (inf_form(dynamic_cast(f2)->first(),f1)) + { + result_ = f2; + spot::ltl::destroy(f1); + return; + } + break; - result_ = binop::instance(binop::R, - f1, f2); - return; - } - /* Unreachable code. */ - assert(0); + } + } + result_ = binop::instance(bo->op(), f1, f2); } void @@ -229,109 +208,86 @@ namespace spot for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); - switch (mo->op()) - { + if (o != EventualUniversal){ + switch (mo->op()) + { - case multop::Or: - index = indextmp = res->begin(); - if (index != res->end()) - { - f1 = *index; - index++; - } - for (; index != res->end();index++) - { - f2 = *index; - /* a < b => a + b = b */ - if (inf_form(f1,f2)) // f1 < f2 - { - f1 = f2; - spot::ltl::destroy(*indextmp); - res->erase(indextmp); - indextmp = index; - index--; - } - else if (inf_form(f2,f1)) // f2 < f1 - { - spot::ltl::destroy(*index); - res->erase(index); - index--; - } - } - break; - - case multop::And: - index = indextmp = res->begin(); - if (mos) - { - f1 = mo->nth(0); - index++; - } - for (; index != res->end(); index++) - { - f2 = *index; - /* a < b => a & b = a */ - if (inf_form(f1,f2)) // f1 < f2 - { - spot::ltl::destroy(*index); - res->erase(index); - index--; - } - else if (inf_form(f2,f1)) // f2 < f1 - { - f1 = f2; - spot::ltl::destroy(*indextmp); - res->erase(indextmp); - indextmp = index; - index--; - } - } - break; - } - - /* f1 < !f2 => f1 & f2 = false - !f1 < f2 => f1 | f2 = true */ - - for (index = res->begin(); index != res->end(); index++){ - for (indextmp = res->begin(); indextmp != res->end(); indextmp++){ - if (index != indextmp){ - if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) { - for (multop::vec::iterator j = res->begin(); j != res->end(); j++){ - spot::ltl::destroy(*j); + case multop::Or: + index = indextmp = res->begin(); + if (index != res->end()) + { + f1 = *index; + index++; } - if (mo->op() == multop::Or) - result_ = constant::true_instance(); - else - result_ = constant::false_instance(); - return; - } + for (; index != res->end();index++) + { + f2 = *index; + /* a < b => a + b = b */ + if (inf_form(f1,f2)) // f1 < f2 + { + f1 = f2; + spot::ltl::destroy(*indextmp); + res->erase(indextmp); + indextmp = index; + index--; + } + else if (inf_form(f2,f1)) // f2 < f1 + { + spot::ltl::destroy(*index); + res->erase(index); + index--; + } + } + break; - /* - if ((constant*)(*index) != NULL) - if (((((constant*)(*index))->val() == constant::True) && - (mo->op() == multop::Or)) || - (((((constant*)(*index))->val() == constant::False)) - && (mo->op() == multop::And)) - ) { - //std::cout << "constant" << std::endl; - for (multop::vec::iterator j = res->begin(); j != res->end(); j++){ + case multop::And: + index = indextmp = res->begin(); + if (mos) + { + f1 = mo->nth(0); + index++; + } + for (; index != res->end(); index++) + { + f2 = *index; + /* a < b => a & b = a */ + if (inf_form(f1,f2)) // f1 < f2 + { + spot::ltl::destroy(*index); + res->erase(index); + index--; + } + else if (inf_form(f2,f1)) // f2 < f1 + { + f1 = f2; + spot::ltl::destroy(*indextmp); + res->erase(indextmp); + indextmp = index; + index--; + } + } + break; + } + + /* f1 < !f2 => f1 & f2 = false + !f1 < f2 => f1 | f2 = true */ + for (index = res->begin(); index != res->end(); index++) { + for (indextmp = res->begin(); indextmp != res->end(); indextmp++) { + if (index != indextmp){ + if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) { + for (multop::vec::iterator j = res->begin(); j != res->end(); j++) { spot::ltl::destroy(*j); } if (mo->op() == multop::Or) result_ = constant::true_instance(); else result_ = constant::false_instance(); - - std::cout << "2" << std::endl; - spot::ltl::dump(std::cout,mo); return; } - */ - + } } } } - if (res->size()) { result_ = multop::instance(mo->op(),res); return; @@ -342,36 +298,41 @@ namespace spot formula* recurse(formula* f) { - return reduce_form(f); + return reduce_form(f,o); } protected: formula* result_; - /* - bool eventuality_; - bool universality_; - */ + option o; }; formula* - reduce_form(const formula* f) + reduce_form(const formula* f, option o) { - spot::ltl::formula* ftmp1; - spot::ltl::formula* ftmp2; - reduce_form_visitor v; + spot::ltl::formula* ftmp1 = NULL; + spot::ltl::formula* ftmp2 = NULL; + reduce_form_visitor v(o); - ftmp1 = spot::ltl::basic_reduce_form(f); - const_cast(ftmp1)->accept(v); - ftmp2 = spot::ltl::basic_reduce_form(v.result()); + if (o == BRI) { + ftmp1 = spot::ltl::basic_reduce_form(f); + const_cast(ftmp1)->accept(v); + ftmp2 = spot::ltl::basic_reduce_form(v.result()); + spot::ltl::destroy(ftmp1); + spot::ltl::destroy(v.result()); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(v.result()); + return ftmp2; + } + else { + const_cast(f)->accept(v); + return v.result(); + } - return ftmp2; + /* unreachable code */ + assert(0); } formula* - reduce(const formula* f) + reduce(const formula* f, option o) { spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp2; @@ -379,14 +340,27 @@ namespace spot ftmp1 = spot::ltl::unabbreviate_logic(f); ftmp2 = spot::ltl::negative_normal_form(ftmp1); - ftmp3 = spot::ltl::reduce_form(ftmp2); + switch (o) { + case Base: + ftmp3 = spot::ltl::basic_reduce_form(ftmp2); + break; + case Inf: + ftmp3 = spot::ltl::reduce_form(ftmp2,o); + break; + case EventualUniversal: + ftmp3 = spot::ltl::reduce_form(ftmp2,o); + break; + case BRI: + ftmp3 = spot::ltl::reduce_form(ftmp2); + break; + default: + assert(0); + } spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); return ftmp3; - } - } } diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh index 3e063d9b3..8a34547f9 100644 --- a/src/ltlvisit/reducform.hh +++ b/src/ltlvisit/reducform.hh @@ -25,38 +25,48 @@ #include "ltlast/formula.hh" #include "ltlast/visitor.hh" -// For debog +// For debug #include "ltlvisit/dump.hh" namespace spot { namespace ltl { - formula* reduce(const formula* f); + /// \brief Reduce a formula \a f using Basic rewriting, implies relation, + /// and class of eventuality and univerality formula. + /// Put the formula in negative normal form with + /// spot::ltl::negative_normal_form. + /// option are: + /// Base for spot::ltl::Basic_reduce_form, + /// Inf for spot::ltl:: reduce_inf_form, + /// EventualUniversal for spot::ltl::reduce_eventuality_universality_form, + /// BRI for spot::ltl::reduce_form. - /* Basic rewriting */ + enum option {Base, Inf, EventualUniversal, BRI}; + formula* reduce(const formula* f, option o = BRI); + + /// Implement basic rewriting. formula* basic_reduce_form(const formula* f); - /* formula rewriting using univerality, eventuality, - implies and basic_reduce_form */ - formula* reduce_form(const formula* f); + /// Use by spot::ltl::reduce + /// 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 */ + /// detect easy case of implies. bool inf_form(const formula* f1, const formula* f2); - /* true if f1 < f2, false otherwise */ + /// true if f1 < f2, false otherwise. bool infneg_form(const formula* f1, const formula* f2, int n); - /* true if !f1 < f2, false otherwise */ + /// true if !f1 < f2, false otherwise. - /* detect if a formula is of class eventuality or universality */ + /// detect if a formula is of class eventuality or universality. bool is_eventual(const formula* f); bool is_universal(const formula* f); - /* detect if a formula is of form GF or FG */ - bool is_GF(const formula* f); - bool is_FG(const formula* f); - - /* To know the first node of a formula */ + /// For test. + int form_length(const formula* f); + /// To know the first node of a formula. class node_type_form_visitor : public const_visitor { public: @@ -72,14 +82,11 @@ namespace spot protected: type result_; }; - node_type_form_visitor::type node_type(const formula* f); - /* Obsolete */ - int nb_term_multop(const formula* f); - formula* reduce_inf_form(const formula* f); /* Obsolete */ - int form_length(const formula* f); /* For test */ - + /// detect if a formula is of form GF or FG. + bool is_GF(const formula* f); + bool is_FG(const formula* f); } }