[Spot] Re: Issue in translation from LTLf

Hi Marco, Marco Faella <marfaella@gmail.com> writes:

It seems that subformulas of the type "X p" get translated into "X (!alive | p)" instead of "X (alive & p)", as they should be according to the LTLf semantics, as well as the translation outlined in the Memocode '14 paper by Dutta and Vardi.

This all depends on whether you consider X to be weak or strong. That paper gives the semantics for a strong X. However, in Spot - X is the weak next. - X[!] is the strong next. See https://spot.lre.epita.fr/tut12.html#org0e1e575