Is Time a reserved keyword in Electrum?
sig Time{}
run {}
gives the error message
Syntax error at line 1 column 5:
There are 3 possible tokens that can appear here:
NAME seq this
Hi
it has been for a long time (!). BUT, since the preparation of the merger of Electrum into Alloy 6, we changed this (to keep “old” Alloy models working without modification).
Starting at Electrum v2.1 (I think), Time isn’t a keyword anymore in Electrum.
I suggest you download the latest release which is as of today v2.1.5. Up to minor changes, this the version merged into the Alloy 6 repository.
Up-to-date, end-user-intended documentation is in preparation but, meanwhile you can refer to the Language Reference for accurate information regarding Electrum v2.1+/Alloy 6 (in particular keywords).
Hope this helps.
Thanks for the hint,
in v 2.1.5 Time is no reserved word anymore and old Alloy specs are processed fine.
Kind regards,
Burt.
One caveat: the prime symbol now means something in Electrum/Alloy 6, and this may change the meaning of old Alloy models. Please update them accordingly if needed, for instance by replacing every prime symbol ' by a (so-called) neutral double-quotation mark " (which happens to be legal Alloy).
Awww this makes me sad, because I’m used to using " for writing fact names. Why ' and not backtick, which would be backwards compatible with all previous alloy models?
(Realize it might be too late to change, just asking)
You can still use " for fact names.
We chose ' because it’s the standard way to represent post-state in most formal methods… BTW, although this did not influence our choice consciously, notice also that backticks are hard to type on some non-US keyboards and even to name (I don’t know how to call this symbol in my native language for instance, apart from using an awkward, long description: “apostrophe à l’envers”, not cool when teaching!).