How to reduce temporal update boilerplate for state-rich models?

[grayswandyr]

Completing other answers, I wrote some months ago a post about how to model stateful models in our so called “reified event” style.

@DanielJackson

— Organize events into a hierarchy using signature extension, and associate frame conditions with larger event classes. For example, in the hotel model in my book (p. 204), there’s a class of events called RoomKeyEvent which has a frame condition associated with it saying there is no change at the front desk.

If you use the novel, built-in-temporal features of Alloy 6, I would advise against this style and would favor the reified event cited hereabove. The latter has all advantages of Daniel’s, while it doesn’t suffer from the tricky part, which is you don’t know how many atoms you may need in traces (you may miss some traces due to a bad scope specification for the event signature).

@hwayne

You could use a macro. Off the top of my head, it might look something like

let unchanged[x] = x' = x

I’m using this, but I write it as follows to avoid bad surprises with the possible application of the prime symbol over a compound expression:

let unchanged[x] { (x)' = (x) }