Some comments about facts and invariants:
- the term invariant is subject to various meanings depending on situations:
- it may refer, in the style of so-called axiomatic semantics or Floyd-Hoare assertions, to a property that is preserved by every operation. Which requires, in your model, a notion of operation or event or action… You may check these properties with pure Alloy in fact.
- in some contexts, people use the term to refer to properties that are always true, that is true in every reachable state. In Electrum, this would correspond to a property of the shape
always P,Pbeing a pure first-order constraint.
- general facts are axioms: that is constraints imposed on any instance. They may contain any constraint: therefore they are not necessarily invariants.
- signature facts are implicitly preprended an
alwaysconnective so, if they only contain a pure first-order constraint, then they define an invariant (this is to mimick class invariants of OO design).
About events: for typical modelling, I would advise to use predicates to represent events. Using sigs is risky: indeed, in some contexts, due to the command scope applying to event sigs too, you may prune instances which require more events than there are possible instances for them, and (possibly) miss the violation of a property. Predicates are OTOH immune to this. If you still want to visualize events and manipulate them like sigs, I think it’s better to use event reification.