From a258c25238a73c097618232d93a2b54fa84c24dd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 16:41:34 +0100
Subject: [PATCH] model reorg: move priorities definition to own folder

---
 .../analysis/abstract/instantiations/ideal_processor.v          | 2 +-
 restructuring/analysis/arrival/workload_bound.v                 | 2 +-
 restructuring/analysis/basic_facts/service_of_jobs.v            | 2 +-
 restructuring/analysis/basic_facts/workload.v                   | 2 +-
 restructuring/analysis/definitions/priority_inversion.v         | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/floating.v       | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/limited.v        | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v  | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/preemptive.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/busy_interval_exists.v             | 2 +-
 restructuring/analysis/facts/no_carry_in_exists.v               | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/floating.v     | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/limited.v      | 2 +-
 .../rta/nonpr_reg/concrete_models/nonpreemptive.v               | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/preemptive.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/aggregate/service_of_jobs.v                 | 2 +-
 restructuring/model/aggregate/workload.v                        | 2 +-
 .../priority_based/priorities.v => priority/classes.v}          | 0
 restructuring/model/schedule/priority_based/edf.v               | 2 +-
 restructuring/model/schedule/priority_based/preemption_aware.v  | 2 +-
 restructuring/model/schedule/priority_based/preemptive.v        | 2 +-
 25 files changed, 24 insertions(+), 24 deletions(-)
 rename restructuring/model/{schedule/priority_based/priorities.v => priority/classes.v} (100%)

diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index e57014b41..69f89f25e 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -3,7 +3,7 @@ Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.schedule.sequential.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.definitions.busy_interval.
 Require Import rt.restructuring.analysis.definitions.priority_inversion.
 Require Import rt.restructuring.analysis.abstract.core.definitions.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 70798f72d..bdb5ba43e 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,7 +1,7 @@
 Require Import rt.util.sum.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.model.task.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.analysis.basic_facts.workload.
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 20f607065..93741e6f1 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -6,7 +6,7 @@ Require Export rt.restructuring.model.aggregate.workload.
 Require Export rt.restructuring.model.aggregate.service_of_jobs.
 Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.restructuring.model.processor.platform_properties.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 Require Import rt.restructuring.analysis.basic_facts.service.
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/basic_facts/workload.v
index a049cb004..67c71814b 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/basic_facts/workload.v
@@ -1,6 +1,6 @@
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index f0367af97..076db9e09 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 5185299fa..d5497e73b 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 46937e75f..0db53dbef 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index c8d39e1e0..8212144b8 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -8,7 +8,7 @@ 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.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 8a73acd95..04a01e3c4 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -8,7 +8,7 @@ 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.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
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 b6c66b81d..d266393a6 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -14,7 +14,7 @@ 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.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index f64d965fe..0fbb317ab 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -14,7 +14,7 @@ Require Import rt.restructuring.model.preemption.task.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.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 0dfdaa5b9..4a402cc05 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
 
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 478de7349..b7aa4490f 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 9fa2cb467..3f15c28b0 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index ecf26b2d2..fe73e59a1 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index fd36a8f6a..78c93cd06 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -8,7 +8,7 @@ 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.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 80b08a0f0..565952da9 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -8,7 +8,7 @@ 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.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
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 d96346587..1b91e8ccf 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
@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index d086e8082..b1ed59948 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 2fdd41a5a..0d6af1276 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.model.processor.ideal.
      
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index f7e0b2093..9040dbbcb 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/schedule/priority_based/priorities.v b/restructuring/model/priority/classes.v
similarity index 100%
rename from restructuring/model/schedule/priority_based/priorities.v
rename to restructuring/model/priority/classes.v
diff --git a/restructuring/model/schedule/priority_based/edf.v b/restructuring/model/schedule/priority_based/edf.v
index daaf6ce3f..17a8c2590 100644
--- a/restructuring/model/schedule/priority_based/edf.v
+++ b/restructuring/model/schedule/priority_based/edf.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.job_deadline.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 From mathcomp Require Export seq.
 
 (** In this section we introduce the notion of EDF priorities. *)
diff --git a/restructuring/model/schedule/priority_based/preemption_aware.v b/restructuring/model/schedule/priority_based/preemption_aware.v
index 3918c457d..59e8b33d3 100644
--- a/restructuring/model/schedule/priority_based/preemption_aware.v
+++ b/restructuring/model/schedule/priority_based/preemption_aware.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.model.preemption.preemption_time.
 
 (** We now define what it means for a schedule to respect a priority
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index fda859922..d41123a36 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 
 (** We now define what it means for a schedule to respect a priority *)
 (** We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
-- 
GitLab