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.