From 572c699b62acd357e23b276c205d30cc74ca0220 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:31:38 +0100
Subject: [PATCH] model reorg: move preemption.valid_schedule ->
schedule.limited_preemptive
All "kinds of schedules" and associated validity conditions are being
collected in model.schedule.
---
restructuring/analysis/basic_facts/preemption/job/limited.v | 2 +-
.../analysis/basic_facts/preemption/rtc_threshold/limited.v | 2 +-
restructuring/analysis/basic_facts/preemption/task/floating.v | 2 +-
restructuring/analysis/basic_facts/preemption/task/limited.v | 2 +-
restructuring/model/preemption/floating.v | 2 +-
restructuring/model/preemption/limited.v | 2 +-
restructuring/model/preemption/nonpreemptive.v | 2 +-
restructuring/model/preemption/preemptive.v | 2 +-
.../valid_schedule.v => schedule/limited_preemptive.v} | 0
9 files changed, 8 insertions(+), 8 deletions(-)
rename restructuring/model/{preemption/valid_schedule.v => schedule/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 41f1276cf..4a4e11d94 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -4,7 +4,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.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 548a8b375..4a4f9f54a 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.behavior.schedule.
Require Import rt.restructuring.analysis.definitions.job_properties.
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.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.parameters.
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/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 32cb214d3..9a918e50a 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.preemption.job.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.
+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 58c4e7fc0..e51e4269d 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/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.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.valid_schedule.
+Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
diff --git a/restructuring/model/preemption/floating.v b/restructuring/model/preemption/floating.v
index a1e3a8fe9..a44335562 100644
--- a/restructuring/model/preemption/floating.v
+++ b/restructuring/model/preemption/floating.v
@@ -1,4 +1,4 @@
Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
diff --git a/restructuring/model/preemption/limited.v b/restructuring/model/preemption/limited.v
index ba3d31790..fad9bf13e 100644
--- a/restructuring/model/preemption/limited.v
+++ b/restructuring/model/preemption/limited.v
@@ -1,4 +1,4 @@
Require Export rt.restructuring.model.preemption.valid_model.
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.limited_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
diff --git a/restructuring/model/preemption/nonpreemptive.v b/restructuring/model/preemption/nonpreemptive.v
index 026c58041..b213f9636 100644
--- a/restructuring/model/preemption/nonpreemptive.v
+++ b/restructuring/model/preemption/nonpreemptive.v
@@ -1,6 +1,6 @@
Require Export rt.restructuring.model.schedule.nonpreemptive.
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
diff --git a/restructuring/model/preemption/preemptive.v b/restructuring/model/preemption/preemptive.v
index 872abdd18..4a081def8 100644
--- a/restructuring/model/preemption/preemptive.v
+++ b/restructuring/model/preemption/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.valid_schedule.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.fully_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
diff --git a/restructuring/model/preemption/valid_schedule.v b/restructuring/model/schedule/limited_preemptive.v
similarity index 100%
rename from restructuring/model/preemption/valid_schedule.v
rename to restructuring/model/schedule/limited_preemptive.v
--
GitLab