weak_fairness

vstd_extra::temporal_logic::defs

Function weak_fairness 

Source 
pub open spec fn weak_fairness<T>(action_pred: ActionPred<T>) -> TempPred<T>
Expand description
{ always(lift_state(enabled(action_pred))).leads_to(lift_action(action_pred)) }