% All processes requesting a number can eventually enter the critical section
% Described in "A Checker for Modal Formulas on Processed with Data",
% J.F. Groote and T.A.C. Willemse
nu X . ([true]X && forall b:Bool. [request(b)]mu Y. <true> Y || <enter(b)> true)

