# Library prosa.analysis.definitions.priority.classes

Require Export prosa.model.priority.classes.
We define properties linking JLFP and FP policies.
Section JLFP_FP.
Consider any type of tasks ...
Context {Task : TaskType}.
... and any type of jobs associated with these tasks, ...
Context {Job : JobType}.
Context `{JobTask Job Task}.
Consider any pair of JLFP and FP policies.
Context (JLFP : JLFP_policy Job) (FP : FP_policy Task).
A JLFP policy is compatible with a FP policy if the priority of the first on jobs doesn't contradict the priority of the second on tasks.
Definition JLFP_FP_compatible :=
(∀ j1 j2, hep_job j1 j2 → hep_task (job_task j1) (job_task j2))
∧ (∀ j1 j2, hp_task (job_task j1) (job_task j2) → hep_job j1 j2).
End JLFP_FP.