Re: [Spot] Issue with SPOT and LTLf

On Wed, Aug 28, 2019 at 8:10 AM Andrew Wells <andrewmw94(a)gmail.com> wrote: [...] [...] [...] Hi Andrew, Hmmm... The problem is that Spot really support only LTL over infinite words, so its LTL operators have some hard-coded simplifications when the arguments are true/false (e.g., F(0)=0, F(1)=1, G(0)=0, G(1)=1, X(0)=0, X(1)=1) or for idempotence rules (FFa = Fa, GGa=Ga, etc.) Those rules are listed as "trivial identities" in several sub-sections of https://spot.lrde.epita.fr/tl.pdf and are automatically applied every time an LTL formula is constructed. So there is actually no way to represent the formula ((a && b) U (! (X 1))) in Spot: because X(1)=1, !1=0, and (a && b) U 0 = 0, the output of the parser is already 0. The LTL simplifier and translations algorithms also rely on the fact that these trivial identities (especially X(1)=1) are automatically simplified. When I added the from_ltlf() function to help support LTLf, I did not realize those trivial identities could cause any problem. I'm just realizing that with your email. Looking at the list of trivial identities we have, I believe X(1)=1 is the only one that makes no sense in LTLf. Do you agree? I'm not sure what is the best way to fix that. I guess we need a way to disable the X(1)=1 simplification, at least during parsing. That could be an option for the constructor of X, and for the parser. Or we could introduce support for two versions of X (weak/strong) with different trivial identities, getting us closer to the PSL standard. In this particular case, because from_ltlf() will add some "alive" property in your formula, a simple workaround for you would be to alter the input formula to use X(alive) instead of X(1). -- Alexandre Duret-Lutz