Hi Yong!
On Tue, Sep 10, 2019 at 6:59 AM Yong Li (李勇) <liyong(a)ios.ac.cn> wrote:
Spot supports LTL with finite semantics (LTLf) but I
found out that Spot
eagerly simplifies the input formulas with LTL semantics.
Exactly; this was reported two weeks ago. See
http://lists.lrde.epita.fr/pipermail/spot/2019q3/000256.html
Is there a an option I can use to make Spot parse the
formula without
simplying it?
Not yet. I believe one workaround is to replace "True" by "alive" in
your input.
--
Alexandre Duret-Lutz