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
Hi Simon,
On Sun, Sep 23, 2018 at 5:46 PM Simon Jantsch simon.jantsch@gmail.com wrote:
which makes me believe that simplification is done before removing the operators M and W.
Yes. It has to be in this order because the simplifications can detect patterns that correspond to M or W, and reintroduce these operators...
Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators?
I'm afraid we don't have that. Simplification and unabbrevation are two separate functions, and rewriting those to be a single function would be a lot of work. I've an idea that could improve this specific case, but that isn't like the "simplify with restricted operators" solution you could dream of. See https://gitlab.lrde.epita.fr/spot/spot/issues/362
-
Alexandre Duret-Lutz -
Simon Jantsch