I’ve been applying the event reification pattern (thanks people) and finding it extremely useful. It strikes me that implementing it is entirely mechanical and therefore tedious and error-prone.
Would this be a good candidate for some kind of built-in feature that could reflect over the model somehow? I’m not fluent enough to understand if it could be done just within the language.
I’ve created a Pluscal like extension that makes it easier to work with the predicate-as-event model. I think this model also requires you to write a lot of boilerplate and the pluscal syntax seems to simplify this considerably for a certain class of problems.
How do you think the syntax for this event-reification should look like?
Hi
Implementing am extended language for the event reification pattern is indeed in the works. Which is why we reserved some keywords by the way. But, for one, there is actually more to do than what we just showed, so coming up with a general solution is a bit of work. Secondly, contrary to “pure” Electrum, this extension somehow loses the declarative nature of Alloy and looks more like a (neat) state machine framework. For this reason, we believe it should certainly appear as an opt-in feature. Thirdly, such a framework is even more interesting if it also comes with an improved verification technique. But such a technique may also influence the design of the state machine syntactic sugar, so both should be thought out simultaneously. Finally of course, this should also be agreed by the Alloy Board.
that’s why I’m not jumping in here, but it’s an obvious improvement that makes Alloy much more usable (to me). of course, there could be another way altogether to achieve this effect. Maybe it shouldn’t even be in the language, but in the visualisation?
One more thing, when building up a model I’m working on, I found that setting up the events structure showed me where there were multiple candidate events for the next step, which I take to be a clue about narrowing the predicates.
Well I think it’s first and foremost a language and verification matter, but enhancing the Visualizer for a better exploration of traces with first-class events is also useful (we had done this in former, deprecated work).