Alloy 6 First Impressions

> Alloy is an open source language and analyzer for software modeling.

Regarding the warning about the user forgetting to specify the next-state of a mutable value, it would be great of course but I don't see how to do this in current Alloy. Indeed this detection is dependent on the syntactic context (you need to know in which event you are to know whether a next-state specification is likely to be missing). This is because of the freedom offered by Alloy: events may be written in several ways (predicates, sub-predicates of predicates, in a flat way in a single fact...).

Furthermore, you are even free to specify the value of a mutable object in no event at all. For instance, suppose you're modeling a leader election protocol in a ring (a la Chang&Roberts). To keep track of elected nodes, one way would be to add to every node a mutable Boolean field that becomes true if the said node receives its own identifier from its predecessor in the ring. And then, every event would leave this field unchanged, except for one (e.g. receiving a message) that would possibly set the field to true. But another, nice way offered by the declarative approach of Alloy would be to just declare a mutable set of elected nodes. An then, you'd simply add a fact stating that, in every state (`always` in our logic), the set of elected nodes is equal to those nodes which have received their identifier at least (`once` past operator). If you model things this way, then raising a warning would necessarily be wrong. In fact, we should raise a warning if the opposite is done, that is if the user specifies the next-state of the "elected" set in an event! Of course, a warning is wahat it is, it doesn't have to be true all the time, but we expect it to be raised for a good reason, say, 90% of times.

I think the best solution here would be to create a stricter extension of Alloy, with an event blocks to delimit events clearly. We've made such experiments a couple of times this past year. The result is my opinion quite nice but you have to sacrifice a lot of the flexibility that Alloy is particularly good at.

I'd personally prefer the latter. I find that temporal logic is significantly easier to understand than the usual Alloy workarounds (vs. e.g. stuff I've done with TLA+).