From 1306c75c88883b3ffca7e94bc310971ff3a6c0a9 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:47:16 +0100
Subject: [PATCH] model reorg: flatten model.preemption

---
 restructuring/analysis/basic_facts/preemption/job/limited.v     | 2 +-
 .../analysis/basic_facts/preemption/job/nonpreemptive.v         | 2 +-
 restructuring/analysis/basic_facts/preemption/job/preemptive.v  | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/floating.v    | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/limited.v     | 2 +-
 .../basic_facts/preemption/rtc_threshold/nonpreemptive.v        | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/preemptive.v  | 2 +-
 restructuring/analysis/basic_facts/preemption/task/floating.v   | 2 +-
 restructuring/analysis/basic_facts/preemption/task/limited.v    | 2 +-
 .../analysis/basic_facts/preemption/task/nonpreemptive.v        | 2 +-
 restructuring/analysis/basic_facts/preemption/task/preemptive.v | 2 +-
 .../{job/instance/nonpreemptive.v => fully_nonpreemptive.v}     | 0
 .../{job/instance/preemptive.v => fully_preemptive.v}           | 0
 .../preemption/{job/instance/limited.v => limited_preemptive.v} | 0
 restructuring/model/task/preemption/floating_nonpreemptive.v    | 2 +-
 restructuring/model/task/preemption/limited_preemptive.v        | 2 +-
 16 files changed, 13 insertions(+), 13 deletions(-)
 rename restructuring/model/preemption/{job/instance/nonpreemptive.v => fully_nonpreemptive.v} (100%)
 rename restructuring/model/preemption/{job/instance/preemptive.v => fully_preemptive.v} (100%)
 rename restructuring/model/preemption/{job/instance/limited.v => limited_preemptive.v} (100%)

diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 8a9eef37b..bde0d0fc0 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.schedule.limited_preemptive.
 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.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index 42fa25ea3..06493bcc5 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 
 Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index e09ef19d5..53852d2d8 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.job.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 
 (** * Preemptions in Fully Premptive Model *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index f9c02c130..afae13c18 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 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.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 9a7f2c99c..72e2dd088 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 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.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 2f1f3584a..6f7f0d265 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.parameter.
 Require Import rt.restructuring.model.task.preemption.parameters.
 
-Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 4c2d58e60..3bbbd6e62 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.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.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 2fca1a499..d00940655 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 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.preemption.limited_preemptive.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 20b7e7395..17f9ba3d2 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
 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.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index 7646eed4c..d9d3235e4 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -5,7 +5,7 @@ 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.job.instance.nonpreemptive.
+Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
 
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index a32ac7b2a..7fbbc1952 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.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.instance.preemptive.
+Require Import rt.restructuring.model.preemption.fully_preemptive.
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
 
diff --git a/restructuring/model/preemption/job/instance/nonpreemptive.v b/restructuring/model/preemption/fully_nonpreemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/nonpreemptive.v
rename to restructuring/model/preemption/fully_nonpreemptive.v
diff --git a/restructuring/model/preemption/job/instance/preemptive.v b/restructuring/model/preemption/fully_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/preemptive.v
rename to restructuring/model/preemption/fully_preemptive.v
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/limited_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/job/instance/limited.v
rename to restructuring/model/preemption/limited_preemptive.v
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 61eff9396..d0e75b0ac 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.instance.limited.
+Require Export rt.restructuring.model.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 194ceb278..343a6db76 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.job.instance.limited.
+Require Export rt.restructuring.model.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
-- 
GitLab