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

Force Clang and GCC to have the same behaviour.

Browse source 
* src/ltlvisit/remove_x.cc, src/ltltest/remove_x.test: here.
This commit is contained in:
Etienne Renault 2015-04-17 08:55:56 +01:00
parent 439517736f
commit dc7ca7d8d2
2 changed files with 24 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ltltest/remove_x.test
View file

@ -38,3 +38,11 @@ run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xb)' > out
grep -v X out
# The output is stutter invariant, even if the input wasn't.
run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out'
# Ensure remove_x does not depend on clang or gcc recursive calls
echo 'F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) |'\
' (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b))'\
' & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b)))'\
' | (!a & b & (G!a | Ga) & (G!b | Gb))))' > expected
run 0 ../../bin/ltlfilt --remove-x -f 'F(a & X(!a & b))' > 'out'
diff expected out

22
src/ltlvisit/remove_x.cc
View file

@ -75,8 +75,12 @@ namespace spot
for (atomic_prop_set::const_iterator j = aps.begin();
j != aps.end(); ++j)
if (*j != *i)
va1->push_back(OR(U((*j)->clone(), npi->clone()),
U(NOT((*j)->clone()), npi->clone())));
{
// make sure the arguments of OR are created in a
// deterministic order
auto tmp = U(NOT((*j)->clone()), npi->clone());
va1->push_back(OR(U((*j)->clone(), npi->clone()), tmp));
}
vo->push_back(multop::instance(multop::And, va1));
// Second line
multop::vec* va2 = new multop::vec;
@ -85,8 +89,12 @@ namespace spot
for (atomic_prop_set::const_iterator j = aps.begin();
j != aps.end(); ++j)
if (*j != *i)
va2->push_back(OR(U((*j)->clone(), (*i)->clone()),
U(NOT((*j)->clone()), (*i)->clone())));
{
// make sure the arguments of OR are created in a
// deterministic order
auto tmp = U(NOT((*j)->clone()), (*i)->clone());
va2->push_back(OR(U((*j)->clone(), (*i)->clone()), tmp));
}
vo->push_back(multop::instance(multop::And, va2));
}
const formula* l12 = multop::instance(multop::Or, vo);
@ -95,8 +103,10 @@ namespace spot
for (atomic_prop_set::const_iterator i = aps.begin();
i != aps.end(); ++i)
{
va3->push_back(OR(G((*i)->clone()),
G(NOT((*i)->clone()))));
// make sure the arguments of OR are created in a
// deterministic order
auto tmp = G(NOT((*i)->clone()));
va3->push_back(OR(G((*i)->clone()), tmp));
}
result_ = OR(l12, AND(multop::instance(multop::And, va3), c));
return;