Skip to content
GitLab
Commit f2f10852 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style. 

* sanity/style.test: More tests.
parent aa5368ba
Hide whitespace changes
Inline Side-by-side
ChangeLog
View file @ f2f10852
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
* sanity/style.test: More tests.
* src/tgbatest/ltl2tgba.cc (main): Fix style.
* HACKING: Mention `else if'.
......
src/ltltest/inf.cc
View file @ f2f10852
......@@ -64,23 +64,26 @@ main(int argc, char** argv)
int exit_return = 0;
std::cout << "Test f1 < f2" << std::endl;
if (spot::ltl::inf_form(f1,f2)) {
std::cout << f1s << " < " << f2s << std::endl;
exit_return = 1;
}
if (spot::ltl::inf_form(f1, f2))
{
std::cout << f1s << " < " << f2s << std::endl;
exit_return = 1;
}
/*
std::cout << "Test !f1 < f2" << std::endl;
if (spot::ltl::infneg_form(f1,f2,0)) {
std::cout << "!(" << f1s << ") < " << f2s << std::endl;
exit_return = 2;
}
if (spot::ltl::infneg_form(f1, f2, 0))
{
std::cout << "!(" << f1s << ") < " << f2s << std::endl;
exit_return = 2;
}
std::cout << "Test f1 < !f2" << std::endl;
if (spot::ltl::infneg_form(f1,f2,1)) {
std::cout << f1s << " < !(" << f2s << ")" << std::endl;
exit_return = 3;
}
if (spot::ltl::infneg_form(f1, f2, 1))
{
std::cout << f1s << " < !(" << f2s << ")" << std::endl;
exit_return = 3;
}
*/
spot::ltl::dump(std::cout, f1); std::cout << std::endl;
......
src/ltltest/reduc.cc
View file @ f2f10852
......@@ -45,20 +45,22 @@ main(int argc, char** argv)
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;
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;
......@@ -69,12 +71,13 @@ main(int argc, char** argv)
return 2;
if (argc == 4){
spot::ltl::parse_error_list p2;
f2 = spot::ltl::parse(argv[3], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
return 2;
}
if (argc == 4)
{
spot::ltl::parse_error_list p2;
f2 = spot::ltl::parse(argv[3], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
return 2;
}
int exit_code = 0;
......@@ -93,7 +96,7 @@ main(int argc, char** argv)
std::string f1s_before = spot::ltl::to_string(f1);
ftmp1 = f1;
f1 = spot::ltl::reduce(f1,o);
f1 = spot::ltl::reduce(f1, o);
ftmp2 = f1;
f1 = spot::ltl::unabbreviate_logic(f1);
spot::ltl::destroy(ftmp1);
......@@ -103,51 +106,56 @@ main(int argc, char** argv)
std::string f1s_after = spot::ltl::to_string(f1);
bool red = (length_f1_after < length_f1_before);
if (red);
std::string f2s = "";
if (f2 != NULL) {
ftmp1 = f2;
f2 = unabbreviate_logic(f2);
ftmp2 = f2;
f2 = negative_normal_form(f2);
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2);
ftmp1 = f2;
f2 = unabbreviate_logic(f2);
spot::ltl::destroy(ftmp1);
f2s = spot::ltl::to_string(f2);
}
if (f2 != NULL)
{
ftmp1 = f2;
f2 = unabbreviate_logic(f2);
ftmp2 = f2;
f2 = negative_normal_form(f2);
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2);
ftmp1 = f2;
f2 = unabbreviate_logic(f2);
spot::ltl::destroy(ftmp1);
f2s = spot::ltl::to_string(f2);
}
if (red && (f2 == NULL)) {
std::cout << length_f1_before << " " << length_f1_after
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
<< std::endl;
}
if (red && !f2)
{
std::cout << length_f1_before << " " << length_f1_after
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
<< std::endl;
}
if (f2 != NULL){
if (f1 != f2) {
if (length_f1_after < length_f1_before)
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " KOREDUC " << std::endl;
if (f2)
{
if (f1 != f2)
{
if (length_f1_after < length_f1_before)
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " KOREDUC " << std::endl;
else
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " KOIDEM " << std::endl;
exit_code = 1;
}
else
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " KOIDEM " << std::endl;
exit_code = 1;
{
if (f1s_before != f1s_after)
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " OKREDUC " << std::endl;
else
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " OKIDEM" << std::endl;
exit_code = 0;
}
}
else {
if (f1s_before != f1s_after)
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " OKREDUC " << std::endl;
else
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
<< " OKIDEM" << std::endl;
exit_code = 0;
else
{
if (length_f1_after < length_f1_before)
exit_code = 0;
}
}
else{
if (length_f1_after < length_f1_before) exit_code = 0;
}
spot::ltl::destroy(f1);
if (f2 != NULL)
......
src/ltlvisit/reducform.cc
View file @ f2f10852
......@@ -90,17 +90,15 @@ namespace spot
return;
case unop::F:
/* if f is class of eventuality then F(f)=f */
if (!is_eventual(result_) || (o == Inf)) {
/* If f is class of eventuality then F(f)=f. */
if (!is_eventual(result_) || (o == Inf))
result_ = unop::instance(unop::F, result_);
}
return;
case unop::G:
/* if f is class of universality then G(f)=f */
if (!is_universal(result_) || (o == Inf)) {
/* If f is class of universality then G(f)=f. */
if (!is_universal(result_) || (o == Inf))
result_ = unop::instance(unop::G, result_);
}
return;
}
/* Unreachable code. */
......@@ -112,86 +110,86 @@ namespace spot
{
formula* f2 = recurse(bo->second());
/* if b is of class eventuality then a U b = b
if b is of class universality then a R b = b */
if (o != Inf) {
if ((is_eventual(f2) && ((bo->op()) == binop::U)) ||
(is_universal(f2) && ((bo->op()) == binop::R)))
{
result_ = f2;
return;
}
}
/* If b is of class eventuality then a U b = b.
If b is of class universality then a R b = b. */
if ((o != Inf)
&& ((is_eventual(f2) && ((bo->op()) == binop::U))
|| (is_universal(f2) && ((bo->op()) == binop::R))))
{
result_ = f2;
return;
}
/* case of implies */
formula* f1 = recurse(bo->first());
if (o != EventualUniversal) {
bool inf = inf_form(f1,f2);
bool infinv = inf_form(f2,f1);
bool infnegleft = infneg_form(f2,f1,0);
bool infnegright = infneg_form(f2,f1,1);
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
break;;
case binop::U:
/* a < b => a U b = b */
if (inf)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* !b < a => a U b = Fb */
if (infnegleft)
{
result_ = unop::instance(unop::F, f2);
spot::ltl::destroy(f1);
return;
}
/* a < b => a U (b U c) = (b U c) */
if (node_type(f2) == node_type_form_visitor::Binop)
if (dynamic_cast<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:
/* b < a => a R b = b */
if (infinv)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* b < !a => a R b = Gb */
if (infnegright)
{
result_ = unop::instance(unop::G, f2);
spot::ltl::destroy(f1);
return;
}
/* b < a => a R (b R c) = b R c */
if (node_type(f2) == node_type_form_visitor::Binop)
if (dynamic_cast<binop*>(f2)->op() == binop::R)
if (inf_form(dynamic_cast<binop*>(f2)->first(),f1))
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
break;
}
}
if (o != EventualUniversal)
{
bool inf = inf_form(f1, f2);
bool infinv = inf_form(f2, f1);
bool infnegleft = infneg_form(f2, f1, 0);
bool infnegright = infneg_form(f2, f1, 1);
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
break;;
case binop::U:
/* a < b => a U b = b */
if (inf)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* !b < a => a U b = Fb */
if (infnegleft)
{
result_ = unop::instance(unop::F, f2);
spot::ltl::destroy(f1);
return;
}
/* a < b => a U (b U c) = (b U c) */
if (node_type(f2) == node_type_form_visitor::Binop
&& dynamic_cast<binop*>(f2)->op() == binop::U
&& inf_form(f1, dynamic_cast<binop*>(f2)->first()))
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
break;
case binop::R:
/* b < a => a R b = b */
if (infinv)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* b < !a => a R b = Gb */
if (infnegright)
{
result_ = unop::instance(unop::G, f2);
spot::ltl::destroy(f1);
return;
}
/* b < a => a R (b R c) = b R c */
if (node_type(f2) == node_type_form_visitor::Binop
&& dynamic_cast<binop*>(f2)->op() == binop::R
&& inf_form(dynamic_cast<binop*>(f2)->first(), f1))
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
break;
}
}
result_ = binop::instance(bo->op(), f1, f2);
}
......@@ -208,97 +206,98 @@ namespace spot
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
if (o != EventualUniversal){
switch (mo->op())
{
case multop::Or:
index = indextmp = res->begin();
if (index != res->end())
{
f1 = *index;
index++;
}
for (; index != res->end();index++)
{
f2 = *index;
/* a < b => a + b = b */
if (inf_form(f1,f2)) // f1 < f2
{
f1 = f2;
spot::ltl::destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
else if (inf_form(f2,f1)) // f2 < f1
{
spot::ltl::destroy(*index);
res->erase(index);
index--;
}
}
break;
case multop::And:
index = indextmp = res->begin();
if (mos)
{
f1 = mo->nth(0);
index++;
}
for (; index != res->end(); index++)
{
f2 = *index;
/* a < b => a & b = a */
if (inf_form(f1,f2)) // f1 < f2
{
spot::ltl::destroy(*index);
res->erase(index);
index--;
}
else if (inf_form(f2,f1)) // f2 < f1
{
f1 = f2;
spot::ltl::destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
}
break;
}
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (index = res->begin(); index != res->end(); index++) {
for (indextmp = res->begin(); indextmp != res->end(); indextmp++) {
if (index != indextmp){
if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) {
for (multop::vec::iterator j = res->begin(); j != res->end(); j++) {
spot::ltl::destroy(*j);
if (o != EventualUniversal)
{
switch (mo->op())
{
case multop::Or:
index = indextmp = res->begin();
if (index != res->end())
{
f1 = *index;
index++;
}
for (; index != res->end();index++)
{
f2 = *index;
/* a < b => a + b = b */
if (inf_form(f1, f2)) // f1 < f2
{
f1 = f2;
spot::ltl::destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
else if (inf_form(f2, f1)) // f2 < f1
{
spot::ltl::destroy(*index);
res->erase(index);
index--;
}
}
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
return;
}
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
&& infneg_form(*index,*indextmp,
(mo->op() == multop::Or) ? 0 : 1))
{
for (multop::vec::iterator j = res->begin();
j != res->end(); j++)
spot::ltl::destroy(*j);
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
return;
}
}
if (res->size())
{
result_ = multop::instance(mo->op(), res);
return;
}
}
if (res->size()) {
result_ = multop::instance(mo->op(),res);
return;
}
assert(0);
}
formula*
recurse(formula* f)
{
return reduce_form(f,o);
return reduce_form(f, o);
}
protected:
......@@ -313,19 +312,21 @@ namespace spot
spot::ltl::formula* ftmp2 = NULL;
reduce_form_visitor v(o);
if (o == BRI) {
ftmp1 = spot::ltl::basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(v.result());
if (o == BRI)
{
ftmp1 = spot::ltl::basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(v.result());
return ftmp2;
}
else {
const_cast<formula*>(f)->accept(v);
return v.result();
}
return ftmp2;
}
else
{
const_cast<formula*>(f)->accept(v);
return v.result();
}
/* unreachable code */
assert(0);
......@@ -341,22 +342,23 @@ namespace spot
ftmp1 = spot::ltl::unabbreviate_logic(f);
ftmp2 = spot::ltl::negative_normal_form(ftmp1);
switch (o) {