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

* src/ltlvisit/Makefile.am: Copyright 2004.

Browse source 
* 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.
This commit is contained in:
martinez 2004-05-13 16:00:15 +00:00
parent f7e5fe0821
commit 4cd10c3dfc
9 changed files with 489 additions and 460 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2004-05-13 Thomas Martinez <martinez@src.lip6.fr>
* 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 <adl@src.lip6.fr> 2004-05-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltltest/reduc.test: Typo. * src/ltltest/reduc.test: Typo.

24
src/ltltest/inf.test
View file

@ -26,6 +26,27 @@
. ./defs || exit 1 . ./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 '1' '1'
run 1 ./inf '0' '0' 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' 'b'
run 1 ./inf 'a R b' '1' 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 U b' '1 U b'
run 1 ./inf 'a R b' '1 R b' run 1 ./inf 'a R b' '1 R b'

42
src/ltltest/reduc.cc
View file

@ -34,30 +34,45 @@
void void
syntax(char* prog) syntax(char* prog)
{ {
std::cerr << prog << " formula1 (formula2)?" << std::endl; std::cerr << prog << " option formula1 (formula2)?" << std::endl;
exit(2); exit(2);
} }
typedef spot::ltl::formula* ptrfunct(const spot::ltl::formula*);
int int
main(int argc, char** argv) main(int argc, char** argv)
{ {
if (argc < 2) if (argc < 3)
syntax(argv[0]); 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::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; 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; return 2;
if (argc == 3){ if (argc == 4){
spot::ltl::parse_error_list p2; spot::ltl::parse_error_list p2;
f2 = spot::ltl::parse(argv[2], p2); f2 = spot::ltl::parse(argv[3], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
return 2; return 2;
} }
@ -78,7 +93,7 @@ main(int argc, char** argv)
std::string f1s_before = spot::ltl::to_string(f1); std::string f1s_before = spot::ltl::to_string(f1);
ftmp1 = f1; ftmp1 = f1;
f1 = spot::ltl::reduce(f1); f1 = spot::ltl::reduce(f1,o);
ftmp2 = f1; ftmp2 = f1;
f1 = spot::ltl::unabbreviate_logic(f1); f1 = spot::ltl::unabbreviate_logic(f1);
spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp1);
@ -134,13 +149,6 @@ main(int argc, char** argv)
if (length_f1_after < length_f1_before) exit_code = 0; 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); spot::ltl::destroy(f1);
if (f2 != NULL) if (f2 != NULL)
spot::ltl::destroy(f2); spot::ltl::destroy(f2);

31
src/ltltest/reduc.test
View file

@ -23,30 +23,37 @@
# Check for the reduc visitor. # Check for the reduc visitor.
. ./defs || exit 1 #. ./defs || exit 1
set -e set -e
FICH=${1-$srcdir/formules.ltl} #FICH=${1-$srcdir/formules.ltl}
FICH=${1-formules.ltl}
##################################### #####################################
rm -f result.data for opt in 0 1 2 3
do
rm -f result.data
cat $FICH | cat $FICH |
while read f; do while read f; do
if [ -n "$f" ] && [ "$f" != "####" ]; then if [ -n "$f" ] && [ "$f" != "####" ]; then
./reduc "$f" >> result.data ./reduc $opt "$f" >> result.data
fi fi
done done
test $? == 0 || exit 1 test $? == 0 || exit 1
##################################### #####################################
perl -ne 'BEGIN { $sum1 = 0; $sum2 = 0; } perl -ne 'BEGIN { $sum1 = 0; $sum2 = 0; }
/^(\d+)\s+(\d+)/; /^(\d+)\s+(\d+)/;
$sum1 += $1; $sum1 += $1;
$sum2 += $2; $sum2 += $2;
END { print $sum2 * 100 / $sum1; print "\n"; } END { print 100 - ($sum2 * 100 / $sum1); print "\n"; }
' < result.data ' < result.data
done
#####################################

2
src/ltlvisit/Makefile.am
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.
## ##

148
src/ltlvisit/basereduc.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.
// //
@ -88,24 +88,24 @@ namespace spot
/* X(f1 & GF(f2)) = X(f1) & GF(F2) */ /* X(f1 & GF(f2)) = X(f1) & GF(F2) */
/* 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 (node_type(result_) == (node_type_form_visitor::Multop)) {
if (spot::ltl::nb_term_multop(result_) == 2) { if (dynamic_cast<multop*>(result_)->size() == 2) {
if (is_GF(((multop*)result_)->nth(0)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) { is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1)))); res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
f = result_; f = result_;
result_ = multop::instance(((multop*)(result_))->op(), res); result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
spot::ltl::destroy(f); spot::ltl::destroy(f);
return; return;
} }
if (is_GF(((multop*)result_)->nth(1)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) { is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0)))); res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
f = result_; f = result_;
result_ = multop::instance(((multop*)(result_))->op(), res); result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
spot::ltl::destroy(f); spot::ltl::destroy(f);
return; return;
} }
@ -124,33 +124,33 @@ namespace spot
/* FX(a) = XF(a) */ /* FX(a) = XF(a) */
if (node_type(result_) == (node_type_form_visitor::Unop)) if (node_type(result_) == (node_type_form_visitor::Unop))
if ( ((unop*)(result_))->op() == unop::X ){ if (dynamic_cast<unop*>(result_)->op() == unop::X){
f = result_; f = result_;
result_ = unop::instance(unop::X, result_ = unop::instance(unop::X,
unop::instance(unop::F, unop::instance(unop::F,
basic_reduce_form(((unop*)(result_))->child()) )); basic_reduce_form(dynamic_cast<unop*>(result_)->child()) ));
spot::ltl::destroy(f); spot::ltl::destroy(f);
return; return;
} }
/* F(f1 & GF(f2)) = F(f1) & GF(F2) */ /* F(f1 & GF(f2)) = F(f1) & GF(F2) */
if (node_type(result_) == (node_type_form_visitor::Multop)) { if (node_type(result_) == (node_type_form_visitor::Multop)) {
if ( ((multop*)(result_))->op() == multop::And ) { if (dynamic_cast<multop*>(result_)->op() == multop::And) {
if (spot::ltl::nb_term_multop(result_) == 2) { if (dynamic_cast<multop*>(result_)->size() == 2) {
if (is_GF(((multop*)result_)->nth(0)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) { is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1)))); res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
spot::ltl::destroy(result_); spot::ltl::destroy(result_);
result_ = multop::instance(multop::And, res); result_ = multop::instance(multop::And, res);
return; return;
} }
if (is_GF(((multop*)result_)->nth(1)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) { is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0)))); res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
spot::ltl::destroy(result_); spot::ltl::destroy(result_);
result_ = multop::instance(multop::And, res); result_ = multop::instance(multop::And, res);
return; return;
@ -171,42 +171,42 @@ namespace spot
/* G(a R b) = G(b) */ /* G(a R b) = G(b) */
if (node_type(result_) == node_type_form_visitor::Binop) if (node_type(result_) == node_type_form_visitor::Binop)
if ( ((binop*)(result_))->op() == binop::R ){ if (dynamic_cast<binop*>(result_)->op() == binop::R){
f = result_; f = result_;
result_ = unop::instance(unop::G, basic_reduce_form(((binop*)(result_))->second())); result_ = unop::instance(unop::G, basic_reduce_form(dynamic_cast<binop*>(result_)->second()));
spot::ltl::destroy(f); spot::ltl::destroy(f);
return; return;
} }
/* GX(a) = XG(a) */ /* GX(a) = XG(a) */
if (node_type(result_) == (node_type_form_visitor::Unop)) if (node_type(result_) == (node_type_form_visitor::Unop))
if ( ((unop*)(result_))->op() == unop::X ){ if ( dynamic_cast<unop*>(result_)->op() == unop::X ){
f = result_; f = result_;
result_ = unop::instance(unop::X, result_ = unop::instance(unop::X,
unop::instance(unop::G, unop::instance(unop::G,
basic_reduce_form(((unop*)(result_))->child()) )); basic_reduce_form(dynamic_cast<unop*>(result_)->child())));
spot::ltl::destroy(f); spot::ltl::destroy(f);
return; return;
} }
/* G(f1 | GF(f2)) = G(f1) | GF(F2) */ /* G(f1 | GF(f2)) = G(f1) | GF(F2) */
if (node_type(result_) == (node_type_form_visitor::Multop)) { if (node_type(result_) == (node_type_form_visitor::Multop)) {
if ( ((multop*)(f))->op() == multop::Or ) { if (dynamic_cast<multop*>(f)->op() == multop::Or) {
if (spot::ltl::nb_term_multop(result_) == 2) { if (dynamic_cast<multop*>(result_)->size() == 2) {
if (is_GF(((multop*)result_)->nth(0)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) { is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(1)))); res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
spot::ltl::destroy(result_); spot::ltl::destroy(result_);
result_ = multop::instance(multop::Or, res); result_ = multop::instance(multop::Or, res);
return; return;
} }
if (is_GF(((multop*)result_)->nth(1)) || if (is_GF(dynamic_cast<multop*>(result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) { is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(0)))); res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1))); res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
spot::ltl::destroy(result_); spot::ltl::destroy(result_);
result_ = multop::instance(multop::Or, res); result_ = multop::instance(multop::Or, res);
return; return;
@ -262,11 +262,11 @@ namespace spot
/* X(a) U X(b) = X(a U b) */ /* X(a) U X(b) = X(a U b) */
if ( node_type(f1) == (node_type_form_visitor::Unop) if ( node_type(f1) == (node_type_form_visitor::Unop)
&& node_type(f2) == (node_type_form_visitor::Unop)) { && node_type(f2) == (node_type_form_visitor::Unop)) {
if ( (((unop*)(f1))->op() == unop::X) if ((dynamic_cast<unop*>(f1)->op() == unop::X)
&& (((unop*)(f2))->op() == unop::X) ) { && (dynamic_cast<unop*>(f2)->op() == unop::X)) {
ftmp = binop::instance(binop::U, ftmp = binop::instance(binop::U,
basic_reduce_form(((unop*)(f1))->child()), basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
basic_reduce_form(((unop*)(f2))->child())); basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
spot::ltl::destroy(f2); spot::ltl::destroy(f2);
@ -290,13 +290,13 @@ namespace spot
f1 = basic_reduce_form(f1); f1 = basic_reduce_form(f1);
/* X(a) R X(b) = X(a R b) */ /* X(a) R X(b) = X(a R b) */
if ( node_type(f1) == (node_type_form_visitor::Unop) if (node_type(f1) == (node_type_form_visitor::Unop)
&& node_type(f2) == (node_type_form_visitor::Unop)) { && node_type(f2) == (node_type_form_visitor::Unop)) {
if ( (((unop*)(f1))->op() == unop::X) if ((dynamic_cast<unop*>(f1)->op() == unop::X)
&& (((unop*)(f2))->op() == unop::X) ) { && (dynamic_cast<unop*>(f2)->op() == unop::X)) {
ftmp = binop::instance(bo->op(), ftmp = binop::instance(bo->op(),
basic_reduce_form(((unop*)(f1))->child()), basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
basic_reduce_form(((unop*)(f2))->child())); basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
spot::ltl::destroy(f2); spot::ltl::destroy(f2);
@ -347,14 +347,14 @@ namespace spot
case node_type_form_visitor::Unop: case node_type_form_visitor::Unop:
/* Xa & Xb = X(a & b)*/ /* Xa & Xb = X(a & b)*/
if (((unop*)(*i))->op() == unop::X) { if (dynamic_cast<unop*>(*i)->op() == unop::X) {
tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) ); tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
break; break;
} }
/* FG(a) & FG(b) = FG(a & b)*/ /* FG(a) & FG(b) = FG(a & b)*/
if (is_FG(*i)) { 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<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
break; break;
} }
tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
@ -368,19 +368,19 @@ namespace spot
case node_type_form_visitor::Binop: case node_type_form_visitor::Binop:
/* (a U b) & (c U b) = (a & c) U b */ /* (a U b) & (c U b) = (a & c) U b */
if (((binop*)(*i))->op() == binop::U) { if (dynamic_cast<binop*>(*i)->op() == binop::U) {
ftmp = ((binop*)(*i))->second(); ftmp = dynamic_cast<binop*>(*i)->second();
tmpUright = new multop::vec; 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 (*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<binop*>(*j)->op() == binop::U)
{ {
if (ftmp == ((binop*)(*j))->second()) if (ftmp == dynamic_cast<binop*>(*j)->second())
{ {
tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() )); tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first() ));
if (j != i) { if (j != i) {
spot::ltl::destroy(*j); spot::ltl::destroy(*j);
*j = NULL; *j = NULL;
@ -396,19 +396,19 @@ namespace spot
} }
/* (a R b) & (a R c) = a R (b & c) */ /* (a R b) & (a R c) = a R (b & c) */
if (((binop*)(*i))->op() == binop::R) { if (dynamic_cast<binop*>(*i)->op() == binop::R) {
ftmp = ((binop*)(*i))->first(); ftmp = dynamic_cast<binop*>(*i)->first();
tmpRright = new multop::vec; 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 (*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<binop*>(*j)->op() == binop::R)
{ {
if (ftmp == ((binop*)(*j))->first()) if (ftmp == dynamic_cast<binop*>(*j)->first())
{ {
tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() )); tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second() ));
if (j != i) { if (j != i) {
spot::ltl::destroy(*j); spot::ltl::destroy(*j);
*j = NULL; *j = NULL;
@ -445,14 +445,14 @@ namespace spot
case node_type_form_visitor::Unop: case node_type_form_visitor::Unop:
/* Xa | Xb = X(a | b)*/ /* Xa | Xb = X(a | b)*/
if (((unop*)(*i))->op() == unop::X) { if (dynamic_cast<unop*>(*i)->op() == unop::X) {
tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) ); tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
break; break;
} }
/* GF(a) & GF(b) = GF(a & b)*/ /* GF(a) & GF(b) = GF(a & b)*/
if (is_GF(*i)) { 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<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
break; break;
} }
tmpOther->push_back(spot::ltl::basic_reduce_form(*i)); tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
@ -461,19 +461,19 @@ namespace spot
case node_type_form_visitor::Binop: case node_type_form_visitor::Binop:
/* (a U b) | (a U c) = a U (b | c) */ /* (a U b) | (a U c) = a U (b | c) */
if (((binop*)(*i))->op() == binop::U) { if (dynamic_cast<binop*>(*i)->op() == binop::U) {
ftmp = ((binop*)(*i))->first(); ftmp = dynamic_cast<binop*>(*i)->first();
tmpUright = new multop::vec; 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 (*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<binop*>(*j)->op() == binop::U)
{ {
if (ftmp == ((binop*)(*j))->first()) if (ftmp == dynamic_cast<binop*>(*j)->first())
{ {
tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() )); tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second()));
if (j != i) { if (j != i) {
spot::ltl::destroy(*j); spot::ltl::destroy(*j);
*j = NULL; *j = NULL;
@ -489,19 +489,19 @@ namespace spot
} }
/* (a R b) | (c R b) = (a | c) R b */ /* (a R b) | (c R b) = (a | c) R b */
if (((binop*)(*i))->op() == binop::R) { if (dynamic_cast<binop*>(*i)->op() == binop::R) {
ftmp = ((binop*)(*i))->second(); ftmp = dynamic_cast<binop*>(*i)->second();
tmpRright = new multop::vec; 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 (*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<binop*>(*j)->op() == binop::R)
{ {
if (ftmp == ((binop*)(*j))->second()) if (ftmp == dynamic_cast<binop*>(*j)->second())
{ {
tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() )); tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first()));
if (j != i) { if (j != i) {
spot::ltl::destroy(*j); spot::ltl::destroy(*j);
*j = NULL; *j = NULL;

143
src/ltlvisit/forminf.cc
View file

@ -35,10 +35,10 @@ namespace spot
bool bool
is_GF(const formula* f) is_GF(const formula* f)
{ {
if ((const unop*)f != NULL) if (node_type(f) == node_type_form_visitor::Unop)
if (((const unop*)f)->op() == unop::G) if (dynamic_cast<const unop*>(f)->op() == unop::G)
if ((const unop*)(((const unop*)f)->child()) != NULL) if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop)
if (((const unop*)((const unop*)f)->child())->op() == unop::F) if (dynamic_cast<const unop*>(dynamic_cast<const unop*>(f)->child())->op() == unop::F)
return true; return true;
return false; return false;
} }
@ -46,24 +46,14 @@ namespace spot
bool bool
is_FG(const formula* f) is_FG(const formula* f)
{ {
if ((const unop*)f != NULL) if (node_type(f) == node_type_form_visitor::Unop)
if (((const unop*)f)->op() == unop::F) if (dynamic_cast<const unop*>(f)->op() == unop::F)
if ((const unop*)(((const unop*)f)->child()) != NULL) if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop)
if (((const unop*)((const unop*)f)->child())->op() == unop::G) if (dynamic_cast<const unop*>(dynamic_cast<const unop*>(f)->child())->op() == unop::G)
return true; return true;
return false; 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::node_type_form_visitor(){}
node_type_form_visitor::type 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::type node_type(const formula* f)
{ {
node_type_form_visitor v; node_type_form_visitor v;
if (f == NULL) std::cout << "f == NULL !!!!!!!!" << std::endl; assert(f != NULL);
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.result(); return v.result();
} }
@ -113,7 +103,7 @@ namespace spot
form_eventual_universal_visitor() form_eventual_universal_visitor()
{ {
eventual = false; // faux au départ eventual = false;
universal = false; universal = false;
} }
@ -179,12 +169,12 @@ namespace spot
return; return;
case binop::U: case binop::U:
if (node_type(f1) == node_type_form_visitor::Const) if (node_type(f1) == node_type_form_visitor::Const)
if (((const constant*)f1)->val() == constant::True) if (dynamic_cast<const constant*>(f1)->val() == constant::True)
eventual = true; eventual = true;
return; return;
case binop::R: case binop::R:
if (node_type(f1) != node_type_form_visitor::Const) if (node_type(f1) == node_type_form_visitor::Const)
if (((const constant*)f1)->val() == constant::False) if (dynamic_cast<const constant*>(f1)->val() == constant::False)
universal = true; universal = true;
return; return;
} }
@ -201,13 +191,13 @@ namespace spot
eventual = true; eventual = true;
universal = true; universal = true;
for (unsigned i = 0; i < mos; ++i){ for (unsigned i = 0; i < mos; ++i){
if ( !(recurse_ev(mo->nth(i))) ){ if (!(recurse_ev(mo->nth(i)))){
eventual = false; eventual = false;
break; break;
} }
} }
for (unsigned i = 0; i < mos; ++i){ for (unsigned i = 0; i < mos; ++i){
if ( !(recurse_un(mo->nth(i))) ){ if (!(recurse_un(mo->nth(i)))){
universal = false; universal = false;
break; break;
} }
@ -259,25 +249,13 @@ namespace spot
inf_form_right_recurse_visitor(const formula *f) inf_form_right_recurse_visitor(const formula *f)
{ {
this->f = f; this->f = f;
result_ = false; // faux au départ result_ = false;
} }
virtual ~inf_form_right_recurse_visitor() 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 int
result() const result() const
{ {
@ -287,7 +265,7 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
if ((const atomic_prop*)f == ap) if (dynamic_cast<const atomic_prop*>(f) == ap)
result_ = true; result_ = true;
} }
@ -312,18 +290,24 @@ namespace spot
const formula* tmp = NULL; const formula* tmp = NULL;
switch (uo->op()) switch (uo->op())
{ {
case unop::Not:// à gérer !! case unop::Not:
if (uo == f)
result_ = true;
return; return;
case unop::X:// à gérer !! case unop::X:
if (node_type(f) == node_type_form_visitor::Unop)
if (dynamic_cast<const unop*>(f)->op() == unop::X) {
result_ = inf_form(dynamic_cast<const unop*>(f)->child(),f1);
}
return; return;
case unop::F: case unop::F:
// F(a) = true U a /* F(a) = true U a */
result_ = inf_form(f,f1); result_ = inf_form(f,f1);
return; return;
case unop::G: case unop::G:
// G(a) = false R a /* G(a) = false R a */
tmp = constant::false_instance(); tmp = constant::false_instance();
if ( inf_form(f,tmp) ) if (inf_form(f,tmp))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
@ -344,11 +328,11 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if ( (inf_form(f,f2)) ) if ((inf_form(f,f2)))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if ( (inf_form(f,f1)) && (inf_form(f,f2)) ) if ((inf_form(f,f1)) && (inf_form(f,f2)))
result_ = true; result_ = true;
return; return;
} }
@ -366,13 +350,13 @@ namespace spot
{ {
case multop::And: case multop::And:
for (unsigned i = 0; (i < mos) ; ++i) for (unsigned i = 0; (i < mos) ; ++i)
if ( !(inf_form(f,mo->nth(i))) ) if (!(inf_form(f,mo->nth(i))))
return; return;
result_ = true; result_ = true;
break; break;
case multop::Or: case multop::Or:
for (unsigned i = 0; i < mos && !result_; ++i) for (unsigned i = 0; i < mos && !result_; ++i)
if ( (inf_form(f,mo->nth(i))) ) if ((inf_form(f,mo->nth(i))))
result_ = true; result_ = true;
break; break;
} }
@ -388,7 +372,7 @@ namespace spot
} }
protected: protected:
bool result_; // true si f < f1, false sinon. bool result_; /* true if f < f1, false otherwise. */
const formula* f; const formula* f;
}; };
@ -412,14 +396,23 @@ namespace spot
{ {
if ((node_type(f) == node_type_form_visitor::Binop) if ((node_type(f) == node_type_form_visitor::Binop)
&& (node_type(f2) == node_type_form_visitor::Binop)) && (node_type(f2) == node_type_form_visitor::Binop))
if (((const binop*)f)->op() == ((const binop*)f2)->op()) if (dynamic_cast<const binop*>(f)->op() == dynamic_cast<const binop*>(f2)->op())
if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first()) if (inf_form(dynamic_cast<const binop*>(f2)->first(),dynamic_cast<const binop*>(f)->first())
&& inf_form(((const binop*)f2)->second(), && inf_form(dynamic_cast<const binop*>(f2)->second(),dynamic_cast<const binop*>(f)->second()))
((const binop*)f)->second()))
return true; return true;
return false; return false;
} }
bool nodeX()
{
/*
if (node_type(f) == node_type_form_visitor::Unop)
if (dynamic_cast<const unop*>(f)->op() == unop::X)
return true;
*/
return false;
}
int int
result() const result() const
{ {
@ -429,6 +422,7 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
if (this->nodeX()) return;
inf_form_right_recurse_visitor v(ap); inf_form_right_recurse_visitor v(ap);
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
result_ = v.result(); result_ = v.result();
@ -437,6 +431,7 @@ namespace spot
void void
visit(const constant* c) visit(const constant* c)
{ {
if (this->nodeX()) return;
inf_form_right_recurse_visitor v(c); inf_form_right_recurse_visitor v(c);
switch (c->val()) switch (c->val())
{ {
@ -466,32 +461,34 @@ namespace spot
return; return;
case unop::X: case unop::X:
if (node_type(f) == node_type_form_visitor::Unop) if (node_type(f) == node_type_form_visitor::Unop)
if (((const unop*)f)->op() == unop::X) { if (dynamic_cast<const unop*>(f)->op() == unop::X) {
result_ = inf_form(f1,((const unop*)f)->child()); result_ = inf_form(f1,dynamic_cast<const unop*>(f)->child());
} }
return; return;
case unop::F: 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)); tmp = binop::instance(binop::U,constant::true_instance(),clone(f1));
if (this->special_case(tmp)){ if (this->special_case(tmp)){
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
} }
if ( inf_form(tmp,f) ) if (inf_form(tmp,f))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
case unop::G: case unop::G:
// F(a) = false R a if (this->nodeX()) return;
/* F(a) = false R a */
tmp = binop::instance(binop::R, tmp = binop::instance(binop::R,
constant::false_instance(), clone(f1)); constant::false_instance(),clone(f1));
if (this->special_case(tmp)){ if (this->special_case(tmp)){
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
} }
if ( inf_form(f1,f) ) if (inf_form(f1,f))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
@ -503,6 +500,7 @@ namespace spot
void void
visit(const binop* bo) visit(const binop* bo)
{ {
if (this->nodeX()) return;
if (this->special_case(bo)) if (this->special_case(bo))
{ {
@ -519,11 +517,11 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if ( (inf_form(f1,f)) && (inf_form(f2,f)) ) if ((inf_form(f1,f)) && (inf_form(f2,f)))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if ( (inf_form(f2,f)) ) if ((inf_form(f2,f)))
result_ = true; result_ = true;
return; return;
} }
@ -534,19 +532,20 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
if (mo == NULL); if (this->nodeX()) return;
multop::type op = mo->op(); multop::type op = mo->op();
unsigned mos = mo->size(); unsigned mos = mo->size();
switch (op) switch (op)
{ {
case multop::And: case multop::And:
for (unsigned i = 0; (i < mos) && !result_ ; ++i) for (unsigned i = 0; (i < mos) && !result_ ; ++i)
if ( (inf_form(mo->nth(i),f)) ) if ((inf_form(mo->nth(i),f)))
result_ = true; result_ = true;
break; break;
case multop::Or: case multop::Or:
for (unsigned i = 0; i < mos ; ++i) for (unsigned i = 0; i < mos ; ++i)
if ( !(inf_form(mo->nth(i),f)) ) if (!(inf_form(mo->nth(i),f)))
return; return;
result_ = true; result_ = true;
break; break;
@ -554,21 +553,21 @@ namespace spot
} }
protected: protected:
bool result_; // true if f1 < f, 1 otherwise. bool result_; /* true if f1 < f, 1 otherwise. */
const formula* f; const formula* f;
}; };
bool inf_form(const formula* f1, const formula* f2) bool inf_form(const formula* f1, const formula* f2)
{ {
// f1 and f2 are unabbreviate /* f1 and f2 are unabbreviate */
if (f1 == f2) return true; if (f1 == f2) return true;
inf_form_left_recurse_visitor v1(f2); inf_form_left_recurse_visitor v1(f2);
inf_form_right_recurse_visitor v2(f1); inf_form_right_recurse_visitor v2(f1);
if ( (node_type(f1) == node_type_form_visitor::Const) && if ((node_type(f1) == node_type_form_visitor::Const) &&
(node_type(f2) == node_type_form_visitor::Const) ) (node_type(f2) == node_type_form_visitor::Const))
if ( (((const constant*)f2)->val() == constant::True) || if ((dynamic_cast<const constant*>(f2)->val() == constant::True) ||
(((const constant*)f1)->val() == constant::False) ) (dynamic_cast<const constant*>(f1)->val() == constant::False))
{ {
return true; return true;
} }

370
src/ltlvisit/reducform.cc
View file

@ -32,19 +32,13 @@ namespace spot
namespace ltl namespace ltl
{ {
//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(option o)
{ {
/* this->o = o;
eventuality_ = false;
universality_ = false;
*/
} }
virtual ~reduce_form_visitor() virtual ~reduce_form_visitor()
@ -57,20 +51,6 @@ namespace spot
return result_; return result_;
} }
/*
bool
is_eventuality()
{
return eventuality_;
}
bool
is_universality()
{
return universality_;
}
*/
void void
visit(atomic_prop* ap) visit(atomic_prop* ap)
{ {
@ -111,14 +91,14 @@ namespace spot
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_) || (o == Inf)) {
result_ = unop::instance(unop::F, result_); result_ = unop::instance(unop::F, result_);
} }
return; return;
case unop::G: case unop::G:
/* if f is class of universality then G(f)=f */ /* 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_); result_ = unop::instance(unop::G, result_);
} }
return; return;
@ -134,86 +114,85 @@ namespace spot
/* 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 (o != Inf) {
( is_universal(f2) && ( (bo->op()) == binop::R )) ) if ((is_eventual(f2) && ((bo->op()) == binop::U)) ||
{ (is_universal(f2) && ((bo->op()) == binop::R)))
result_ = f2; {
return; result_ = f2;
} return;
}
}
/* case of implies */ /* case of implies */
formula* f1 = recurse(bo->first()); 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()) if (o != EventualUniversal) {
{ bool inf = inf_form(f1,f2);
case binop::Xor: bool infinv = inf_form(f2,f1);
case binop::Equiv: bool infnegleft = infneg_form(f2,f1,0);
case binop::Implies: bool infnegright = infneg_form(f2,f1,1);
result_ = binop::instance(bo->op(), f1, f2);
return;
case binop::U: switch (bo->op())
/* a < b => a U b = b */ {
if (inf) case binop::Xor:
{ case binop::Equiv:
result_ = f2; case binop::Implies:
spot::ltl::destroy(f1); break;;
return;
} case binop::U:
/* !b < a => a U b = Fb */ /* a < b => a U b = b */
if (infnegleft) if (inf)
{ {
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())){
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
return; return;
} }
result_ = binop::instance(binop::U, /* !b < a => a U b = Fb */
f1, f2); if (infnegleft)
return; {
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<binop*>(f2)->op() == binop::U)
if (inf_form(f1,dynamic_cast<binop*>(f2)->first()))
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
break;
case binop::R: case binop::R:
/* b < a => a R b = b */ /* b < a => a R b = b */
if (infinv) 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)){
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
return; 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<binop*>(f2)->op() == binop::R)
if (inf_form(dynamic_cast<binop*>(f2)->first(),f1))
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
break;
result_ = binop::instance(binop::R, }
f1, f2); }
return; result_ = binop::instance(bo->op(), f1, f2);
}
/* Unreachable code. */
assert(0);
} }
void void
@ -229,109 +208,86 @@ namespace spot
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)));
switch (mo->op()) if (o != EventualUniversal){
{ switch (mo->op())
{
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++;
}
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);
} }
if (mo->op() == multop::Or) for (; index != res->end();index++)
result_ = constant::true_instance(); {
else f2 = *index;
result_ = constant::false_instance(); /* a < b => a + b = b */
return; 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:
if ((constant*)(*index) != NULL) index = indextmp = res->begin();
if (((((constant*)(*index))->val() == constant::True) && if (mos)
(mo->op() == multop::Or)) || {
(((((constant*)(*index))->val() == constant::False)) f1 = mo->nth(0);
&& (mo->op() == multop::And)) index++;
) { }
//std::cout << "constant" << std::endl; for (; index != res->end(); index++)
for (multop::vec::iterator j = res->begin(); j != res->end(); j++){ {
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); spot::ltl::destroy(*j);
} }
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;
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;
@ -342,36 +298,41 @@ namespace spot
formula* formula*
recurse(formula* f) recurse(formula* f)
{ {
return reduce_form(f); return reduce_form(f,o);
} }
protected: protected:
formula* result_; formula* result_;
/* option o;
bool eventuality_;
bool universality_;
*/
}; };
formula* formula*
reduce_form(const formula* f) reduce_form(const formula* f, option o)
{ {
spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp1 = NULL;
spot::ltl::formula* ftmp2; spot::ltl::formula* ftmp2 = NULL;
reduce_form_visitor v; reduce_form_visitor v(o);
ftmp1 = spot::ltl::basic_reduce_form(f); if (o == BRI) {
const_cast<formula*>(ftmp1)->accept(v); ftmp1 = spot::ltl::basic_reduce_form(f);
ftmp2 = spot::ltl::basic_reduce_form(v.result()); const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(v.result());
spot::ltl::destroy(ftmp1); return ftmp2;
spot::ltl::destroy(v.result()); }
else {
const_cast<formula*>(f)->accept(v);
return v.result();
}
return ftmp2; /* unreachable code */
assert(0);
} }
formula* formula*
reduce(const formula* f) reduce(const formula* f, option o)
{ {
spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp1;
spot::ltl::formula* ftmp2; spot::ltl::formula* ftmp2;
@ -379,14 +340,27 @@ namespace spot
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);
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(ftmp1);
spot::ltl::destroy(ftmp2); spot::ltl::destroy(ftmp2);
return ftmp3; return ftmp3;
} }
} }
} }

49
src/ltlvisit/reducform.hh
View file

@ -25,38 +25,48 @@
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
#include "ltlast/visitor.hh" #include "ltlast/visitor.hh"
// For debog // For debug
#include "ltlvisit/dump.hh" #include "ltlvisit/dump.hh"
namespace spot namespace spot
{ {
namespace ltl 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* basic_reduce_form(const formula* f);
/* formula rewriting using univerality, eventuality, /// Use by spot::ltl::reduce
implies and basic_reduce_form */ /// Implement rewritings rules using implies relation,
formula* reduce_form(const formula* f); /// 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); 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);
/* detect if a formula is of form GF or FG */ /// For test.
bool is_GF(const formula* f); int form_length(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 +82,11 @@ 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 */ /// detect if a formula is of form GF or FG.
int nb_term_multop(const formula* f); bool is_GF(const formula* f);
formula* reduce_inf_form(const formula* f); /* Obsolete */ bool is_FG(const formula* f);
int form_length(const formula* f); /* For test */
} }
} }