[BUG] Bogus "Expected Spec to be in the canonical form Init /\ [][Next]_vars"

[lemmy]

Reported as not in canonical form:

VARIABLE x
Init == x = TRUE

Spec == Init /\ [][UNCHANGED x]_x

Works fine:

VARIABLE x
Init == x = TRUE
Next == UNCHANGED x
Spec == Init /\ [][Next]_x

With APALACHE version 0.11.1-SNAPSHOT build v0.11.0-17-gf55663c

[lemmy]

Spec == Init /\ [][TRUE]_x

also not accepted.

[konnov]

Right. Now Apalache is expecting an operator name like Next. A similar issue has been raised by @Quantifier

[Kukovec]

Closing this, as it is effectively a duplicate of #468