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