Temporal translation broken with nested temporal subformulas and quantifiers

[thpani]

Temporal translation broken with nested temporal subformulas and quantifiers

[thpani]

Are we talking about main or the temporal branch?

main.

This is non-blocking, I just created the issue to have it on file.

[p-offtermatt]

iirc this is not supported at all - I remember stumbling over this and I think the decision was to focus on the non-quantifier case, and the quantified temporal-formula case was never finished

[thpani]

@p-offtermatt Do you remember if you considered this during your internship?
That is, is this kind of property not supported at all?

[Kukovec]

Are we talking about main or the temporal branch?

[josef-widder]

I think for many specs we can work around that. Even in the draft spec that I have written, I first had written temporal formulas where indices don't range over temporal operators (because that is what I am used to in the parameterized case).

But then I realized that to others (e.g., clients), the formula that creates the troubles might be more readable.

From a user perspective, the error message was a bit frightening, though. Would it be hard to identify whether the temporal formula is outside of the fragment Apalache supports, and in this case return a better error message?

[thpani]

From a user perspective, the error message was a bit frightening, though. Would it be hard to identify whether the temporal formula is outside of the fragment Apalache supports, and in this case return a better error message?

Yes, we should issue a proper error message if the property is outside the supported language fragment.