once p is true, it's always true
Brian Hicks, August 28, 2023
In Alloy, to say "once this is true, it's always true", you say:
always (p implies always p)
This is true because
always means "in all states starting from this one." So, the outer "always" means that the condition is always true starting from the initial time. Once
p is true, the
implies says that it will always remain true.
If you did just
p implies always p without the wrapper, that would be saying "if
p is true at the initial time then
p will always be true."
Source: Alcino Cunha's answer to my question about this on the Alloy discourse instance