Redundancy in definition of `respects_max_arrivals`
In the definition of respects_max_arrivals
, the precondition t1 <= t2
is not needed. If the condition is not true then the property trivially holds.
In the definition of respects_max_arrivals
, the precondition t1 <= t2
is not needed. If the condition is not true then the property trivially holds.