* src/ltlvisit/basereduc.cc (spot): 80 columns.
* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc, src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh, src/tgbatest/ltl2tgba.cc (main): More option. * src/ltltest/inf.test: More test.
This commit is contained in:
martinez
parent
41589e2818
commit
788ed772c2
8 changed files with 458 additions and 349 deletions
|
|
@ -1,3 +1,11 @@
|
||||||
|
2004-05-17 Thomas Martinez <martinez@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/ltlvisit/basereduc.cc (spot): 80 columns.
|
||||||
|
* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
|
||||||
|
src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,
|
||||||
|
src/tgbatest/ltl2tgba.cc (main): More option.
|
||||||
|
* src/ltltest/inf.test: More test.
|
||||||
|
|
||||||
2004-05-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-05-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
* wrap/python/buddy.i: Define typemap for input_buf and use it
|
* wrap/python/buddy.i: Define typemap for input_buf and use it
|
||||||
|
|
|
||||||
|
|
@ -41,21 +41,22 @@ syntax(char* prog)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
if (argc < 3)
|
if (argc < 4)
|
||||||
syntax(argv[0]);
|
syntax(argv[0]);
|
||||||
|
|
||||||
|
int opt = atoi(argv[1]);
|
||||||
|
|
||||||
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;
|
||||||
|
|
||||||
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;
|
||||||
|
|
||||||
std::string f1s = spot::ltl::to_string(f1);
|
std::string f1s = spot::ltl::to_string(f1);
|
||||||
|
|
@ -63,28 +64,36 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
int exit_return = 0;
|
int exit_return = 0;
|
||||||
|
|
||||||
std::cout << "Test f1 < f2" << std::endl;
|
switch (opt)
|
||||||
if (spot::ltl::inf_form(f1, f2))
|
|
||||||
{
|
{
|
||||||
std::cout << f1s << " < " << f2s << std::endl;
|
case 0:
|
||||||
exit_return = 1;
|
std::cout << "Test f1 < f2" << std::endl;
|
||||||
}
|
if (spot::ltl::inf_form(f1, f2))
|
||||||
|
{
|
||||||
|
std::cout << f1s << " < " << f2s << std::endl;
|
||||||
|
exit_return = 1;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
|
||||||
/*
|
case 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 = 1;
|
||||||
}
|
}
|
||||||
|
break;
|
||||||
|
|
||||||
std::cout << "Test f1 < !f2" << std::endl;
|
case 2:
|
||||||
if (spot::ltl::infneg_form(f1, f2, 1))
|
std::cout << "Test f1 < !f2" << std::endl;
|
||||||
{
|
if (spot::ltl::infneg_form(f1, f2, 1))
|
||||||
std::cout << f1s << " < !(" << f2s << ")" << std::endl;
|
{
|
||||||
exit_return = 3;
|
std::cout << f1s << " < !(" << f2s << ")" << std::endl;
|
||||||
|
exit_return = 1;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
default: break;
|
||||||
}
|
}
|
||||||
*/
|
|
||||||
|
|
||||||
spot::ltl::dump(std::cout, f1); std::cout << std::endl;
|
spot::ltl::dump(std::cout, f1); std::cout << std::endl;
|
||||||
spot::ltl::dump(std::cout, f2); std::cout << std::endl;
|
spot::ltl::dump(std::cout, f2); std::cout << std::endl;
|
||||||
|
|
|
||||||
|
|
@ -26,67 +26,67 @@
|
||||||
. ./defs || exit 1
|
. ./defs || exit 1
|
||||||
|
|
||||||
#
|
#
|
||||||
run 1 ./inf 'Xa' 'X(b U a)'
|
run 1 ./inf 0 'Xa' 'X(b U a)'
|
||||||
run 1 ./inf 'XXa' 'XX(b U a)'
|
run 1 ./inf 0 'XXa' 'XX(b U a)'
|
||||||
|
|
||||||
run 1 ./inf '(e R f)' '(g U f)'
|
run 1 ./inf 0 '(e R f)' '(g U f)'
|
||||||
run 1 ./inf '( X(a + b))' '( X((a + b)+(c)+(d)))'
|
run 1 ./inf 0 '( 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 1 ./inf 0 '( 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 0 'Xa' 'XX(b U a)'
|
||||||
run 0 ./inf 'XXa' 'X(b U a)'
|
run 0 ./inf 0 'XXa' 'X(b U a)'
|
||||||
|
|
||||||
run 0 ./inf '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
|
run 0 ./inf 0 '( 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 0 '( 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 0 'a' 'b'
|
||||||
run 0 ./inf 'a' 'b + c'
|
run 0 ./inf 0 'a' 'b + c'
|
||||||
run 0 ./inf 'a + b' 'a'
|
run 0 ./inf 0 'a + b' 'a'
|
||||||
run 0 ./inf 'a' 'a * c'
|
run 0 ./inf 0 'a' 'a * c'
|
||||||
run 0 ./inf 'a * b' 'c'
|
run 0 ./inf 0 'a * b' 'c'
|
||||||
run 0 ./inf 'a' 'a U b'
|
run 0 ./inf 0 'a' 'a U b'
|
||||||
run 0 ./inf 'a' 'a R b'
|
run 0 ./inf 0 'a' 'a R b'
|
||||||
run 0 ./inf 'a R b' 'a'
|
run 0 ./inf 0 'a R b' 'a'
|
||||||
|
|
||||||
run 1 ./inf '1' '1'
|
run 1 ./inf 0 '1' '1'
|
||||||
run 1 ./inf '0' '0'
|
run 1 ./inf 0 '0' '0'
|
||||||
|
|
||||||
run 1 ./inf 'a' '1'
|
run 1 ./inf 0 'a' '1'
|
||||||
run 1 ./inf 'a' 'a'
|
run 1 ./inf 0 'a' 'a'
|
||||||
|
|
||||||
run 1 ./inf 'a' 'a * 1'
|
run 1 ./inf 0 'a' 'a * 1'
|
||||||
|
|
||||||
run 1 ./inf 'a * b' 'b'
|
run 1 ./inf 0 'a * b' 'b'
|
||||||
run 1 ./inf 'a * b' 'a'
|
run 1 ./inf 0 'a * b' 'a'
|
||||||
|
|
||||||
run 1 ./inf 'a' 'a + b'
|
run 1 ./inf 0 'a' 'a + b'
|
||||||
run 1 ./inf 'b' 'a + b'
|
run 1 ./inf 0 'b' 'a + b'
|
||||||
|
|
||||||
run 1 ./inf 'a + b' '1'
|
run 1 ./inf 0 'a + b' '1'
|
||||||
|
|
||||||
run 1 ./inf 'a' 'b U a'
|
run 1 ./inf 0 'a' 'b U a'
|
||||||
run 1 ./inf 'a' 'b U 1'
|
run 1 ./inf 0 'a' 'b U 1'
|
||||||
run 1 ./inf 'a U b' '1'
|
run 1 ./inf 0 'a U b' '1'
|
||||||
|
|
||||||
run 1 ./inf 'a' '1 R a'
|
run 1 ./inf 0 'a' '1 R a'
|
||||||
run 1 ./inf 'a' 'a R 1'
|
run 1 ./inf 0 'a' 'a R 1'
|
||||||
run 1 ./inf 'a R b' 'b'
|
run 1 ./inf 0 'a R b' 'b'
|
||||||
run 1 ./inf 'a R b' '1'
|
run 1 ./inf 0 'a R b' '1'
|
||||||
|
|
||||||
run 1 ./inf 'Xa' 'X(b U a)'
|
run 1 ./inf 0 'Xa' 'X(b U a)'
|
||||||
run 1 ./inf 'X(a R b)' 'Xb'
|
run 1 ./inf 0 'X(a R b)' 'Xb'
|
||||||
|
|
||||||
run 1 ./inf 'a U b' '1 U b'
|
run 1 ./inf 0 'a U b' '1 U b'
|
||||||
run 1 ./inf 'a R b' '1 R b'
|
run 1 ./inf 0 'a R b' '1 R b'
|
||||||
|
|
||||||
run 1 ./inf 'b * (a U b)' 'a U b'
|
run 1 ./inf 0 'b * (a U b)' 'a U b'
|
||||||
run 1 ./inf 'a U b' 'c + (a U b)'
|
run 1 ./inf 0 'a U b' 'c + (a U b)'
|
||||||
|
|
||||||
exit 0
|
exit 0
|
||||||
#
|
#
|
||||||
|
|
||||||
#run 1 ./inf '(a U b) U ((a U b) U (a U b))' 'a U b'
|
#run 1 ./inf 0 '(a U b) U ((a U b) U (a U b))' 'a U b'
|
||||||
#run 1 ./inf '(a U b) && (a U b)' 'a U b'
|
#run 1 ./inf 0 '(a U b) && (a U b)' 'a U b'
|
||||||
|
|
||||||
'X1' '1'
|
'X1' '1'
|
||||||
'a U 0' '0'
|
'a U 0' '0'
|
||||||
|
|
|
||||||
|
|
@ -59,6 +59,15 @@ main(int argc, char** argv)
|
||||||
case 3:
|
case 3:
|
||||||
o = spot::ltl::BRI;
|
o = spot::ltl::BRI;
|
||||||
break;
|
break;
|
||||||
|
case 4:
|
||||||
|
o = spot::ltl::InfBase;
|
||||||
|
break;
|
||||||
|
case 5:
|
||||||
|
o = spot::ltl::EventualUniversalBase;
|
||||||
|
break;
|
||||||
|
case 6:
|
||||||
|
o = spot::ltl::InfEventualUniversal;
|
||||||
|
break;
|
||||||
default:
|
default:
|
||||||
return 2;
|
return 2;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -70,6 +70,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula* f = uo->child();
|
formula* f = uo->child();
|
||||||
result_ = basic_reduce_form(f);
|
result_ = basic_reduce_form(f);
|
||||||
|
multop* mo = NULL;
|
||||||
|
unop* u = NULL;
|
||||||
|
binop* bo = NULL;
|
||||||
switch (uo->op())
|
switch (uo->op())
|
||||||
{
|
{
|
||||||
case unop::Not:
|
case unop::Not:
|
||||||
|
|
@ -87,30 +90,31 @@ 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)) {
|
mo = dynamic_cast<multop*>(result_);
|
||||||
if (dynamic_cast<multop*>(result_)->size() == 2) {
|
if (mo && mo->size() == 2)
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
|
{
|
||||||
//|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
|
if (is_GF(mo->nth(0)))
|
||||||
|
{
|
||||||
multop::vec* res = new multop::vec;
|
multop::vec* res = new multop::vec;
|
||||||
res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
|
res->push_back(unop::instance(unop::F,
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
|
basic_reduce_form(mo->nth(1))));
|
||||||
f = result_;
|
res->push_back(basic_reduce_form(mo->nth(0)));
|
||||||
result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
|
result_ = multop::instance(mo->op(), res);
|
||||||
spot::ltl::destroy(f);
|
spot::ltl::destroy(mo);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
|
if (is_GF(mo->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(dynamic_cast<multop*>(result_)->nth(0))));
|
res->push_back(unop::instance(unop::F,
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
|
basic_reduce_form(mo->nth(0))));
|
||||||
f = result_;
|
res->push_back(basic_reduce_form(mo->nth(1)));
|
||||||
result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
|
result_ = multop::instance(mo->op(), res);
|
||||||
spot::ltl::destroy(f);
|
spot::ltl::destroy(mo);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
result_ = unop::instance(unop::X, result_);
|
result_ = unop::instance(unop::X, result_);
|
||||||
return;
|
return;
|
||||||
|
|
@ -123,41 +127,46 @@ namespace spot
|
||||||
return;
|
return;
|
||||||
|
|
||||||
/* FX(a) = XF(a) */
|
/* FX(a) = XF(a) */
|
||||||
if (node_type(result_) == (node_type_form_visitor::Unop))
|
u = dynamic_cast<unop*>(result_);
|
||||||
if (dynamic_cast<unop*>(result_)->op() == unop::X){
|
if (u && u->op() == unop::X)
|
||||||
f = result_;
|
{
|
||||||
result_ = unop::instance(unop::X,
|
result_ =
|
||||||
unop::instance(unop::F,
|
unop::instance(unop::X,
|
||||||
basic_reduce_form(dynamic_cast<unop*>(result_)->child()) ));
|
unop::instance(unop::F,
|
||||||
spot::ltl::destroy(f);
|
basic_reduce_form(u->child())));
|
||||||
return;
|
spot::ltl::destroy(u);
|
||||||
}
|
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)) {
|
mo = dynamic_cast<multop*>(result_);
|
||||||
if (dynamic_cast<multop*>(result_)->op() == multop::And) {
|
if (mo && mo->op() == multop::And)
|
||||||
if (dynamic_cast<multop*>(result_)->size() == 2) {
|
{
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
|
if (mo->size() == 2)
|
||||||
//|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
|
{
|
||||||
multop::vec* res = new multop::vec;
|
if (is_GF(mo->nth(0)))
|
||||||
res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
|
{
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
|
multop::vec* res = new multop::vec;
|
||||||
spot::ltl::destroy(result_);
|
res->push_back(unop::instance(unop::F,
|
||||||
result_ = multop::instance(multop::And, res);
|
basic_reduce_form(mo->nth(1))));
|
||||||
return;
|
res->push_back(basic_reduce_form(mo->nth(0)));
|
||||||
|
result_ = multop::instance(mo->op(), res);
|
||||||
|
spot::ltl::destroy(mo);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
if (is_GF(mo->nth(1)))
|
||||||
|
{
|
||||||
|
multop::vec* res = new multop::vec;
|
||||||
|
res->push_back(unop::instance(unop::F,
|
||||||
|
basic_reduce_form(mo->nth(0))));
|
||||||
|
res->push_back(basic_reduce_form(mo->nth(1)));
|
||||||
|
result_ = multop::instance(mo->op(), res);
|
||||||
|
spot::ltl::destroy(mo);
|
||||||
|
return;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
|
|
||||||
//|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
|
|
||||||
multop::vec* res = new multop::vec;
|
|
||||||
res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
|
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
|
|
||||||
spot::ltl::destroy(result_);
|
|
||||||
result_ = multop::instance(multop::And, res);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
result_ = unop::instance(unop::F, result_);
|
result_ = unop::instance(unop::F, result_);
|
||||||
return;
|
return;
|
||||||
|
|
@ -170,50 +179,56 @@ namespace spot
|
||||||
return;
|
return;
|
||||||
|
|
||||||
/* G(a R b) = G(b) */
|
/* G(a R b) = G(b) */
|
||||||
if (node_type(result_) == node_type_form_visitor::Binop)
|
bo = dynamic_cast<binop*>(result_);
|
||||||
if (dynamic_cast<binop*>(result_)->op() == binop::R){
|
if (bo && bo->op() == binop::R)
|
||||||
f = result_;
|
{
|
||||||
result_ = unop::instance(unop::G, basic_reduce_form(dynamic_cast<binop*>(result_)->second()));
|
result_ = unop::instance(unop::G,
|
||||||
spot::ltl::destroy(f);
|
basic_reduce_form(bo->second()));
|
||||||
|
spot::ltl::destroy(bo);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
/* GX(a) = XG(a) */
|
/* GX(a) = XG(a) */
|
||||||
if (node_type(result_) == (node_type_form_visitor::Unop))
|
u = dynamic_cast<unop*>(result_);
|
||||||
if ( dynamic_cast<unop*>(result_)->op() == unop::X ){
|
if (u && u->op() == unop::X)
|
||||||
f = result_;
|
{
|
||||||
result_ = unop::instance(unop::X,
|
result_ =
|
||||||
unop::instance(unop::G,
|
unop::instance(unop::X,
|
||||||
basic_reduce_form(dynamic_cast<unop*>(result_)->child())));
|
unop::instance(unop::G,
|
||||||
spot::ltl::destroy(f);
|
basic_reduce_form(u->child())));
|
||||||
|
spot::ltl::destroy(u);
|
||||||
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)) {
|
mo = dynamic_cast<multop*>(result_);
|
||||||
if (dynamic_cast<multop*>(f)->op() == multop::Or) {
|
if (mo && mo->op() == multop::Or)
|
||||||
if (dynamic_cast<multop*>(result_)->size() == 2) {
|
{
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
|
if (mo->size() == 2)
|
||||||
//|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
|
{
|
||||||
multop::vec* res = new multop::vec;
|
if (is_GF(mo->nth(0)))
|
||||||
res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
|
{
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
|
multop::vec* res = new multop::vec;
|
||||||
spot::ltl::destroy(result_);
|
res->push_back(unop::instance(unop::F,
|
||||||
result_ = multop::instance(multop::Or, res);
|
basic_reduce_form(mo->nth(1))));
|
||||||
return;
|
res->push_back(basic_reduce_form(mo->nth(0)));
|
||||||
|
result_ = multop::instance(mo->op(), res);
|
||||||
|
spot::ltl::destroy(mo);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
if (is_GF(mo->nth(1)))
|
||||||
|
{
|
||||||
|
multop::vec* res = new multop::vec;
|
||||||
|
res->push_back(unop::instance(unop::F,
|
||||||
|
basic_reduce_form(mo->nth(0))));
|
||||||
|
res->push_back(basic_reduce_form(mo->nth(1)));
|
||||||
|
result_ = multop::instance(mo->op(), res);
|
||||||
|
spot::ltl::destroy(mo);
|
||||||
|
return;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
|
|
||||||
//|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
|
|
||||||
multop::vec* res = new multop::vec;
|
|
||||||
res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
|
|
||||||
res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
|
|
||||||
spot::ltl::destroy(result_);
|
|
||||||
result_ = multop::instance(multop::Or, res);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
result_ = unop::instance(unop::G, result_);
|
result_ = unop::instance(unop::G, result_);
|
||||||
return;
|
return;
|
||||||
|
|
@ -230,6 +245,8 @@ namespace spot
|
||||||
formula* ftmp = NULL;
|
formula* ftmp = NULL;
|
||||||
node_type_form_visitor v1;
|
node_type_form_visitor v1;
|
||||||
node_type_form_visitor v2;
|
node_type_form_visitor v2;
|
||||||
|
unop* fu1 = NULL;
|
||||||
|
unop* fu2 = NULL;
|
||||||
switch (bo->op())
|
switch (bo->op())
|
||||||
{
|
{
|
||||||
case binop::Xor:
|
case binop::Xor:
|
||||||
|
|
@ -252,28 +269,31 @@ namespace spot
|
||||||
|
|
||||||
/* a U false = false
|
/* a U false = false
|
||||||
a U true = true */
|
a U true = true */
|
||||||
if (node_type(f2) == (node_type_form_visitor::Const)) {
|
if (node_type(f2) == (node_type_form_visitor::Const))
|
||||||
result_ = f2;
|
{
|
||||||
return;
|
result_ = f2;
|
||||||
}
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
f1 = basic_reduce_form(f1);
|
f1 = basic_reduce_form(f1);
|
||||||
|
|
||||||
/* 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)
|
fu1 = dynamic_cast<unop*>(f1);
|
||||||
&& node_type(f2) == (node_type_form_visitor::Unop)) {
|
fu2 = dynamic_cast<unop*>(f2);
|
||||||
if ((dynamic_cast<unop*>(f1)->op() == unop::X)
|
if ((fu1 && fu2) &&
|
||||||
&& (dynamic_cast<unop*>(f2)->op() == unop::X)) {
|
(fu1->op() == unop::X) &&
|
||||||
|
(fu2->op() == unop::X))
|
||||||
|
{
|
||||||
ftmp = binop::instance(binop::U,
|
ftmp = binop::instance(binop::U,
|
||||||
basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
|
basic_reduce_form(fu1->child()),
|
||||||
basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
|
basic_reduce_form(fu2->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);
|
||||||
spot::ltl::destroy(ftmp);
|
spot::ltl::destroy(ftmp);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
}
|
|
||||||
result_ = binop::instance(binop::U, f1, f2);
|
result_ = binop::instance(binop::U, f1, f2);
|
||||||
return;
|
return;
|
||||||
|
|
||||||
|
|
@ -282,28 +302,31 @@ namespace spot
|
||||||
|
|
||||||
/* a R false = false
|
/* a R false = false
|
||||||
a R true = true */
|
a R true = true */
|
||||||
if (node_type(f2) == (node_type_form_visitor::Const)) {
|
if (node_type(f2) == (node_type_form_visitor::Const))
|
||||||
result_ = f2;
|
{
|
||||||
return;
|
result_ = f2;
|
||||||
}
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
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)
|
fu1 = dynamic_cast<unop*>(f1);
|
||||||
&& node_type(f2) == (node_type_form_visitor::Unop)) {
|
fu2 = dynamic_cast<unop*>(f2);
|
||||||
if ((dynamic_cast<unop*>(f1)->op() == unop::X)
|
if ((fu1 && fu2) &&
|
||||||
&& (dynamic_cast<unop*>(f2)->op() == unop::X)) {
|
(fu1->op() == unop::X) &&
|
||||||
|
(fu2->op() == unop::X))
|
||||||
|
{
|
||||||
ftmp = binop::instance(bo->op(),
|
ftmp = binop::instance(bo->op(),
|
||||||
basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
|
basic_reduce_form(fu1->child()),
|
||||||
basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
|
basic_reduce_form(fu2->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);
|
||||||
spot::ltl::destroy(ftmp);
|
spot::ltl::destroy(ftmp);
|
||||||
return;
|
return;
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
result_ = binop::instance(bo->op(),
|
result_ = binop::instance(bo->op(),
|
||||||
f1, f2);
|
f1, f2);
|
||||||
return;
|
return;
|
||||||
|
|
@ -330,6 +353,9 @@ namespace spot
|
||||||
|
|
||||||
multop::vec* tmpOther = new multop::vec;
|
multop::vec* tmpOther = new multop::vec;
|
||||||
|
|
||||||
|
unop* uo = NULL;
|
||||||
|
unop* uo2 = NULL;
|
||||||
|
binop* bo = NULL;
|
||||||
formula* ftmp = NULL;
|
formula* ftmp = NULL;
|
||||||
|
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
for (unsigned i = 0; i < mos; ++i)
|
||||||
|
|
@ -340,96 +366,107 @@ namespace spot
|
||||||
{
|
{
|
||||||
case multop::And:
|
case multop::And:
|
||||||
|
|
||||||
for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
|
for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
|
||||||
if (*i == NULL) continue;
|
{
|
||||||
switch (node_type(*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)*/
|
/* Xa & Xb = X(a & b)*/
|
||||||
if (dynamic_cast<unop*>(*i)->op() == unop::X) {
|
uo = dynamic_cast<unop*>(*i);
|
||||||
tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
|
if (uo && uo->op() == unop::X)
|
||||||
break;
|
{
|
||||||
}
|
tmpX->push_back(basic_reduce_form(uo->child()));
|
||||||
|
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(dynamic_cast<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
|
{
|
||||||
break;
|
uo2 = dynamic_cast<unop*>(uo->child());
|
||||||
}
|
tmpFG->push_back(basic_reduce_form(uo2->child()));
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
break;
|
||||||
break;
|
}
|
||||||
/* A GERER !!!!!!!!!!!!!!!!!!!!!!!
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
case node_type_form_visitor::Const:
|
break;
|
||||||
tmpX->push_back( spot::ltl::clone((*i)) );
|
|
||||||
break;
|
|
||||||
*/
|
|
||||||
|
|
||||||
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 (dynamic_cast<binop*>(*i)->op() == binop::U) {
|
if (dynamic_cast<binop*>(*i)->op() == binop::U)
|
||||||
ftmp = dynamic_cast<binop*>(*i)->second();
|
{
|
||||||
tmpUright = new multop::vec;
|
ftmp = dynamic_cast<binop*>(*i)->second();
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
tmpUright = new multop::vec;
|
||||||
{
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
if (*j == NULL) continue;
|
{
|
||||||
if (node_type(*j) == node_type_form_visitor::Binop)
|
if (*j == NULL) continue;
|
||||||
{
|
if ((node_type(*j) == node_type_form_visitor::Binop)
|
||||||
if (dynamic_cast<binop*>(*j)->op() == binop::U)
|
&&
|
||||||
{
|
(dynamic_cast<binop*>(*j)->op() == binop::U) &&
|
||||||
if (ftmp == dynamic_cast<binop*>(*j)->second())
|
(ftmp == dynamic_cast<binop*>(*j)->second()))
|
||||||
{
|
{
|
||||||
tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first() ));
|
bo = dynamic_cast<binop*>(*j);
|
||||||
if (j != i) {
|
tmpUright
|
||||||
|
->push_back(basic_reduce_form(bo->first()));
|
||||||
|
if (j != i)
|
||||||
|
{
|
||||||
|
destroy(*j);
|
||||||
|
*j = NULL;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
tmpU
|
||||||
|
->push_back(binop::instance(binop::U,
|
||||||
|
multop::
|
||||||
|
instance(multop::
|
||||||
|
And,
|
||||||
|
tmpUright),
|
||||||
|
basic_reduce_form(ftmp)));
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* (a R b) & (a R c) = a R (b & c) */
|
||||||
|
if (dynamic_cast<binop*>(*i)->op() == binop::R)
|
||||||
|
{
|
||||||
|
ftmp = dynamic_cast<binop*>(*i)->first();
|
||||||
|
tmpRright = new multop::vec;
|
||||||
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
|
{
|
||||||
|
if (*j == NULL) continue;
|
||||||
|
if ((node_type(*j) == node_type_form_visitor::Binop)
|
||||||
|
&&
|
||||||
|
(dynamic_cast<binop*>(*j)->op() == binop::R) &&
|
||||||
|
(ftmp == dynamic_cast<binop*>(*j)->first()))
|
||||||
|
{
|
||||||
|
bo = dynamic_cast<binop*>(*j);
|
||||||
|
tmpRright
|
||||||
|
->push_back(basic_reduce_form(bo->second()));
|
||||||
|
if (j != i)
|
||||||
|
{
|
||||||
spot::ltl::destroy(*j);
|
spot::ltl::destroy(*j);
|
||||||
*j = NULL;
|
*j = NULL;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
tmpR
|
||||||
}
|
->push_back(binop::instance(binop::R,
|
||||||
tmpU->push_back(binop::instance(binop::U,
|
basic_reduce_form(ftmp),
|
||||||
multop::instance(multop::And,tmpUright),
|
multop::
|
||||||
basic_reduce_form(ftmp)));
|
instance(multop::And,
|
||||||
break;
|
tmpRright)));
|
||||||
}
|
break;
|
||||||
|
}
|
||||||
/* (a R b) & (a R c) = a R (b & c) */
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
if (dynamic_cast<binop*>(*i)->op() == binop::R) {
|
break;
|
||||||
ftmp = dynamic_cast<binop*>(*i)->first();
|
default:
|
||||||
tmpRright = new multop::vec;
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
break;
|
||||||
{
|
}
|
||||||
if (*j == NULL) continue;
|
spot::ltl::destroy(*i);
|
||||||
if (node_type(*j) == node_type_form_visitor::Binop)
|
|
||||||
{
|
|
||||||
if (dynamic_cast<binop*>(*j)->op() == binop::R)
|
|
||||||
{
|
|
||||||
if (ftmp == dynamic_cast<binop*>(*j)->first())
|
|
||||||
{
|
|
||||||
tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second() ));
|
|
||||||
if (j != i) {
|
|
||||||
spot::ltl::destroy(*j);
|
|
||||||
*j = NULL;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
tmpR->push_back(binop::instance(binop::R,
|
|
||||||
basic_reduce_form(ftmp),
|
|
||||||
multop::instance(multop::And,tmpRright)));
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
|
||||||
break;
|
|
||||||
}
|
}
|
||||||
spot::ltl::destroy(*i);
|
|
||||||
}
|
|
||||||
|
|
||||||
delete(tmpGF);
|
delete(tmpGF);
|
||||||
tmpGF = NULL;
|
tmpGF = NULL;
|
||||||
|
|
@ -438,91 +475,104 @@ namespace spot
|
||||||
|
|
||||||
case multop::Or:
|
case multop::Or:
|
||||||
|
|
||||||
for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
|
for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
|
||||||
if (*i == NULL) continue;
|
{
|
||||||
switch (node_type(*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)*/
|
/* Xa | Xb = X(a | b)*/
|
||||||
if (dynamic_cast<unop*>(*i)->op() == unop::X) {
|
uo = dynamic_cast<unop*>(*i);
|
||||||
tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
|
if (uo && uo->op() == unop::X)
|
||||||
break;
|
{
|
||||||
}
|
tmpX->push_back(basic_reduce_form(uo->child()));
|
||||||
|
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(dynamic_cast<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
|
{
|
||||||
break;
|
uo2 = dynamic_cast<unop*>(uo->child());
|
||||||
}
|
tmpGF->push_back(basic_reduce_form(uo2->child()));
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
break;
|
||||||
break;
|
}
|
||||||
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
|
break;
|
||||||
|
|
||||||
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 (dynamic_cast<binop*>(*i)->op() == binop::U) {
|
if (dynamic_cast<binop*>(*i)->op() == binop::U)
|
||||||
ftmp = dynamic_cast<binop*>(*i)->first();
|
{
|
||||||
tmpUright = new multop::vec;
|
ftmp = dynamic_cast<binop*>(*i)->first();
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
tmpUright = new multop::vec;
|
||||||
{
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
if (*j == NULL) continue;
|
{
|
||||||
if (node_type(*j) == node_type_form_visitor::Binop)
|
if (*j == NULL) continue;
|
||||||
{
|
if ((node_type(*j) == node_type_form_visitor::Binop)
|
||||||
if (dynamic_cast<binop*>(*j)->op() == binop::U)
|
&&
|
||||||
{
|
(dynamic_cast<binop*>(*j)->op() == binop::U) &&
|
||||||
if (ftmp == dynamic_cast<binop*>(*j)->first())
|
(ftmp == dynamic_cast<binop*>(*j)->first()))
|
||||||
{
|
{
|
||||||
tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second()));
|
bo = dynamic_cast<binop*>(*j);
|
||||||
if (j != i) {
|
tmpUright
|
||||||
spot::ltl::destroy(*j);
|
->push_back(basic_reduce_form(bo->second()));
|
||||||
|
if (j != i)
|
||||||
|
{
|
||||||
|
destroy(*j);
|
||||||
*j = NULL;
|
*j = NULL;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
tmpU->push_back(binop::instance(binop::U,
|
||||||
}
|
basic_reduce_form(ftmp),
|
||||||
tmpU->push_back(binop::instance(binop::U,
|
multop::
|
||||||
basic_reduce_form(ftmp),
|
instance(multop::Or,
|
||||||
multop::instance(multop::Or,tmpUright)));
|
tmpUright)));
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
/* (a R b) | (c R b) = (a | c) R b */
|
/* (a R b) | (c R b) = (a | c) R b */
|
||||||
if (dynamic_cast<binop*>(*i)->op() == binop::R) {
|
if (dynamic_cast<binop*>(*i)->op() == binop::R)
|
||||||
ftmp = dynamic_cast<binop*>(*i)->second();
|
{
|
||||||
tmpRright = new multop::vec;
|
ftmp = dynamic_cast<binop*>(*i)->second();
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
tmpRright = new multop::vec;
|
||||||
{
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
if (*j == NULL) continue;
|
{
|
||||||
if (node_type(*j) == node_type_form_visitor::Binop)
|
if (*j == NULL) continue;
|
||||||
{
|
if ((node_type(*j) == node_type_form_visitor::Binop)
|
||||||
if (dynamic_cast<binop*>(*j)->op() == binop::R)
|
&&
|
||||||
{
|
(dynamic_cast<binop*>(*j)->op() == binop::R) &&
|
||||||
if (ftmp == dynamic_cast<binop*>(*j)->second())
|
(ftmp == dynamic_cast<binop*>(*j)->second()))
|
||||||
{
|
{
|
||||||
tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first()));
|
bo = dynamic_cast<binop*>(*j);
|
||||||
if (j != i) {
|
tmpRright
|
||||||
spot::ltl::destroy(*j);
|
->push_back(basic_reduce_form(bo->first()));
|
||||||
|
if (j != i)
|
||||||
|
{
|
||||||
|
destroy(*j);
|
||||||
*j = NULL;
|
*j = NULL;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
tmpR
|
||||||
}
|
->push_back(binop::instance(binop::R,
|
||||||
tmpR->push_back(binop::instance(binop::R,
|
multop::
|
||||||
multop::instance(multop::Or,tmpRright),
|
instance(multop::Or,
|
||||||
basic_reduce_form(ftmp)));
|
tmpRright),
|
||||||
break;
|
basic_reduce_form(ftmp)));
|
||||||
}
|
break;
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
}
|
||||||
break;
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
default:
|
break;
|
||||||
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
|
default:
|
||||||
break;
|
tmpOther->push_back(basic_reduce_form(*i));
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
spot::ltl::destroy(*i);
|
||||||
}
|
}
|
||||||
spot::ltl::destroy(*i);
|
|
||||||
}
|
|
||||||
|
|
||||||
delete(tmpFG);
|
delete(tmpFG);
|
||||||
tmpFG = NULL;
|
tmpFG = NULL;
|
||||||
|
|
@ -535,27 +585,37 @@ namespace spot
|
||||||
delete(res);
|
delete(res);
|
||||||
|
|
||||||
if (tmpX->size())
|
if (tmpX->size())
|
||||||
tmpOther->push_back(unop::instance(unop::X,multop::instance(mo->op(),tmpX)));
|
tmpOther->push_back(unop::instance(unop::X,
|
||||||
|
multop::instance(mo->op(),
|
||||||
|
tmpX)));
|
||||||
else delete(tmpX);
|
else delete(tmpX);
|
||||||
|
|
||||||
if (tmpU->size())
|
if (tmpU->size())
|
||||||
tmpOther->push_back(multop::instance(mo->op(),tmpU));
|
tmpOther->push_back(multop::instance(mo->op(), tmpU));
|
||||||
else delete(tmpU);
|
else delete(tmpU);
|
||||||
|
|
||||||
if (tmpR->size())
|
if (tmpR->size())
|
||||||
tmpOther->push_back(multop::instance(mo->op(),tmpR));
|
tmpOther->push_back(multop::instance(mo->op(), tmpR));
|
||||||
else delete(tmpR);
|
else delete(tmpR);
|
||||||
|
|
||||||
if (tmpGF != NULL)
|
if ((tmpGF != NULL) &&
|
||||||
if (tmpGF->size())
|
(tmpGF->size()))
|
||||||
tmpOther->push_back(unop::instance(unop::G,
|
{
|
||||||
unop::instance(unop::F,
|
ftmp = unop::instance(unop::G,
|
||||||
multop::instance(mo->op(),tmpGF))));
|
unop::instance(unop::F,
|
||||||
if (tmpFG != NULL)
|
multop::instance(mo->op(),
|
||||||
if (tmpFG->size())
|
tmpGF)));
|
||||||
tmpOther->push_back(unop::instance(unop::F,
|
tmpOther->push_back(ftmp);
|
||||||
unop::instance(unop::G,
|
}
|
||||||
multop::instance(mo->op(),tmpFG))));
|
if ((tmpFG != NULL) &&
|
||||||
|
(tmpFG->size()))
|
||||||
|
{
|
||||||
|
ftmp = unop::instance(unop::F,
|
||||||
|
unop::instance(unop::G,
|
||||||
|
multop::instance(mo->op(),
|
||||||
|
tmpFG)));
|
||||||
|
tmpOther->push_back(ftmp);
|
||||||
|
}
|
||||||
|
|
||||||
result_ = multop::instance(op, tmpOther);
|
result_ = multop::instance(op, tmpOther);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -91,13 +91,13 @@ 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_) || (o == Inf))
|
if (!is_eventual(result_) || o == Inf || o == InfBase)
|
||||||
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_) || (o == Inf))
|
if (!is_universal(result_) || o == Inf || o == InfBase)
|
||||||
result_ = unop::instance(unop::G, result_);
|
result_ = unop::instance(unop::G, result_);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
@ -112,7 +112,7 @@ 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 ((o != Inf)
|
if ((o != Inf) && (o != InfBase)
|
||||||
&& ((is_eventual(f2) && ((bo->op()) == binop::U))
|
&& ((is_eventual(f2) && ((bo->op()) == binop::U))
|
||||||
|| (is_universal(f2) && ((bo->op()) == binop::R))))
|
|| (is_universal(f2) && ((bo->op()) == binop::R))))
|
||||||
{
|
{
|
||||||
|
|
@ -122,7 +122,7 @@ namespace spot
|
||||||
/* case of implies */
|
/* case of implies */
|
||||||
formula* f1 = recurse(bo->first());
|
formula* f1 = recurse(bo->first());
|
||||||
|
|
||||||
if (o != EventualUniversal)
|
if (o != EventualUniversal && o != EventualUniversalBase)
|
||||||
{
|
{
|
||||||
bool inf = inf_form(f1, f2);
|
bool inf = inf_form(f1, f2);
|
||||||
bool infinv = inf_form(f2, f1);
|
bool infinv = inf_form(f2, f1);
|
||||||
|
|
@ -206,7 +206,7 @@ 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)));
|
||||||
|
|
||||||
if (o != EventualUniversal)
|
if (o != EventualUniversal && o != EventualUniversalBase)
|
||||||
{
|
{
|
||||||
switch (mo->op())
|
switch (mo->op())
|
||||||
{
|
{
|
||||||
|
|
@ -312,7 +312,8 @@ namespace spot
|
||||||
spot::ltl::formula* ftmp2 = NULL;
|
spot::ltl::formula* ftmp2 = NULL;
|
||||||
reduce_form_visitor v(o);
|
reduce_form_visitor v(o);
|
||||||
|
|
||||||
if (o == BRI)
|
if (o == BRI || o == InfBase ||
|
||||||
|
o == EventualUniversalBase)
|
||||||
{
|
{
|
||||||
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);
|
||||||
|
|
@ -350,11 +351,20 @@ namespace spot
|
||||||
case Inf:
|
case Inf:
|
||||||
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
break;
|
break;
|
||||||
|
case InfBase:
|
||||||
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
|
break;
|
||||||
case EventualUniversal:
|
case EventualUniversal:
|
||||||
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
break;
|
break;
|
||||||
|
case EventualUniversalBase:
|
||||||
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
|
break;
|
||||||
|
case InfEventualUniversal:
|
||||||
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
|
break;
|
||||||
case BRI:
|
case BRI:
|
||||||
ftmp3 = spot::ltl::reduce_form(ftmp2);
|
ftmp3 = spot::ltl::reduce_form(ftmp2, o);
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
assert(0);
|
assert(0);
|
||||||
|
|
|
||||||
|
|
@ -42,7 +42,13 @@ namespace spot
|
||||||
/// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
|
/// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
|
||||||
/// BRI for spot::ltl::reduce_form.
|
/// BRI for spot::ltl::reduce_form.
|
||||||
|
|
||||||
enum option {Base, Inf, EventualUniversal, BRI};
|
enum option {Base,
|
||||||
|
Inf,
|
||||||
|
InfBase,
|
||||||
|
EventualUniversal,
|
||||||
|
EventualUniversalBase,
|
||||||
|
InfEventualUniversal,
|
||||||
|
BRI};
|
||||||
formula* reduce(const formula* f, option o = BRI);
|
formula* reduce(const formula* f, option o = BRI);
|
||||||
|
|
||||||
/// Implement basic rewriting.
|
/// Implement basic rewriting.
|
||||||
|
|
|
||||||
|
|
@ -352,12 +352,19 @@ main(int argc, char** argv)
|
||||||
else if (reduc_r1 | reduc_r2 | reduc_r3)
|
else if (reduc_r1 | reduc_r2 | reduc_r3)
|
||||||
{
|
{
|
||||||
spot::ltl::option o = spot::ltl::BRI;
|
spot::ltl::option o = spot::ltl::BRI;
|
||||||
if (reduc_r1)
|
if (reduc_r1 & !reduc_r2 & !reduc_r3)
|
||||||
o = spot::ltl::Base;
|
o = spot::ltl::Base;
|
||||||
if (reduc_r2)
|
if (!reduc_r1 & reduc_r2 & !reduc_r3)
|
||||||
o = spot::ltl::EventualUniversal;
|
o = spot::ltl::EventualUniversal;
|
||||||
if (reduc_r3)
|
if (reduc_r1 & reduc_r2 & !reduc_r3)
|
||||||
|
o = spot::ltl::EventualUniversalBase;
|
||||||
|
if (!reduc_r1 & !reduc_r2 & reduc_r3)
|
||||||
o = spot::ltl::Inf;
|
o = spot::ltl::Inf;
|
||||||
|
if (reduc_r1 & !reduc_r2 & reduc_r3)
|
||||||
|
o = spot::ltl::InfBase;
|
||||||
|
if (!reduc_r1 & reduc_r2 & reduc_r3)
|
||||||
|
o = spot::ltl::InfEventualUniversal;
|
||||||
|
|
||||||
f = spot::ltl::reduce(f, o);
|
f = spot::ltl::reduce(f, o);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue