how to add weak fairness on actions

Brian Hicks, March 6, 2023

In Alloy, you can add weak fairness to actions (that is, ensure that they'll always eventually fire if they're able) by saying:

(eventually always p) implies (always eventually q)

In English, this means: "if p is eventually true, then q will eventually be true at all points afterwards." In other words, p is the condition under which q can happen.

Note that you should be careful about existential (some) vs universal (all) quantifiers with this kind of statement. For example:

all t: Thing {
  (eventually always enabled[t]) implies (always eventually do[t])
}

Saying all here means that every time the condition enabled is true the action do is eventually taken. If this said some t: Thing instead, that would mean that this condition would only be true some of the time.

Source: Alcino Cunha's answer to my question about this on the Alloy discourse instance