From 390228e8a41fe92b279f507a6b9f5abad9638afc Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 23 Nov 2019 15:06:42 +0100
Subject: [PATCH] remove unneeded 'Require' statement in analysis spec
---
.../analysis/abstract/core/abstract_rta.v | 17 ++--------
.../analysis/abstract/core/abstract_seq_rta.v | 29 +++--------------
.../analysis/abstract/core/definitions.v | 6 ++--
...ondition_for_run_to_completion_threshold.v | 11 ++-----
.../abstract/instantiations/ideal_processor.v | 13 ++------
restructuring/analysis/arrival/rbf.v | 9 ++----
.../analysis/arrival/workload_bound.v | 12 ++-----
.../analysis/basic_facts/completion.v | 3 --
.../analysis/basic_facts/deadlines.v | 2 --
.../analysis/basic_facts/ideal_schedule.v | 5 ++-
.../basic_facts/preemption/job/limited.v | 16 +++-------
.../preemption/job/nonpreemptive.v | 11 ++-----
.../basic_facts/preemption/job/preemptive.v | 6 +---
.../preemption/rtc_threshold/floating.v | 12 ++-----
.../rtc_threshold/job_preemptable.v | 10 ++----
.../preemption/rtc_threshold/limited.v | 13 ++------
.../preemption/rtc_threshold/nonpreemptive.v | 10 +-----
.../preemption/rtc_threshold/preemptive.v | 5 ---
.../basic_facts/preemption/task/floating.v | 11 +------
.../basic_facts/preemption/task/limited.v | 10 +-----
.../preemption/task/nonpreemptive.v | 8 +----
.../basic_facts/preemption/task/preemptive.v | 8 ++---
restructuring/analysis/basic_facts/service.v | 10 ++----
.../analysis/basic_facts/service_of_jobs.v | 15 ++-------
restructuring/analysis/basic_facts/workload.v | 4 +--
.../analysis/definitions/busy_interval.v | 11 +++----
.../analysis/definitions/no_carry_in.v | 12 +++----
.../analysis/definitions/priority_inversion.v | 7 ----
.../rta/nonpr_reg/concrete_models/floating.v | 23 ++-----------
.../rta/nonpr_reg/concrete_models/limited.v | 21 ++----------
.../nonpr_reg/concrete_models/nonpreemptive.v | 18 ++---------
.../nonpr_reg/concrete_models/preemptive.v | 15 +--------
.../edf/rta/nonpr_reg/response_time_bound.v | 24 +++-----------
.../analysis/edf/rta/response_time_bound.v | 32 +++----------------
.../analysis/facts/busy_interval_exists.v | 14 +++-----
.../analysis/facts/no_carry_in_exists.v | 16 +++-------
.../facts/priority_inversion_is_bounded.v | 14 ++------
.../rta/nonpr_reg/concrete_models/floating.v | 25 ++++-----------
.../rta/nonpr_reg/concrete_models/limited.v | 24 ++++----------
.../nonpr_reg/concrete_models/nonpreemptive.v | 26 ++++-----------
.../nonpr_reg/concrete_models/preemptive.v | 19 ++---------
.../rta/nonpr_reg/response_time_bound.v | 26 +++++----------
.../fixed_priority/rta/response_time_bound.v | 30 ++++-------------
.../analysis/transform/facts/swaps.v | 3 --
.../model/aggregate/service_of_jobs.v | 4 ++-
.../task/preemption/floating_nonpreemptive.v | 2 +-
46 files changed, 135 insertions(+), 487 deletions(-)
diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 3283abbd5..467bf8b6c 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,17 +1,6 @@
-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.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.analysis.schedulability.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Import rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
+Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.abstract.core.reduction_of_search_space.
+Require Export rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 6f07e8297..5cef87568 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,28 +1,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.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.
-
-Require Import rt.restructuring.model.task.sequentiality.
-Require Import rt.restructuring.analysis.schedulability.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Import rt.restructuring.analysis.basic_facts.workload.
-Require Import rt.restructuring.analysis.task_schedule.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.analysis.basic_facts.task_arrivals.
-
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Import rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
-Require Import rt.restructuring.analysis.abstract.core.abstract_rta.
+Require Export rt.restructuring.analysis.task_schedule.
+Require Export rt.restructuring.analysis.arrival.rbf.
+Require Export rt.restructuring.analysis.basic_facts.task_arrivals.
+Require Export rt.restructuring.analysis.abstract.core.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 22116f1dd..e0341070e 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,6 +1,6 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.concept.
+Require Export rt.restructuring.model.task.concept.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 95e11dde6..faf66a2b1 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
@@ -1,12 +1,5 @@
-Require Import rt.util.all.
-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.parameter.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.abstract.core.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index 6e2a74c49..f8bb00941 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -1,13 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.aggregate.workload.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.task.sequentiality.
-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.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
+Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.analysis.abstract.core.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** In this file we consider an ideal uni-processor ... *)
@@ -16,7 +8,6 @@ Require Import rt.restructuring.model.processor.ideal.
(** ... and classic model of readiness without jitter and no
self-suspensions, where pending jobs are always ready. *)
Require Import rt.restructuring.model.readiness.basic.
-
(** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
(** In this module we instantiate functions Interference and Interfering Workload
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index bde7b2ae1..e9c18f445 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,10 +1,5 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.aggregate.task_arrivals.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.arrival.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 07be1832e..98471fce2 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,12 +1,6 @@
-Require Import rt.util.sum.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.concept.
-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.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.workload.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.model.arrival.arrival_curves.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index d57646ad1..35d507ff8 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,9 +1,6 @@
-Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.service.
Require Export rt.restructuring.analysis.basic_facts.arrivals.
-Require Export rt.util.nat.
-
(** In this file, we establish basic facts about job completions. *)
Section CompletionFacts.
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 47163b68c..fb80bdae3 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,5 +1,3 @@
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.service.
Require Export rt.restructuring.analysis.basic_facts.completion.
(** In this file, we observe basic properties of the behavioral job
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
index 707b53a2b..4759a455b 100644
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ b/restructuring/analysis/basic_facts/ideal_schedule.v
@@ -1,6 +1,9 @@
From mathcomp Require Import all_ssreflect.
+Require Export rt.restructuring.model.processor.platform_properties.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.processor.platform_properties.
+
(** Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index bde0d0fc0..81e57d575 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -1,14 +1,8 @@
-Require Import rt.util.all.
-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.parameter.
-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.limited_preemptive.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.model.schedule.limited_preemptive.
+
+Require Export 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 06493bcc5..efa8ad2f5 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -1,14 +1,9 @@
-Require Import rt.util.all.
-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.schedule.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
-
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Preemptive model *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 53852d2d8..f5f56bdef 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -1,8 +1,4 @@
-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.all.
-
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.fully_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 afae13c18..4a2d046f7 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -1,15 +1,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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
-
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.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
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 099296ceb..8ea77ec19 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,10 +1,6 @@
-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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export 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 72e2dd088..f515e6358 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -1,17 +1,8 @@
-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.job.
-Require Import rt.restructuring.behavior.schedule.
-Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.concept.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-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.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.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 6f7f0d265..8875e0e6f 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,15 +1,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.schedule.nonpreemptive.
-
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 3bbbd6e62..25f5ab7fe 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -1,8 +1,3 @@
-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.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 d00940655..286e8d2e2 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -1,16 +1,7 @@
-Require Import rt.util.all.
-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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 17f9ba3d2..fb3661327 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -1,15 +1,7 @@
-Require Import rt.util.all.
-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 Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-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.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index d9d3235e4..717d7cdde 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -1,13 +1,7 @@
-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
-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.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index 7fbbc1952..1a33d34bb 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -1,11 +1,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 Export rt.restructuring.analysis.definitions.job_properties.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.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.
(** * Platform for Fully Premptive Model *)
(** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index a84571773..543fcdf4b 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -1,11 +1,7 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
-
-Require Export rt.restructuring.behavior.all.
+Require Export rt.util.all.
Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Export rt.restructuring.model.processor.platform_properties.
-Require Import rt.util.tactics.
-Require Import rt.util.step_function.
-Require Import rt.util.sum.
+
+From mathcomp Require Import ssrnat ssrbool fintype.
(** In this file, we establish basic facts about the service received by
jobs. *)
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 698a63177..2d10fa54b 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,17 +1,8 @@
-Require Import rt.util.all.
-
-Require Import rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.task.concept.
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.priority.classes.
-
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
-Require Import rt.restructuring.analysis.basic_facts.service.
-Require Import rt.restructuring.analysis.basic_facts.completion.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+
+Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/basic_facts/workload.v
index 67c71814b..942bd6582 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/basic_facts/workload.v
@@ -1,7 +1,5 @@
-Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index 0857ebc79..5a2edb38f 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -1,9 +1,8 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
+Require Export rt.restructuring.model.priority.classes.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index 2118f1c9f..f30d12ba1 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -1,8 +1,8 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.restructuring.model.priority.classes.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * No Carry-In *)
@@ -34,4 +34,4 @@ Section NoCarryIn.
arrived_before j_o t ->
completed_by sched j_o t.
-End NoCarryIn.
+End NoCarryIn.
\ No newline at end of file
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index 559b0a207..a868dba5c 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -1,10 +1,3 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-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 e111ffeb1..1d05d354e 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,26 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+
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.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
-
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 08df29bc1..5f3aafd52 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,24 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+
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.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 5449e5c8e..503ea76a0 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,25 +1,11 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+
+Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
(** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 c8d0f9157..338deb120 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,20 +1,7 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
+
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.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 bbcc09196..de5919d64 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -1,25 +1,9 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
+Require Export rt.restructuring.analysis.arrival.rbf.
+
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.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.analysis.facts.priority_inversion_is_bounded.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 481eba533..5d71602be 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -1,32 +1,10 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.facts.edf.
+Require Export rt.restructuring.model.schedule.priority_driven.
+Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
+Require Export rt.restructuring.analysis.schedulability.
+
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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.analysis.facts.edf.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.schedulability.
-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.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index d5600eb1d..3e0864478 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -1,16 +1,12 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.analysis.basic_facts.all.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
-(** Throughout the file we assume for the classic Liu & Layland model
- of readiness without jitter and no self-suspensions, where prending
- jobs are always ready. *)
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 196b6376c..1e9b85e35 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -1,18 +1,10 @@
-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-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.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-(** Throughout the file we assume for the classic Liu & Layland model
- of readiness without jitter and no self-suspensions, where prending
- jobs are always ready. *)
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index c0b7ad091..33fa5cd7a 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -1,15 +1,5 @@
-Require Import rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
-
-Require Import rt.restructuring.model.schedule.preemption_time.
-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.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 c84d38c4e..988413f76 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
@@ -1,24 +1,13 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.schedule.limited_preemptive.
+
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 fcc437b33..214f39696 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
@@ -1,23 +1,13 @@
-Require Import rt.util.all.
-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.aggregate.workload.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.model.arrival.arrival_curves.
-Require Import rt.restructuring.model.schedule.limited_preemptive.
+
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 ec552eb46..f78d709f2 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
@@ -1,26 +1,14 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
-(** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 f5ec02a06..c411242a2 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
@@ -1,23 +1,10 @@
-Require Import rt.util.all.
-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.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.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
(** Assume we have a fully preemptive model. *)
+Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 0797d23a7..88825b64b 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
@@ -1,23 +1,13 @@
-Require Import rt.util.all.
-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.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 Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.arrival.workload_bound.
+Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
-Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 3ca80c5bf..8662ed9f2 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -1,29 +1,13 @@
-Require Import rt.util.all.
-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.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.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
-
-Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_driven.
-Require Import rt.restructuring.analysis.arrival.workload_bound.
-Require Import rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.schedulability.
-Require Export rt.restructuring.analysis.definitions.busy_interval.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
+Require Export rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index 016ad4d5f..d59d6035c 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -1,7 +1,4 @@
-Require Export rt.restructuring.analysis.transform.swap.
Require Export rt.restructuring.analysis.transform.facts.replace_at.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.util.nat.
(** In this file, we establish invariants about schedules in which two
allocations have been swapped, as for instance it is done in the
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 0d6af1276..d22cedb04 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,5 +1,7 @@
Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index a66d11cc5..3c801eabc 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.limited_preemptive.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
--
GitLab