fix dependency of basic readiness model on analysis facts

Move proof of readiness model property to analysis module.

restructuring/analysis/edf/optimality.v

@@ -8,10 +8,10 @@ Require Import rt.restructuring.analysis.transform.facts.edf_opt.
     schedule in which all deadlines are met. *)
 
 (** The following results assume ideal uniprocessor schedules... *)
-From rt.restructuring.model.processor Require ideal.
+Require rt.restructuring.model.processor.ideal.
 (** ... and the basic (i.e., Liu & Layland) readiness model under which any
     pending job is ready. *)
-From rt.restructuring.model.readiness Require basic.
+Require rt.restructuring.model.readiness.basic.
 
 Section Optimality.
   (** For any given type of jobs... *)

restructuring/analysis/facts/readiness/basic.v

+Require Export rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.analysis.basic_facts.completion.
+
+Section LiuAndLaylandReadiness.
+  (** Consider any kind of jobs... *)
+  Context {Job : JobType}.
+
+  (** ... and any kind of processor state. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Supose jobs have an arrival time and a cost. *)
+  Context `{JobArrival Job} `{JobCost Job}.
+
+  (** In the basic Liu & Layland model, a schedule satisfies that only ready 
+      jobs execute as long as jobs must arrive to execute and completed jobs
+      don't execute, which we note with the following theorem. *)
+  Lemma basic_readiness_compliance:
+    forall sched,
+      jobs_must_arrive_to_execute sched ->
+      completed_jobs_dont_execute sched ->
+      jobs_must_be_ready_to_execute sched.
+  Proof.
+    move=> sched ARR COMP.
+    rewrite /jobs_must_be_ready_to_execute =>  j t SCHED.
+    rewrite /job_ready /basic_ready_instance /pending.
+    apply /andP; split.
+    - by apply ARR.
+    - rewrite -less_service_than_cost_is_incomplete.
+      by apply COMP.
+  Qed.
+
+End LiuAndLaylandReadiness.

restructuring/analysis/transform/facts/edf_opt.v

@@ -4,6 +4,7 @@ Require Export rt.restructuring.model.schedule.edf.
 Require Export rt.restructuring.analysis.schedulability.
 Require Export rt.restructuring.analysis.transform.edf_trans.
 Require Export rt.restructuring.analysis.transform.facts.swaps.
+Require Export rt.restructuring.analysis.facts.readiness.basic.
 
 Require Import rt.util.tactics.
 Require Import rt.util.nat.

restructuring/model/readiness/basic.v

 Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.completion.
 
 (** We define the readiness indicator function for the classic Liu & Layland
    model without jitter and no self-suspensions, where jobs are always
@@ -22,24 +21,5 @@ Section LiuAndLaylandReadiness.
       job_ready sched j t := pending sched j t
     }.
 
-
-  (** Under this definition, a schedule satisfies that only ready jobs execute
-     as long as jobs must arrive to execute and completed jobs don't execute,
-     which we note with the following theorem. *)
-  Theorem basic_readiness_compliance:
-    forall sched,
-      jobs_must_arrive_to_execute sched ->
-      completed_jobs_dont_execute sched ->
-      jobs_must_be_ready_to_execute sched.
-  Proof.
-    move=> sched ARR COMP.
-    rewrite /jobs_must_be_ready_to_execute =>  j t SCHED.
-    rewrite /job_ready /basic_ready_instance /pending.
-    apply /andP; split.
-    - by apply ARR.
-    - rewrite -less_service_than_cost_is_incomplete.
-      by apply COMP.
-  Qed.
-
 End LiuAndLaylandReadiness.