Library prosa.model.priority.fifo
FIFO Priority Policy
Consider jobs with arrival times.
A JLFP policy is FIFO if it never assigns higher priority to a
later-arriving job. Ties among jobs that arrive at the same time may be
resolved by any reflexive, transitive, and total tie-breaking rule.
Definition policy_is_FIFO (JLFP : JLFP_policy Job) :=
(∀ j1 j2, hep_job j1 j2 → job_arrival j1 ≤ job_arrival j2)
∧ reflexive_job_priorities JLFP
∧ transitive_job_priorities JLFP
∧ total_job_priorities JLFP.
End FIFOPolicy.
(∀ j1 j2, hep_job j1 j2 → job_arrival j1 ≤ job_arrival j2)
∧ reflexive_job_priorities JLFP
∧ transitive_job_priorities JLFP
∧ total_job_priorities JLFP.
End FIFOPolicy.