From 4d5c9497f4964f26119689ad3deb8774dbc6474c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 20:26:21 +0100
Subject: [PATCH] model reorg: merge job_preemptable def and validity

---
 .../analysis/abstract/core/abstract_rta.v     |  4 +-
 .../analysis/abstract/core/abstract_seq_rta.v |  4 +-
 ...ondition_for_run_to_completion_threshold.v |  4 +-
 .../basic_facts/preemption/job/limited.v      | 20 +++---
 .../preemption/job/nonpreemptive.v            |  4 +-
 .../basic_facts/preemption/job/preemptive.v   |  4 +-
 .../preemption/rtc_threshold/floating.v       |  2 +-
 .../rtc_threshold/job_preemptable.v           |  4 +-
 .../preemption/rtc_threshold/limited.v        |  2 +-
 .../preemption/rtc_threshold/nonpreemptive.v  |  4 +-
 .../basic_facts/preemption/task/floating.v    |  6 +-
 .../basic_facts/preemption/task/limited.v     |  6 +-
 .../basic_facts/preemption/task/preemptive.v  |  2 +-
 .../edf/rta/nonpr_reg/response_time_bound.v   |  4 +-
 .../analysis/edf/rta/response_time_bound.v    |  4 +-
 .../facts/priority_inversion_is_bounded.v     |  4 +-
 .../rta/nonpr_reg/response_time_bound.v       |  4 +-
 .../fixed_priority/rta/response_time_bound.v  |  4 +-
 .../model/preemption/job/instance/limited.v   |  2 +-
 .../preemption/job/instance/nonpreemptive.v   |  2 +-
 .../preemption/job/instance/preemptive.v      |  2 +-
 .../{job/parameters.v => parameter.v}         | 66 ++++++++++++++++++
 restructuring/model/preemption/valid_model.v  | 67 -------------------
 .../model/schedule/limited_preemptive.v       |  2 +-
 .../model/schedule/preemption_time.v          |  2 +-
 .../model/task/preemption/parameters.v        |  3 +-
 26 files changed, 115 insertions(+), 117 deletions(-)
 rename restructuring/model/preemption/{job/parameters.v => parameter.v} (55%)
 delete mode 100644 restructuring/model/preemption/valid_model.v

diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 03df8f5ac..3283abbd5 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -2,8 +2,8 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 350c71c37..6f07e8297 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -3,8 +3,8 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.arrival.arrival_curves.
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index 00a4644ac..95e11dde6 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -3,8 +3,8 @@ Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.abstract.core.definitions.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 255cd93ca..8a9eef37b 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -3,9 +3,9 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
@@ -164,36 +164,36 @@ Section ModelWithLimitedPreemptions.
 
     (** Recall that file [job.parameters] also defines notion of
         preemption poins.  And note that
-        [job.parameters.job_preemption_points] cannot have a
+        [job.parameter.job_preemption_points] cannot have a
         duplicating preemption points. Therefore, we need additional
-        lemmas to relate [job.parameters.job_preemption_points] and
+        lemmas to relate [job.parameter.job_preemption_points] and
         [limited.job_preemption_points]]. *)
 
     (** First we show that the length of the last non-preemptive
-        segment of [job.parameters.job_preemption_points] is equal to
+        segment of [job.parameter.job_preemption_points] is equal to
         the length of the last non-empty non-preemptive segment of
         [limited.job_preemption_points]. *)
     Lemma job_parameters_last_np_to_job_limited:
-        last0 (distances (parameters.job_preemption_points j)) =
+        last0 (distances (parameter.job_preemption_points j)) =
         last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
       intros; rewrite distances_iota_filtered; eauto.
       rewrite -A2 //.
         by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
     Qed.
 
     (** Next we show that the length of the max non-preemptive
-        segment of [job.parameters.job_preemption_points] is equal to
+        segment of [job.parameter.job_preemption_points] is equal to
         the length of the max non-preemptive segment of
         [limited.job_preemption_points]. *)
     Lemma job_parameters_max_np_to_job_limited:
-      max0 (distances (parameters.job_preemption_points j)) =
+      max0 (distances (parameter.job_preemption_points j)) =
       max0 (distances (job_preemption_points j)).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
       intros; rewrite distances_iota_filtered; eauto 2.
       rewrite max0_rem0 //.
       rewrite -A2 //.
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index efaaf78a2..42fa25ea3 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -4,8 +4,8 @@ Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 1392a0cfb..e09ef19d5 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index e3e91e0cf..f9c02c130 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
index f446e860d..099296ceb 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -2,8 +2,8 @@ Require Import rt.util.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index cebdf4816..9a7f2c99c 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 
 Require Import rt.restructuring.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index b90c5e803..2f1f3584a 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -3,8 +3,8 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index fd6ad2ea1..2fca1a499 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.preemption.job.instance.limited.
@@ -68,7 +68,7 @@ Section FloatingNonPremptiveRegionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
       rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index e51e4269d..20b7e7395 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -3,8 +3,8 @@ Require Import rt.util.nondecreasing.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
@@ -66,7 +66,7 @@ Section LimitedPreemptionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
       rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index c9ea62b66..a32ac7b2a 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.valid_model.
+
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index 961efe2fb..bbcc09196 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 3f5bec3e2..481eba533 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -8,8 +8,8 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index ad9688c9f..c0b7ad091 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.model.preemption.valid_model.
+
 Require Import rt.restructuring.model.schedule.preemption_time.
-Require Import rt.restructuring.model.preemption.job.parameters.
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 48361205f..0797d23a7 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 7d97db5a0..3ca80c5bf 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -7,8 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.job.parameters.
+
+Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/job/instance/limited.v
index 8b631a17f..d4345918c 100644
--- a/restructuring/model/preemption/job/instance/limited.v
+++ b/restructuring/model/preemption/job/instance/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** Definition of a parameter relating a job
diff --git a/restructuring/model/preemption/job/instance/nonpreemptive.v b/restructuring/model/preemption/job/instance/nonpreemptive.v
index 804d5e3fc..95f900017 100644
--- a/restructuring/model/preemption/job/instance/nonpreemptive.v
+++ b/restructuring/model/preemption/job/instance/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 
 (** * Platform for Fully Non-Preemptive Model *)
 (** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/job/instance/preemptive.v b/restructuring/model/preemption/job/instance/preemptive.v
index 6febcfda7..9f8e026d8 100644
--- a/restructuring/model/preemption/job/instance/preemptive.v
+++ b/restructuring/model/preemption/job/instance/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
 
 (** * Platform for Fully Premptive Model *)
 (** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/job/parameters.v b/restructuring/model/preemption/parameter.v
similarity index 55%
rename from restructuring/model/preemption/job/parameters.v
rename to restructuring/model/preemption/parameter.v
index 9ce2edafa..20a26f083 100644
--- a/restructuring/model/preemption/job/parameters.v
+++ b/restructuring/model/preemption/parameter.v
@@ -74,3 +74,69 @@ Section MaxAndLastNonpreemptiveSegment.
     job_cost j - (job_last_nonpreemptive_segment j - ε).
   
 End MaxAndLastNonpreemptiveSegment. 
+
+(** * Platform with limited preemptions *)
+(** In the follwoing, we define properties that any reasonable job preemption
+    model must satisfy. *)
+Section PreemptionModel.
+
+  (**  Consider any type of jobs... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... and the existence of a predicate mapping a job and
+      its progress to a boolean value saying whether this job is
+      preemptable at its current point of execution. *)
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of processor state model, ... *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** ... any job arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any given schedule. *)
+  Variable sched : schedule PState.
+
+  (** In this section, we define the notion of a valid preemption model. *)
+  Section ValidPreemptionModel.
+
+    (** We require that a job has to be executed at least one time
+        instant in order to reach a nonpreemptive segment. In other
+        words, a job must start execution to become non-preemptive. *)
+    Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
+      job_preemptable j 0.
+
+    (** And vice versa, a job cannot remain non-preemptive after its completion. *)
+    Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
+      job_preemptable j (job_cost j).
+
+    (** Next, if a job j is not preemptive at some time instant t,
+        then j must be scheduled at time t. *)
+    Definition not_preemptive_implies_scheduled (j : Job) :=
+      forall t,
+        ~~ job_preemptable j (service sched j t) ->
+        scheduled_at sched j t.
+
+    (** A job can start its execution only from a preemption point. *)
+    Definition execution_starts_with_preemption_point (j : Job) :=
+      forall prt,
+        ~~ scheduled_at sched j prt ->
+        scheduled_at sched j prt.+1 ->
+        job_preemptable j (service sched j prt.+1).
+
+    (** We say that a preemption model is a valid preemption model if
+       all the assumptions given above are satisfied for any job. *)
+    Definition valid_preemption_model :=
+      forall j,
+        arrives_in arr_seq j ->
+        job_cannot_become_nonpreemptive_before_execution j
+        /\ job_cannot_be_nonpreemptive_after_completion j
+        /\ not_preemptive_implies_scheduled j
+        /\ execution_starts_with_preemption_point j.
+
+  End ValidPreemptionModel.
+
+End PreemptionModel.
diff --git a/restructuring/model/preemption/valid_model.v b/restructuring/model/preemption/valid_model.v
deleted file mode 100644
index 38ae8fb60..000000000
--- a/restructuring/model/preemption/valid_model.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Export rt.restructuring.model.preemption.job.parameters.
-
-(** * Platform with limited preemptions *)
-(** In the follwoing, we define properties that any reasonable job preemption
-    model must satisfy. *)
-Section PreemptionModel.
-
-  (**  Consider any type of jobs... *)
-  Context {Job : JobType}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-
-  (** ... and the existence of a predicate mapping a job and
-      its progress to a boolean value saying whether this job is
-      preemptable at its current point of execution. *)
-  Context `{JobPreemptable Job}.
-
-  (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  (** ... any job arrival sequence, ... *)
-  Variable arr_seq : arrival_sequence Job.
-
-  (** ... and any given schedule. *)
-  Variable sched : schedule PState.
-
-  (** In this section, we define the notion of a valid preemption model. *)
-  Section ValidPreemptionModel.
-
-    (** We require that a job has to be executed at least one time
-        instant in order to reach a nonpreemptive segment. In other
-        words, a job must start execution to become non-preemptive. *)
-    Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
-      job_preemptable j 0.
-
-    (** And vice versa, a job cannot remain non-preemptive after its completion. *)
-    Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
-      job_preemptable j (job_cost j).
-
-    (** Next, if a job j is not preemptive at some time instant t,
-        then j must be scheduled at time t. *)
-    Definition not_preemptive_implies_scheduled (j : Job) :=
-      forall t,
-        ~~ job_preemptable j (service sched j t) ->
-        scheduled_at sched j t.
-
-    (** A job can start its execution only from a preemption point. *)
-    Definition execution_starts_with_preemption_point (j : Job) :=
-      forall prt,
-        ~~ scheduled_at sched j prt ->
-        scheduled_at sched j prt.+1 ->
-        job_preemptable j (service sched j prt.+1).
-
-    (** We say that a preemption model is a valid preemption model if
-       all the assumptions given above are satisfied for any job. *)
-    Definition valid_preemption_model :=
-      forall j,
-        arrives_in arr_seq j ->
-        job_cannot_become_nonpreemptive_before_execution j
-        /\ job_cannot_be_nonpreemptive_after_completion j
-        /\ not_preemptive_implies_scheduled j
-        /\ execution_starts_with_preemption_point j.
-
-  End ValidPreemptionModel.
-
-End PreemptionModel.
diff --git a/restructuring/model/schedule/limited_preemptive.v b/restructuring/model/schedule/limited_preemptive.v
index 1a96bfbbb..2cc39396f 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/restructuring/model/schedule/limited_preemptive.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.parameter.
  
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/schedule/preemption_time.v b/restructuring/model/schedule/preemption_time.v
index e355941a7..790fd66f7 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/restructuring/model/schedule/preemption_time.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.preemption.parameter.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Preemption Time in Ideal Uni-Processor Model *)
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index 686f863e2..78ce49044 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -1,6 +1,5 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.preemption.parameter.
 Require Export rt.restructuring.model.task.concept.
 (** * Static information about preemption points *)
 
-- 
GitLab