alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test,

Browse source 
src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/reducform.hh: Fix copyright year, these files were
created in 2004.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-10 17:26:32 +00:00
parent 83de4264cb
commit 69169970a2
7 changed files with 87 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,5 +1,10 @@
2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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/80columns.test: New file.
* src/sanity/Makefile.am (check-local): Run it. * src/sanity/Makefile.am (check-local): Run it.
* src/ltltest/equals.test, src/ltltest/lunabbrev.test, * src/ltltest/equals.test, src/ltltest/lunabbrev.test,

14
src/ltltest/inf.cc
View file

@ -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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -54,28 +54,28 @@ main(int argc, char** argv)
spot::ltl::parse_error_list p2; spot::ltl::parse_error_list p2;
f2 = spot::ltl::parse(argv[2], p2); f2 = spot::ltl::parse(argv[2], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
return 2; return 2;
std::string f1s = spot::ltl::to_string(f1); std::string f1s = spot::ltl::to_string(f1);
std::string f2s = spot::ltl::to_string(f2); std::string f2s = spot::ltl::to_string(f2);
int exit_return = 0; int exit_return = 0;
std::cout << "Test f1 < f2" << std::endl; std::cout << "Test f1 < f2" << std::endl;
if (spot::ltl::inf_form(f1,f2)) { if (spot::ltl::inf_form(f1,f2)) {
std::cout << f1s << " < " << f2s << std::endl; std::cout << f1s << " < " << f2s << std::endl;
exit_return = 1; exit_return = 1;
} }
/* /*
std::cout << "Test !f1 < f2" << std::endl; std::cout << "Test !f1 < f2" << std::endl;
if (spot::ltl::infneg_form(f1,f2,0)) { if (spot::ltl::infneg_form(f1,f2,0)) {
std::cout << "!(" << f1s << ") < " << f2s << std::endl; std::cout << "!(" << f1s << ") < " << f2s << std::endl;
exit_return = 2; exit_return = 2;
} }
std::cout << "Test f1 < !f2" << std::endl; std::cout << "Test f1 < !f2" << std::endl;
if (spot::ltl::infneg_form(f1,f2,1)) { if (spot::ltl::infneg_form(f1,f2,1)) {
std::cout << f1s << " < !(" << f2s << ")" << std::endl; std::cout << f1s << " < !(" << f2s << ")" << std::endl;

4
src/ltltest/inf.test
View file

@ -1,5 +1,5 @@
#! /bin/sh #! /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 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # 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 R b' '1'
run 1 ./inf 'a U b' '1 U b' 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 'b * (a U b)' 'a U b'
run 1 ./inf 'a U b' 'c + (a U b)' run 1 ./inf 'a U b' 'c + (a U b)'

12
src/ltltest/reduc.test
View file

@ -1,5 +1,5 @@
#! /bin/sh #! /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 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
@ -26,24 +26,24 @@
#. ./defs || exit 1 #. ./defs || exit 1
if [ $1 ]; then if [ $1 ]; then
FICH=$1 FICH=$1
else else
FICH="formules.ltl" FICH="formules.ltl"
fi fi
##################################### #####################################
rm output? result_bri.test -f 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 do
for f in `awk '{print $1}' $FICH` for f in `awk '{print $1}' $FICH`
do do
if [ ! $f = "####" ]; then if [ ! $f = "####" ]; then
#echo $f; #echo $f;
if ./reduc "$f" >> result_$opt.test; if ./reduc "$f" >> result_$opt.test;
then then
#echo $f >> output1 #echo $f >> output1
# if ../tgbatest/ltl2tgba -f "$f" >> output1; then #automate FM # if ../tgbatest/ltl2tgba -f "$f" >> output1; then #automate FM
# echo "" >> output1 # echo "" >> output1
# else # else
# echo $f; # echo $f;
# fi # fi
#echo "'$f' is reduce ($NB)" #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))) ((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)))) (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))) (((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)) (((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2))

20
src/ltlvisit/formlength.cc
View file

@ -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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -35,17 +35,17 @@ namespace spot
class length_form_visitor : public const_visitor class length_form_visitor : public const_visitor
{ {
public: public:
length_form_visitor() length_form_visitor()
{ {
result_ = 0; result_ = 0;
} }
virtual ~length_form_visitor() virtual ~length_form_visitor()
{ {
} }
int int
result() const result() const
{ {
return result_; return result_;
@ -53,32 +53,32 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
if (ap); if (ap);
result_ = 1; result_ = 1;
} }
void void
visit(const constant* c) visit(const constant* c)
{ {
if (c); if (c);
result_ = 1; result_ = 1;
} }
void void
visit(const unop* uo) visit(const unop* uo)
{ {
if (uo); if (uo);
result_ = 1 + form_length(uo->child()); result_ = 1 + form_length(uo->child());
} }
void void
visit(const binop* bo) visit(const binop* bo)
{ {
if (bo); if (bo);
result_ = 1 + form_length(bo->first()) + form_length(bo->second()); result_ = 1 + form_length(bo->first()) + form_length(bo->second());
} }
void void
visit(const multop* mo) visit(const multop* mo)
{ {
@ -86,7 +86,7 @@ namespace spot
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
result_ += form_length(mo->nth(i)); result_ += form_length(mo->nth(i));
} }
protected: protected:
int result_; // size of the formula int result_; // size of the formula
}; };

94
src/ltlvisit/reducform.cc
View file

@ -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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -32,13 +32,13 @@ namespace spot
namespace ltl namespace ltl
{ {
//class unabbreviate_FG_visitor::unabbreviate_logic_visitor() //class unabbreviate_FG_visitor::unabbreviate_logic_visitor()
class reduce_form_visitor : public visitor class reduce_form_visitor : public visitor
{ {
public: public:
reduce_form_visitor() reduce_form_visitor()
{ {
/* /*
@ -46,38 +46,38 @@ namespace spot
universality_ = false; universality_ = false;
*/ */
} }
virtual ~reduce_form_visitor() virtual ~reduce_form_visitor()
{ {
} }
formula* formula*
result() const result() const
{ {
return result_; return result_;
} }
/* /*
bool bool
is_eventuality() is_eventuality()
{ {
return eventuality_; return eventuality_;
} }
bool bool
is_universality() is_universality()
{ {
return universality_; return universality_;
} }
*/ */
void void
visit(atomic_prop* ap) visit(atomic_prop* ap)
{ {
formula* f = ap->ref(); formula* f = ap->ref();
result_ = f; result_ = f;
} }
void void
visit(constant* c) visit(constant* c)
{ {
@ -93,7 +93,7 @@ namespace spot
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);
} }
void void
visit(unop* uo) visit(unop* uo)
{ {
@ -109,7 +109,7 @@ namespace spot
result_ = unop::instance(unop::X, result_); result_ = unop::instance(unop::X, result_);
return; return;
case unop::F: case unop::F:
/* if f is class of eventuality then F(f)=f */ /* if f is class of eventuality then F(f)=f */
if (!is_eventual(result_)) { if (!is_eventual(result_)) {
result_ = unop::instance(unop::F, result_); result_ = unop::instance(unop::F, result_);
@ -126,21 +126,21 @@ namespace spot
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);
} }
void void
visit(binop* bo) visit(binop* bo)
{ {
formula* f2 = recurse(bo->second()); formula* f2 = recurse(bo->second());
/* if b is of class eventuality then a U b = b /* if b is of class eventuality then a U b = b
if b is of class universality then a R b = b */ if b is of class universality then a R b = b */
if ( ( is_eventual(f2) && ( (bo->op()) == binop::U )) || 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; return;
} }
/* case of implies */ /* case of implies */
formula* f1 = recurse(bo->first()); formula* f1 = recurse(bo->first());
bool inf = inf_form(f1,f2); bool inf = inf_form(f1,f2);
@ -148,7 +148,7 @@ namespace spot
//binop* ftmp = NULL; //binop* ftmp = NULL;
bool infnegleft = infneg_form(f2,f1,0); bool infnegleft = infneg_form(f2,f1,0);
bool infnegright = infneg_form(f2,f1,1); bool infnegright = infneg_form(f2,f1,1);
switch (bo->op()) switch (bo->op())
{ {
case binop::Xor: case binop::Xor:
@ -159,8 +159,8 @@ namespace spot
case binop::U: case binop::U:
/* a < b => a U b = b */ /* a < b => a U b = b */
if (inf) if (inf)
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
return; return;
@ -179,14 +179,14 @@ namespace spot
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
return; return;
} }
result_ = binop::instance(binop::U, result_ = binop::instance(binop::U,
f1, f2); f1, f2);
return; return;
case binop::R: case binop::R:
/* b < a => a R b = b */ /* b < a => a R b = b */
if (infinv) if (infinv)
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
@ -206,7 +206,7 @@ namespace spot
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
return; return;
} }
result_ = binop::instance(binop::R, result_ = binop::instance(binop::R,
f1, f2); f1, f2);
@ -215,7 +215,7 @@ namespace spot
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);
} }
void void
visit(multop* mo) visit(multop* mo)
{ {
@ -225,7 +225,7 @@ namespace spot
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
multop::vec::iterator index; multop::vec::iterator index;
multop::vec::iterator indextmp; multop::vec::iterator indextmp;
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i))); res->push_back(recurse(mo->nth(i)));
@ -234,7 +234,7 @@ namespace spot
case multop::Or: case multop::Or:
index = indextmp = res->begin(); index = indextmp = res->begin();
if (index != res->end()) if (index != res->end())
{ {
f1 = *index; f1 = *index;
index++; index++;
@ -260,7 +260,7 @@ namespace spot
} }
break; break;
case multop::And: case multop::And:
index = indextmp = res->begin(); index = indextmp = res->begin();
if (mos) if (mos)
{ {
@ -288,10 +288,10 @@ namespace spot
} }
break; break;
} }
/* f1 < !f2 => f1 & f2 = false /* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */ !f1 < f2 => f1 | f2 = true */
for (index = res->begin(); index != res->end(); index++){ for (index = res->begin(); index != res->end(); index++){
for (indextmp = res->begin(); indextmp != res->end(); indextmp++){ for (indextmp = res->begin(); indextmp != res->end(); indextmp++){
if (index != indextmp){ if (index != indextmp){
@ -301,16 +301,16 @@ namespace spot
} }
if (mo->op() == multop::Or) if (mo->op() == multop::Or)
result_ = constant::true_instance(); result_ = constant::true_instance();
else else
result_ = constant::false_instance(); result_ = constant::false_instance();
return; return;
} }
/* /*
if ((constant*)(*index) != NULL) if ((constant*)(*index) != NULL)
if (((((constant*)(*index))->val() == constant::True) && if (((((constant*)(*index))->val() == constant::True) &&
(mo->op() == multop::Or)) || (mo->op() == multop::Or)) ||
(((((constant*)(*index))->val() == constant::False)) (((((constant*)(*index))->val() == constant::False))
&& (mo->op() == multop::And)) && (mo->op() == multop::And))
) { ) {
//std::cout << "constant" << std::endl; //std::cout << "constant" << std::endl;
@ -319,26 +319,26 @@ namespace spot
} }
if (mo->op() == multop::Or) if (mo->op() == multop::Or)
result_ = constant::true_instance(); result_ = constant::true_instance();
else else
result_ = constant::false_instance(); result_ = constant::false_instance();
std::cout << "2" << std::endl; std::cout << "2" << std::endl;
spot::ltl::dump(std::cout,mo); spot::ltl::dump(std::cout,mo);
return; return;
} }
*/ */
} }
} }
} }
if (res->size()) { if (res->size()) {
result_ = multop::instance(mo->op(),res); result_ = multop::instance(mo->op(),res);
return; return;
} }
assert(0); assert(0);
} }
formula* formula*
recurse(formula* f) recurse(formula* f)
{ {
@ -355,18 +355,18 @@ namespace spot
formula* formula*
reduce_form(const formula* f) reduce_form(const formula* f)
{ {
spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp1;
spot::ltl::formula* ftmp2; spot::ltl::formula* ftmp2;
reduce_form_visitor v; reduce_form_visitor v;
ftmp1 = spot::ltl::basic_reduce_form(f); ftmp1 = spot::ltl::basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v); const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result()); ftmp2 = spot::ltl::basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp1);
spot::ltl::destroy(v.result()); spot::ltl::destroy(v.result());
return ftmp2; return ftmp2;
} }
@ -378,12 +378,12 @@ namespace spot
spot::ltl::formula* ftmp3; spot::ltl::formula* ftmp3;
ftmp1 = spot::ltl::unabbreviate_logic(f); 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); ftmp3 = spot::ltl::reduce_form(ftmp2);
spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2); spot::ltl::destroy(ftmp2);
return ftmp3; return ftmp3;
} }

20
src/ltlvisit/reducform.hh
View file

@ -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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -36,17 +36,17 @@ namespace spot
/* Basic rewriting */ /* Basic rewriting */
formula* basic_reduce_form(const formula* f); formula* basic_reduce_form(const formula* f);
/* formula rewriting using univerality, eventuality, /* formula rewriting using univerality, eventuality,
implies and basic_reduce_form */ implies and basic_reduce_form */
formula* reduce_form(const formula* f); formula* reduce_form(const formula* f);
/* detect easy case of implies */ /* 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 */ /* 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 */ /* 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_eventual(const formula* f);
bool is_universal(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 */ /* detect if a formula is of form GF or FG */
bool is_GF(const formula* f); bool is_GF(const formula* f);
bool is_FG(const formula* f); bool is_FG(const formula* f);
/* To know the first node of a formula */ /* To know the first node of a formula */
class node_type_form_visitor : public const_visitor class node_type_form_visitor : public const_visitor
{ {
public: public:
@ -72,14 +72,14 @@ namespace spot
protected: protected:
type result_; type result_;
}; };
node_type_form_visitor::type node_type(const formula* f); node_type_form_visitor::type node_type(const formula* f);
/* Obsolete */ /* Obsolete */
int nb_term_multop(const formula* f); int nb_term_multop(const formula* f);
formula* reduce_inf_form(const formula* f); /* Obsolete */ formula* reduce_inf_form(const formula* f); /* Obsolete */
int form_length(const formula* f); /* For test */ int form_length(const formula* f); /* For test */
} }
} }