modify definitions of priority policy compliance

The current definitions of `respects_JLFP_policy_at_preemption_time`
and `respects_FP_policy_at_preemption_time` use the predicate
`hep_job_at`. This predicate does not make sense for `JLFP`
and `FP` policies. To avoid this, these definitions should
instead use the definition `respects_JLDP_policy_at_preemption_point`.
Doing this requires coercions from `JLFP` to `JLDP` and from
`FP` to `JLFP`. This patch also introduces these coercions.

model/priority/classes.v

@@ -49,6 +49,11 @@ Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
 Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=
   fun _ j1 j2 => hep_job j1 j2.
 
+(** We add coercions to enable automatic conversion from [JLFP] to [JLDP]... *)
+Coercion JLFP_to_JLDP : JLFP_policy >-> JLDP_policy.
+(** ...and from [FP] to [JLFP]. *)
+Coercion FP_to_JLFP : FP_policy >-> JLFP_policy.
+
 (** ** Properties of Priority Policies *)
 
 (** In the following section, we define key properties of common priority

model/schedule/priority_driven.v

@@ -46,22 +46,14 @@ Section Priority.
       preemption_time sched t ->
       backlogged sched j t ->
       scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j. 
+      hep_job_at t j_hp j.
+  
    (** ... [JLFP], and... *)
   Definition respects_JLFP_policy_at_preemption_point (policy: JLFP_policy Job) :=
-    forall j j_hp t,
-      arrives_in arr_seq j ->
-      preemption_time sched t ->
-      backlogged sched j t ->
-      scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j.
+    respects_JLDP_policy_at_preemption_point policy.
+     
   (** [FP].  *)
   Definition respects_FP_policy_at_preemption_point (policy: FP_policy Task) :=
-    forall j j_hp t,
-      arrives_in arr_seq j ->
-      preemption_time sched t ->
-      backlogged sched j t ->
-      scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j.
+    respects_JLDP_policy_at_preemption_point (FP_to_JLFP Job Task ).
 
 End Priority.

scripts/wordlist.pws

@@ -77,3 +77,4 @@ et
 al
 discoverable
 formedness
+coercions