Regarding "moving" data in the Visualizer, I also wish we had a better situation (the problem already existed with older versions of Alloy). We've made several experiments to enhance the visualization of two different states featuring the same data. But it's very tricky because you sometimes want the same data to appear at the same place in two graphs, and sometimes not. Until now, I'd say we have at least two open questions: what do we want the user to be able to specify (regarding graphical representation) and how to specify it.
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 don’t know whether it’s better to cover all the static Alloy and then dynamics or to thread temporal logic through the usual route.
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+).
I don't know Iris well but the logical setting and aims are completely different. Iris' primary application is proving safety properties of concurrent programs, with the possibility to express fine properties about memory thanks to separation logic. Alloy is a modeling language: there's no notion of program per se, just a logic. Then Iris relies on a very powerful logic so I guess a substantial amount of human intervention (Coq tactics) is needed to prove some property. Alloy is a so-called lightweight formal method (it trades power for efficiency if I may say so): analysis is fully automatic but limited to a bounded state space (the bound is given by the user). So Alloy is good at finding bugs in specifications, far less at proving things once and for all. Still, we found that it was very useful when doing full proofs (e.g. with the Event-B method) as its fast-bug-finding capabilities make it a very good tool to quickly evaluate an idea (before going full proof). Finally, on the language side, Alloy 6 can be used to specify safety and liveness properties.
> Alloy is an open source language and analyzer for software modeling.