Dear Spot developers,
I am Yong Li from Chinese Academy of Sciences and I am writing to you to
ask a question about parsing LTLf (LTL over finite traces) formulas.
Spot supports LTL with finite semantics (LTLf) but I found out that Spot
eagerly simplifies the input formulas with LTL semantics.
For instance, if I use command line ltlfilt --from-ltlf -f "a U !(X
True)", Spot immediately gives me 0.
This is not correct since the input formula should be satisfiable in
LTLf semantics.
I wonder whether there is a way to get around it?
Is there a an option I can use to make Spot parse the formula without
simplying it?
Regards,
Yong