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

simplify: save some work using a temporary variable.

Browse source 
This is actually an attempt to workaround what might be a compiler bug.
(valgrind complains about some uninitialized memory being read on this
line).

* src/ltlvisit/simplify.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2015-09-27 17:58:41 +02:00
parent 3ad002be5f
commit 96806681e0
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ltlvisit/simplify.cc
View file

@ -1659,9 +1659,12 @@ namespace spot
// if a => c, then a U (b R (c W d)) = (b R (c W d))
// if a => c, then a U (b M (c U d)) = (b M (c U d))
// if a => c, then a U (b M (c W d)) = (b M (c W d))
if (b.is(op::R, op::M) && b.nth(1).is(op::U, op::W)
&& c_->implication(a, b.nth(1).nth(0)))
return b;
if (b.is(op::R, op::M))
{
auto c1 = b.nth(1);
if (c1.is(op::U, op::W) && c_->implication(a, c1.nth(0)))
return b;
}
// if a => b, then (a U c) U b = c U b
// if a => b, then (a W c) U b = c U b
if (a.is(op::U, op::W) && c_->implication(a.nth(0), b))