disambiguate `fully_preemptive_job_model`

analysis/facts/edf_definitions.v

@@ -35,7 +35,7 @@ Section Equivalence.
   #[local] Existing Instance basic_ready_instance.
 
   (** We assume that jobs are fully preemptive. *)
-  #[local] Existing Instance fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
 
   (** For any given type of jobs, each characterized by an arrival time,
       an execution cost, and an absolute deadline, ... *)

analysis/facts/preemption/job/preemptive.v

 Require Export prosa.model.task.preemption.parameters.
-Require Import prosa.model.preemption.fully_preemptive.
+Require Export prosa.model.preemption.fully_preemptive.
 
 (** * Preemptions in Fully Preemptive Model *)
 (** In this section, we prove that instantiation of predicate
@@ -8,7 +8,7 @@ Require Import prosa.model.preemption.fully_preemptive.
 Section FullyPreemptiveModel.
 
   (** We assume that jobs are fully preemptive. *)
-  #[local] Existing Instance fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
 
   (**  Consider any type of jobs. *)
   Context {Job : JobType}.
@@ -54,7 +54,7 @@ Section FullyPreemptiveModel.
     intros ? POS.
     rewrite /job_max_nonpreemptive_segment /lengths_of_segments
             /job_preemption_points.
-    rewrite /job_preemptable /fully_preemptive_model.
+    rewrite /job_preemptable /fully_preemptive_job_model.
     rewrite filter_predT.
     apply max0_of_uniform_set.
     - rewrite /range /index_iota subn0.

analysis/facts/preemption/rtc_threshold/preemptive.v

@@ -10,8 +10,7 @@ Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
 Section TaskRTCThresholdFullyPreemptiveModel.
 
   (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance
-    model.preemption.fully_preemptive.fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
   #[local] Existing Instance fully_preemptive_task_model.
   #[local] Existing Instance fully_preemptive_rtc_threshold.
 

analysis/facts/preemption/task/preemptive.v

@@ -10,8 +10,7 @@ Require Import prosa.model.task.preemption.fully_preemptive.
 Section FullyPreemptiveModel.
 
   (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance
-    model.preemption.fully_preemptive.fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
   #[local] Existing Instance fully_preemptive_task_model.
   #[local] Existing Instance fully_preemptive_rtc_threshold.
 

model/preemption/fully_preemptive.v

@@ -10,7 +10,9 @@ Section FullyPreemptiveModel.
   Context {Job : JobType}.
 
   (** In the fully preemptive model, any job can be preempted at any time. *)
-  Definition fully_preemptive_model : JobPreemptable Job :=
-    fun (_ : Job) (_ : work) => true.
+  #[local] Instance fully_preemptive_job_model : JobPreemptable Job :=
+  {
+    job_preemptable (_ : Job) (_ : work) := true
+  }.
 
 End FullyPreemptiveModel.

results/edf/optimality.v

@@ -24,7 +24,7 @@ Section Optimality.
   #[local] Existing Instance basic_ready_instance.
 
   (** We assume that jobs are fully preemptive. *)
-  #[local] Existing Instance fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
 
   (** For any given type of jobs, each characterized by execution
       costs, an arrival time, and an absolute deadline,... *)

results/edf/rta/fully_preemptive.v

@@ -23,8 +23,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   #[local] Existing Instance basic_ready_instance.
 
   (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance
-    model.preemption.fully_preemptive.fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
   #[local] Existing Instance fully_preemptive_task_model.
   #[local] Existing Instance fully_preemptive_rtc_threshold.
 

results/fixed_priority/rta/fully_preemptive.v

@@ -21,8 +21,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   #[local] Existing Instance ideal.processor_state.
 
   (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance
-    model.preemption.fully_preemptive.fully_preemptive_model.
+  #[local] Existing Instance fully_preemptive_job_model.
   #[local] Existing Instance fully_preemptive_task_model.
   #[local] Existing Instance fully_preemptive_rtc_threshold.