% MEASURE0
AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1))