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

Typo in the code rewriting "a M 1 = Fa".

Browse source 
* src/ltlvisit/simplify.cc (simplify_visitor): Fix it,
and leave the trace code.
This commit is contained in:
Alexandre Duret-Lutz 2011-08-24 16:59:50 +02:00
parent c2335edb57
commit d4d4c0e7d3
1 changed files with 20 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/ltlvisit/simplify.cc
View file

@ -1199,6 +1199,7 @@ namespace spot
if (opt_.event_univ) if (opt_.event_univ)
{ {
trace << "bo: trying eventuniv rules" << std::endl;
/* If b is a pure eventuality formula then a U b = b. /* If b is a pure eventuality formula then a U b = b.
If b is a pure universality formula a R b = b. */ If b is a pure universality formula a R b = b. */
if ((b->is_eventual() && (op == binop::U)) if ((b->is_eventual() && (op == binop::U))
@ -1229,11 +1230,13 @@ namespace spot
tmp->destroy(); tmp->destroy();
return; return;
} }
trace << "bo: no eventuniv rule matched" << std::endl;
} }
// Inclusion-based rules // Inclusion-based rules
if (opt_.synt_impl | opt_.containment_checks) if (opt_.synt_impl | opt_.containment_checks)
{ {
trace << "bo: trying inclusion-based rules" << std::endl;
switch (op) switch (op)
{ {
case binop::Xor: case binop::Xor:
@ -1396,14 +1399,17 @@ namespace spot
} }
break; break;
} }
trace << "bo: no inclusion-based rules matched" << std::endl;
} }
if (!opt_.reduce_basics) if (!opt_.reduce_basics)
{ {
trace << "bo: basic reductions disabled" << std::endl;
result_ = binop::instance(op, a, b); result_ = binop::instance(op, a, b);
return; return;
} }
trace << "bo: trying basic reductions" << std::endl;
// Rewrite U,R,W,M as F or G when possible. // Rewrite U,R,W,M as F or G when possible.
switch (op) switch (op)
{ {
@ -1433,7 +1439,7 @@ namespace spot
break; break;
case binop::M: case binop::M:
// a M true == F(a) // a M true == F(a)
if (b == constant::false_instance()) if (b == constant::true_instance())
{ {
result_ = recurse_destroy(unop::instance(unop::F, a)); result_ = recurse_destroy(unop::instance(unop::F, a));
return; return;
@ -2185,14 +2191,26 @@ namespace spot
simplify_recursively(const formula* f, simplify_recursively(const formula* f,
ltl_simplifier_cache* c) ltl_simplifier_cache* c)
{ {
trace << "** simplify_recursively(" << to_string(f) << ")";
formula* result = const_cast<formula*>(c->lookup_simplified(f)); formula* result = const_cast<formula*>(c->lookup_simplified(f));
if (result) if (result)
return result; {
trace << " cached: " << to_string(result) << std::endl;
return result;
}
else
{
trace << " miss" << std::endl;
}
simplify_visitor v(c); simplify_visitor v(c);
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
result = v.result(); result = v.result();
trace << "** simplify_recursively(" << to_string(f) << ") result: "
<< to_string(result) << std::endl;
c->cache_simplified(f, result); c->cache_simplified(f, result);
return result; return result;
} }