Support for "flag-based" invariants

[shonfeder]

@p-offtermatt has shared the view that there is a certain class of invariants which -- while formalizable as trace invariants or temporal properties -- are easiest to communicate to implementation engineers as "flag-based" invariants. Iiuc, this has a form like

If flag f is (resp. is not) set in state s, then p should (resp. should not) hold.

where f tracks the prior occurrence of some event.

This issue is to track discussion of what support for this might look like, whether thru an idiom, library operator, or some syntactic construct.

Of particular consideration here is that we often don't want to clutter the state of the system with an auxiliary variable to track this kind of thing. This suggest that we may want to translate this as a temporal property, or provide a way of having "hidden state".

[konnov]

Why don't you just use implication: f implies p?

[p-offtermatt]

To clarify, a fictitious example would be this:

val GetsUpdatesAfterOptingIn: HasOptedIn implies FooGetsUpdates

FooGetsUpdates might be a very simple predicate over the current state, e.g. foo.in(recipients)

However, HasOptedIn might not be as simple - intuitively, this predicate should be true after there was a OptInAction, and then become false again when there is an OptOutAction, e.g.

action OptInAction = all {
   ...,
   HasOptedIn' = true
}

action OptOutAction = all {
   ...,
   HasOptedIn' = false
}

Of course, we can just have a flag in the state that is set to true on OptInAction, and then to false on OptOutAction. But imagine we have a large model, and this flag is used nowhere except for this invariant (e.g. because OptInAction does not simply set a flag to indicate the opting-in, but does something more complex, e.g. send a message somewhere, which can be delivered or dropped, etc)

This is a temporal property roughly like currentAction = OptInAction implies (FooGetsUpdates weakuntil currentAction = OptOutAction). But notice that this is very easy to write and understand if we have this little flag, instead.

Then the idea was that it might be nice to not pollute the whole state space of the model with this flag, but rather keep it contained to this one invariant where it is actually used. And the flag is then what allows us to write it exactly as you suggested, with a single implication.