[Spot] ltlfilt does not exhaustively simplify when --remove-wm is enabled

Simon Jantsch simon.jantsch at gmail.com
Tue Sep 18 14:28:15 CEST 2018


Hello,

I am confused by the fact that the following two commands do not produce the same result:

ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“

ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --simplify=3

The first command gives the same formula as:

ltlfilt --simplify=3 --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --remove-wm

which makes me believe that simplification is done before removing the operators M and W. I would expect ltlfilt to first remove the operators
and then simplify exhaustively.

Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators?

Best regards,
Simon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20180918/14e6fae9/attachment.html>


More information about the Spot mailing list