Library prosa.implementation.priority.numeric_fixed_priority

Require Export prosa.model.priority.numeric_fixed_priority.

Numeric Fixed Task Priorities

In this section, we define ascending numeric fixed priorities, where a larger numeric value indicates higher priority, and note some trivial facts about this interpretation of priority values.
Section PropertiesNFPA.

The instance numeric_fp_ascending assigns higher priority to tasks with higher numeric task_priority value.
  #[local] Instance numeric_fp_ascending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
  {
    hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≥ task_priority tsk2
  }.

Consider any kind of tasks with specified priorities.
  Context {Task : TaskType} `{TaskPriority Task}.

The concrete numeric_fp_ascending implementation is indeed an ascending numeric FP policy.
  Fact NFPA_is_numeric_FP_ascending_policy :
    policy_is_numeric_FP_ascending (numeric_fp_ascending Task).

The resulting priority policy is reflexive.
  Fact NFPA_is_reflexive :
    reflexive_task_priorities (numeric_fp_ascending Task).

The resulting priority policy is transitive.
  Fact NFPA_is_transitive :
    transitive_task_priorities (numeric_fp_ascending Task).

The resulting priority policy is total.
  Fact NFPA_is_total :
    total_task_priorities (numeric_fp_ascending Task).

End PropertiesNFPA.

Next, we define descending numeric fixed priorities, where a larger numeric value indicates lower priority, and again note some trivial facts about this alternate interpretation of priority values.
Section PropertiesNFPD.

The instance numeric_fp_descending assigns lower priority to tasks with higher numeric task_priority value.
  #[local] Instance numeric_fp_descending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
  {
    hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≤ task_priority tsk2
  }.

Consider any kind of tasks with specified priorities.
  Context {Task : TaskType} `{TaskPriority Task}.

The concrete numeric_fp_descending implementation is indeed a descending numeric FP policy.
  Fact NFPD_is_numeric_FP_descending_policy :
    policy_is_numeric_FP_descending (numeric_fp_descending Task).

The resulting priority policy is reflexive.
  Fact NFPD_is_reflexive :
    reflexive_task_priorities (numeric_fp_descending Task).

The resulting priority policy is transitive.
  Fact NFPD_is_transitive :
    transitive_task_priorities (numeric_fp_descending Task).

The resulting priority policy is total.
  Fact NFPD_is_total :
    total_task_priorities (numeric_fp_descending Task).

End PropertiesNFPD.

We add the above facts into the basic_rt_facts hint database so Coq can apply them automatically where needed.
Global Hint Resolve
  NFPA_is_numeric_FP_ascending_policy
  NFPA_is_reflexive
  NFPA_is_transitive
  NFPA_is_total
  NFPD_is_numeric_FP_descending_policy
  NFPD_is_reflexive
  NFPD_is_transitive
  NFPD_is_total
  : basic_rt_facts.