From 69169970a233643c9eedfe94d8a0370d354b21bb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 10 May 2004 17:26:32 +0000 Subject: [PATCH] * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh: Fix copyright year, these files were created in 2004. --- ChangeLog | 5 ++ src/ltltest/inf.cc | 14 +++--- src/ltltest/inf.test | 4 +- src/ltltest/reduc.test | 12 ++--- src/ltlvisit/formlength.cc | 20 ++++---- src/ltlvisit/reducform.cc | 94 +++++++++++++++++++------------------- src/ltlvisit/reducform.hh | 20 ++++---- 7 files changed, 87 insertions(+), 82 deletions(-) diff --git a/ChangeLog b/ChangeLog index da4a9fbc1..d1dd641b6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2004-05-10 Alexandre Duret-Lutz + * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, + src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc, + src/ltlvisit/reducform.hh: Fix copyright year, these files were + created in 2004. + * src/sanity/80columns.test: New file. * src/sanity/Makefile.am (check-local): Run it. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, diff --git a/src/ltltest/inf.cc b/src/ltltest/inf.cc index 77ab7496e..e9200d5a9 100644 --- a/src/ltltest/inf.cc +++ b/src/ltltest/inf.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. // @@ -54,28 +54,28 @@ main(int argc, char** argv) spot::ltl::parse_error_list p2; f2 = spot::ltl::parse(argv[2], p2); - + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; - + std::string f1s = spot::ltl::to_string(f1); std::string f2s = spot::ltl::to_string(f2); int exit_return = 0; - + std::cout << "Test f1 < f2" << std::endl; if (spot::ltl::inf_form(f1,f2)) { std::cout << f1s << " < " << f2s << std::endl; exit_return = 1; } - - /* + + /* std::cout << "Test !f1 < f2" << std::endl; if (spot::ltl::infneg_form(f1,f2,0)) { std::cout << "!(" << f1s << ") < " << f2s << std::endl; exit_return = 2; } - + std::cout << "Test f1 < !f2" << std::endl; if (spot::ltl::infneg_form(f1,f2,1)) { std::cout << f1s << " < !(" << f2s << ")" << std::endl; diff --git a/src/ltltest/inf.test b/src/ltltest/inf.test index 852ebd151..a889bf4ed 100755 --- a/src/ltltest/inf.test +++ b/src/ltltest/inf.test @@ -1,5 +1,5 @@ #! /bin/sh -# 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. # @@ -53,7 +53,7 @@ run 1 ./inf 'a R b' 'b' run 1 ./inf 'a R b' '1' run 1 ./inf 'a U b' '1 U b' -run 1 ./inf 'a R b' '1 R b' +run 1 ./inf 'a R b' '1 R b' run 1 ./inf 'b * (a U b)' 'a U b' run 1 ./inf 'a U b' 'c + (a U b)' diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test index 41a0ba897..a39067f51 100755 --- a/src/ltltest/reduc.test +++ b/src/ltltest/reduc.test @@ -1,5 +1,5 @@ #! /bin/sh -# 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. # @@ -26,24 +26,24 @@ #. ./defs || exit 1 if [ $1 ]; then FICH=$1 -else +else FICH="formules.ltl" fi ##################################### rm output? result_bri.test -f -for opt in bri ##b r i br bi rb ri ib ir bri bir rbi rib ibr irb +for opt in bri ##b r i br bi rb ri ib ir bri bir rbi rib ibr irb do for f in `awk '{print $1}' $FICH` do if [ ! $f = "####" ]; then #echo $f; - if ./reduc "$f" >> result_$opt.test; + if ./reduc "$f" >> result_$opt.test; then #echo $f >> output1 # if ../tgbatest/ltl2tgba -f "$f" >> output1; then #automate FM # echo "" >> output1 - # else + # else # echo $f; # fi #echo "'$f' is reduce ($NB)" @@ -131,4 +131,4 @@ X(((p1)R(1))*((0)R((p0)+(p1)))) ((X(0))+((0)R(p2)))U(((p0)R((p2)*(p2)))R(X(p2))) (p1)R(((p2)R(1))R(((p1)U((1)U(p0)))R((p2)U(0)))) (((X(p0))R(X(p0)))R((p0)R(1)))*((0)R((p1)R(0))) -(((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2)) \ No newline at end of file +(((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2)) diff --git a/src/ltlvisit/formlength.cc b/src/ltlvisit/formlength.cc index 8c2f26261..b111cf237 100644 --- a/src/ltlvisit/formlength.cc +++ b/src/ltlvisit/formlength.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. // @@ -35,17 +35,17 @@ namespace spot class length_form_visitor : public const_visitor { public: - + length_form_visitor() { result_ = 0; } - + virtual ~length_form_visitor() { } - int + int result() const { return result_; @@ -53,32 +53,32 @@ namespace spot void visit(const atomic_prop* ap) - { + { if (ap); result_ = 1; } - + void visit(const constant* c) { if (c); result_ = 1; } - + void visit(const unop* uo) { if (uo); result_ = 1 + form_length(uo->child()); } - + void visit(const binop* bo) { if (bo); result_ = 1 + form_length(bo->first()) + form_length(bo->second()); } - + void visit(const multop* mo) { @@ -86,7 +86,7 @@ namespace spot for (unsigned i = 0; i < mos; ++i) result_ += form_length(mo->nth(i)); } - + protected: int result_; // size of the formula }; diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index 94151328f..b8897c066 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.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. // @@ -32,13 +32,13 @@ namespace spot namespace ltl { - + //class unabbreviate_FG_visitor::unabbreviate_logic_visitor() - + class reduce_form_visitor : public visitor { public: - + reduce_form_visitor() { /* @@ -46,38 +46,38 @@ namespace spot universality_ = false; */ } - + virtual ~reduce_form_visitor() { } - formula* + formula* result() const { return result_; } - + /* bool is_eventuality() { return eventuality_; } - + bool is_universality() { return universality_; } */ - + void visit(atomic_prop* ap) - { + { formula* f = ap->ref(); result_ = f; } - + void visit(constant* c) { @@ -93,7 +93,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(unop* uo) { @@ -109,7 +109,7 @@ namespace spot result_ = unop::instance(unop::X, result_); return; - case unop::F: + case unop::F: /* if f is class of eventuality then F(f)=f */ if (!is_eventual(result_)) { result_ = unop::instance(unop::F, result_); @@ -126,21 +126,21 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(binop* bo) { formula* f2 = recurse(bo->second()); - + /* if b is of class eventuality then a U b = b if b is of class universality then a R b = b */ if ( ( is_eventual(f2) && ( (bo->op()) == binop::U )) || - ( is_universal(f2) && ( (bo->op()) == binop::R )) ) + ( is_universal(f2) && ( (bo->op()) == binop::R )) ) { - result_ = f2; + result_ = f2; return; } - + /* case of implies */ formula* f1 = recurse(bo->first()); bool inf = inf_form(f1,f2); @@ -148,7 +148,7 @@ namespace spot //binop* ftmp = NULL; bool infnegleft = infneg_form(f2,f1,0); bool infnegright = infneg_form(f2,f1,1); - + switch (bo->op()) { case binop::Xor: @@ -159,8 +159,8 @@ namespace spot case binop::U: /* a < b => a U b = b */ - if (inf) - { + if (inf) + { result_ = f2; spot::ltl::destroy(f1); return; @@ -179,14 +179,14 @@ namespace spot result_ = f2; spot::ltl::destroy(f1); return; - } + } result_ = binop::instance(binop::U, f1, f2); return; case binop::R: /* b < a => a R b = b */ - if (infinv) + if (infinv) { result_ = f2; spot::ltl::destroy(f1); @@ -206,7 +206,7 @@ namespace spot result_ = f2; spot::ltl::destroy(f1); return; - } + } result_ = binop::instance(binop::R, f1, f2); @@ -215,7 +215,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(multop* mo) { @@ -225,7 +225,7 @@ namespace spot multop::vec* res = new multop::vec; multop::vec::iterator index; multop::vec::iterator indextmp; - + for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); @@ -234,7 +234,7 @@ namespace spot case multop::Or: index = indextmp = res->begin(); - if (index != res->end()) + if (index != res->end()) { f1 = *index; index++; @@ -260,7 +260,7 @@ namespace spot } break; - case multop::And: + case multop::And: index = indextmp = res->begin(); if (mos) { @@ -288,10 +288,10 @@ namespace spot } break; } - - /* f1 < !f2 => f1 & f2 = false + + /* 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){ @@ -301,16 +301,16 @@ namespace spot } if (mo->op() == multop::Or) result_ = constant::true_instance(); - else + else result_ = constant::false_instance(); return; } - + /* if ((constant*)(*index) != NULL) if (((((constant*)(*index))->val() == constant::True) && - (mo->op() == multop::Or)) || - (((((constant*)(*index))->val() == constant::False)) + (mo->op() == multop::Or)) || + (((((constant*)(*index))->val() == constant::False)) && (mo->op() == multop::And)) ) { //std::cout << "constant" << std::endl; @@ -319,26 +319,26 @@ namespace spot } if (mo->op() == multop::Or) result_ = constant::true_instance(); - else + 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; } assert(0); } - + formula* recurse(formula* f) { @@ -355,18 +355,18 @@ namespace spot formula* reduce_form(const formula* f) - { + { spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp2; reduce_form_visitor v; - + 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()); - + return ftmp2; } @@ -378,12 +378,12 @@ namespace spot spot::ltl::formula* ftmp3; ftmp1 = spot::ltl::unabbreviate_logic(f); - ftmp2 = spot::ltl::negative_normal_form(ftmp1); + ftmp2 = spot::ltl::negative_normal_form(ftmp1); ftmp3 = spot::ltl::reduce_form(ftmp2); - + spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); - + return ftmp3; } diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh index 17552e029..3e063d9b3 100644 --- a/src/ltlvisit/reducform.hh +++ b/src/ltlvisit/reducform.hh @@ -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. // @@ -36,17 +36,17 @@ namespace spot /* Basic rewriting */ formula* basic_reduce_form(const formula* f); - - /* formula rewriting using univerality, eventuality, + + /* formula rewriting using univerality, eventuality, implies and basic_reduce_form */ formula* reduce_form(const formula* f); /* detect easy case of implies */ - bool inf_form(const formula* f1, const formula* f2); + bool inf_form(const formula* f1, const formula* f2); /* true if f1 < f2, false otherwise */ - bool infneg_form(const formula* f1, const formula* f2, int n); + bool infneg_form(const formula* f1, const formula* f2, int n); /* true if !f1 < f2, false otherwise */ - + /* detect if a formula is of class eventuality or universality */ bool is_eventual(const formula* f); bool is_universal(const formula* f); @@ -54,9 +54,9 @@ namespace spot /* 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 */ - + class node_type_form_visitor : public const_visitor { public: @@ -72,14 +72,14 @@ 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 */ - + } }