
10 Sep
2019
10 Sep
'19
6:58 a.m.
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