diff --git a/src/ltltest/remove_x.test b/src/ltltest/remove_x.test index a8f3f4931..e81dca283 100755 --- a/src/ltltest/remove_x.test +++ b/src/ltltest/remove_x.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2013 Laboratoire de Recherche et Developement to +# Copyright (C) 2013, 2014 Laboratoire de Recherche et Developement to # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -27,3 +27,13 @@ run 0 ../../bin/ltlfilt --stutter-invariant -f 'F(!a & Xa & Xb)' run 1 ../../bin/ltlfilt --stutter-invariant -f 'F(Xa & Xb)' +run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xa & Xb)' > out +grep -v X out +run 0 ../../bin/ltlfilt --stutter-invariant -F 'out' + + +run 1 ../../bin/ltlfilt --stutter-invariant -f 'F(!a & Xb)' +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 --stutter-invariant -F 'out'