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

Alexandre Duret-Lutz adl at lrde.epita.fr
Sun Sep 23 19:27:36 CEST 2018


Hi Simon,

On Sun, Sep 23, 2018 at 5:46 PM Simon Jantsch <simon.jantsch at 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


More information about the Spot mailing list