From d14a37c02e80db3f167aeabd56f4ec418767c2dc Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 23 Nov 2019 16:08:59 +0100
Subject: [PATCH] Improve comments in analysis
---
restructuring/analysis/abstract/core/definitions.v | 5 ++---
restructuring/analysis/definitions/busy_interval.v | 3 +--
restructuring/analysis/definitions/no_carry_in.v | 3 +--
.../edf/rta/nonpr_reg/concrete_models/floating.v | 8 ++++++--
.../edf/rta/nonpr_reg/concrete_models/limited.v | 8 ++++++--
.../rta/nonpr_reg/concrete_models/nonpreemptive.v | 14 ++++++++------
.../edf/rta/nonpr_reg/concrete_models/preemptive.v | 14 ++++++++------
.../edf/rta/nonpr_reg/response_time_bound.v | 6 ++++--
.../analysis/edf/rta/response_time_bound.v | 7 +++++--
.../analysis/facts/busy_interval_exists.v | 3 +--
restructuring/analysis/facts/no_carry_in_exists.v | 3 +--
.../rta/nonpr_reg/concrete_models/floating.v | 4 ++--
.../rta/nonpr_reg/concrete_models/limited.v | 3 ++-
.../rta/nonpr_reg/concrete_models/nonpreemptive.v | 4 ++--
.../rta/nonpr_reg/concrete_models/preemptive.v | 9 ++++++---
.../rta/nonpr_reg/response_time_bound.v | 3 +--
.../fixed_priority/rta/response_time_bound.v | 3 +--
.../model/task/preemption/limited_preemptive.v | 3 +--
18 files changed, 58 insertions(+), 45 deletions(-)
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index e0341070e..59fe51b6e 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,9 +1,8 @@
Require Export rt.restructuring.model.task.concept.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** 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.
+Require Import rt.restructuring.model.processor.ideal.
(** * Definitions for Abstract Response-Time Analysis *)
(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA)
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index 5a2edb38f..bb1fff380 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -1,11 +1,10 @@
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.analysis.basic_facts.completion.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** 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.
-
(** * Busy Interval for JLFP-models *)
(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
Section BusyIntervalJLFP.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index f30d12ba1..252ab2794 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -1,10 +1,9 @@
Require Export rt.restructuring.model.priority.classes.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** 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 *)
(** In this module we define the notion of no carry-in time for uniprocessor schedulers. *)
Section NoCarryIn.
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 0fd62e5c4..693cb2e7e 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,14 +1,18 @@
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.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** 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.
+
+(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
(** * RTA for Model with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
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 b7550071d..1b646474b 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,14 +1,18 @@
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.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** 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.
+
+(** Throughout this file, we assume the task model with fixed preemption points. *)
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
(** * RTA for EDF-schedulers with Fixed Premption Points *)
(** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
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 725cc69ac..e72bc1c60 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,15 +1,17 @@
-Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
-
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.
Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+(** 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.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the fully non-preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
(** * RTA for Fully Non-Preemptive FP Model *)
(** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
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 6197685dc..07c5ebf84 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,15 +1,17 @@
-Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
-
Require Import rt.restructuring.analysis.edf.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.
Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Assume we have a fully preemptive model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+(** 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.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the fully preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
(** * RTA for Fully Preemptive EDF Model *)
(** In this section we prove the RTA theorem for the fully preemptive EDF model *)
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 885eb5881..6c59465f2 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -2,11 +2,13 @@ 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.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
(** * RTA for EDF-schedulers with Bounded Non-Preemprive Segments *)
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 982e050af..fda9c51b8 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -4,12 +4,15 @@ Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
Require Export rt.restructuring.analysis.schedulability.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.model.task.absolute_deadline.
+Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** 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.analysis.abstract.instantiations.ideal_processor.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
(** In this module we instantiate the Abstract Response-Time analysis
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 3e0864478..d97ca3841 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -2,6 +2,7 @@ Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
Require Export rt.restructuring.analysis.basic_facts.all.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -9,8 +10,6 @@ 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.
-
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
busy intervals for uniprocessor for JLFP schedulers. *)
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 1e9b85e35..26c4bdaf9 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -1,5 +1,6 @@
Require Export rt.restructuring.analysis.definitions.no_carry_in.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -7,8 +8,6 @@ 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.
-
(** * Existence of No Carry-In Instant *)
(** In this section, we derive an alternative condition for the existence of
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 18e002d13..6b9a836ac 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,5 +1,6 @@
Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -7,11 +8,10 @@ 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.
+(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
(** * RTA for Model with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating
non-preemptive regions FP model. *)
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 099c7bf59..7ce643664 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,5 +1,6 @@
Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -7,10 +8,10 @@ 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.
+(** Throughout this file, we assume the task model with fixed preemption points. *)
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * RTA for FP-schedulers with Fixed Premption Points *)
(** In this module we prove the RTA theorem for FP-schedulers with fixed preemption points. *)
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 f78d709f2..853e69903 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,6 +1,7 @@
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.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -8,10 +9,9 @@ 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.
+(** Throughout this file, we assume the fully non-preemptive task model. *)
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
(** * RTA for Fully Non-Preemptive FP Model *)
(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
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 c411242a2..b67faa581 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,13 +1,16 @@
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.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Assume we have a fully preemptive model. *)
+(** 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_preemptive.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the fully preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
(** * RTA for Fully Preemptive FP Model *)
(** In this module we prove the RTA theorem for fully preemptive FP model. *)
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 88825b64b..6f39f334d 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
@@ -2,6 +2,7 @@ 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.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -9,8 +10,6 @@ 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.
-
(** * RTA for FP-schedulers with Bounded Non-Preemprive Segments *)
(** In this section we instantiate the Abstract RTA for FP-schedulers
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 8662ed9f2..3d2122480 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -1,6 +1,7 @@
Require Export rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -8,8 +9,6 @@ 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 *)
(** In this module we instantiate the Abstract Response-Time analysis
(aRTA) to FP-schedulers for ideal uni-processor model of
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 5b6b7f687..1dc1094fc 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,7 +1,6 @@
Require Export rt.restructuring.model.task.preemption.parameters.
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
Require Import rt.restructuring.model.preemption.limited_preemptive.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we introduce a set of requirements for function
--
GitLab