From 9c7b4f3008ed572aa2237cfc7832f5cb478c3a28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 18:13:28 +0100
Subject: [PATCH] model reorg: move task preemption parameters to
 model.task.preemption

---
 restructuring/analysis/abstract/core/abstract_rta.v             | 2 +-
 restructuring/analysis/abstract/core/abstract_seq_rta.v         | 2 +-
 restructuring/analysis/basic_facts/preemption/job/limited.v     | 2 +-
 restructuring/analysis/basic_facts/preemption/job/preemptive.v  | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/floating.v    | 2 +-
 .../basic_facts/preemption/rtc_threshold/job_preemptable.v      | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/limited.v     | 2 +-
 .../basic_facts/preemption/rtc_threshold/nonpreemptive.v        | 2 +-
 restructuring/analysis/basic_facts/preemption/task/floating.v   | 2 +-
 restructuring/analysis/basic_facts/preemption/task/limited.v    | 2 +-
 restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v  | 2 +-
 restructuring/analysis/edf/rta/response_time_bound.v            | 2 +-
 restructuring/analysis/facts/priority_inversion_is_bounded.v    | 2 +-
 .../analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v | 2 +-
 restructuring/analysis/fixed_priority/rta/response_time_bound.v | 2 +-
 restructuring/model/preemption/job/instance/limited.v           | 2 +-
 .../model/preemption/rtc_threshold/instance/floating.v          | 2 +-
 restructuring/model/preemption/rtc_threshold/instance/limited.v | 2 +-
 .../model/preemption/rtc_threshold/instance/nonpreemptive.v     | 2 +-
 .../model/preemption/rtc_threshold/instance/preemptive.v        | 2 +-
 restructuring/model/preemption/valid_model.v                    | 2 +-
 .../model/{preemption/task => task/preemption}/parameters.v     | 0
 22 files changed, 21 insertions(+), 21 deletions(-)
 rename restructuring/model/{preemption/task => task/preemption}/parameters.v (100%)

diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index fe5bd0e9e..68a2ebaa5 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -4,7 +4,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.schedulability.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index b28114eb0..425abc474 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+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/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index c10c94133..41f1276cf 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 912879604..1392a0cfb 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -2,7 +2,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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 
 (** * Preemptions in Fully Premptive Model *)
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index 31d9f7925..d7c2bcfd5 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -3,7 +3,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.floating.
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 63689bce1..f446e860d 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -4,7 +4,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
 (** In this section, we provide a few basic properties 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index f71f40c61..c31493878 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.
 Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 52153acc9..31307deb5 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -5,7 +5,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 Require Import rt.restructuring.model.preemption.task.instance.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 70284babe..535c7bcbd 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.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.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.valid_schedule.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 7aca2dc61..4851f4076 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/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.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.
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 ccb737e69..d24bcd4ed 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -9,7 +9,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 931ed0aa6..23f6787d0 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -10,7 +10,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index d552b4ec3..ad9688c9f 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -4,7 +4,7 @@ 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.task.parameters.
+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.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
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 85d7f7878..54e45fcc7 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
@@ -9,7 +9,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 18e460ccd..b80e1ae55 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -9,7 +9,7 @@ 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.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/job/instance/limited.v
index d6c3ce92c..8b631a17f 100644
--- a/restructuring/model/preemption/job/instance/limited.v
+++ b/restructuring/model/preemption/job/instance/limited.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** Definition of a parameter relating a job
     to the sequence of its preemption points. *)
diff --git a/restructuring/model/preemption/rtc_threshold/instance/floating.v b/restructuring/model/preemption/rtc_threshold/instance/floating.v
index 5197b1e42..4b87a208c 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/floating.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/floating.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/rtc_threshold/instance/limited.v b/restructuring/model/preemption/rtc_threshold/instance/limited.v
index c8aa1d8f6..14efa2870 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/limited.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
index cb323af10..271f11b4a 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
index cf32a1b91..30459d065 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/valid_model.v b/restructuring/model/preemption/valid_model.v
index 5a0299026..d57aa0543 100644
--- a/restructuring/model/preemption/valid_model.v
+++ b/restructuring/model/preemption/valid_model.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Platform with limited preemptions *)
 (** Since the notion of preemption points is based on an user-provided 
diff --git a/restructuring/model/preemption/task/parameters.v b/restructuring/model/task/preemption/parameters.v
similarity index 100%
rename from restructuring/model/preemption/task/parameters.v
rename to restructuring/model/task/preemption/parameters.v
-- 
GitLab