For any action A and state function v, the weak fairness formula

  WF (A)
    v

esentially asserts that if action A is ever continuously enabled, then an A step must eventually occur.

More precisely, it asserts that action

  <A>
     v

is infinitely often disabled, or else infinitely many

  <A>
     v

steps occur.

Formally, it is defined by

  WF (A)  ==  []<> ~Enabled <A>  \/  []<> <A>
    v                          v             v