streamline some imports in the results module

results/edf/rta/floating_nonpreemptive.v

@@ -4,13 +4,11 @@ Require Import prosa.model.readiness.basic.
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
+Require Import prosa.model.priority.edf.
 
 (** * RTA for EDF with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
 
-(** Throughout this file, we assume the EDF priority policy. *)
-Require Import prosa.model.priority.edf.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.

results/edf/rta/fully_nonpreemptive.v

@@ -5,17 +5,12 @@ Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.basic.
-
+Require Export prosa.model.task.preemption.fully_nonpreemptive.
+Require Import prosa.model.priority.edf.
 
 (** * RTA for Fully Non-Preemptive EDF *)
 (** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
 
-(** Throughout this file, we assume the EDF priority policy. *)
-Require Import prosa.model.priority.edf.
-
-(** Furthermore, we assume the fully non-preemptive task model. *)
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.

results/edf/rta/fully_preemptive.v

@@ -6,13 +6,11 @@ Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.basic.
 Require Import prosa.model.task.preemption.fully_preemptive.
+Require Import prosa.model.priority.edf.
 
 (** * RTA for Fully Preemptive EDF *)
 (** In this section we prove the RTA theorem for the fully preemptive EDF model *)
 
-(** Throughout this file, we assume the EDF priority policy. *)
-Require Import prosa.model.priority.edf.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.

results/edf/rta/limited_preemptive.v

 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-Require Import prosa.model.readiness.basic.
+Require Export prosa.model.readiness.basic.
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.basic.
+Require Export prosa.model.task.preemption.limited_preemptive.
+Require Export prosa.model.priority.edf.
 
 (** * RTA for EDF with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with
     fixed preemption points. *)
 
-(** Throughout this file, we assume the EDF priority policy. *)
-Require Import prosa.model.priority.edf.
-
-(** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
-Require Import prosa.model.task.preemption.limited_preemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.

results/fixed_priority/rta/bounded_pi.v

 Require Export prosa.model.schedule.priority_driven.
-Require Import prosa.analysis.abstract.ideal_jlfp_rta.
+Require Export prosa.analysis.abstract.ideal_jlfp_rta.
 Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)

results/fixed_priority/rta/floating_nonpreemptive.v

@@ -7,10 +7,6 @@ Require Export prosa.analysis.facts.readiness.sequential.
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
 
-(** Throughout this file, we assume the FP priority policy,
-    schedules, and the sequential readiness model. *)
-Require Import prosa.model.readiness.sequential.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFloatingModelwithArrivalCurves.

results/fixed_priority/rta/fully_nonpreemptive.v

@@ -4,17 +4,11 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
+Require Export prosa.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 FP model. *)
 
-(** Throughout this file, we assume the FP priority policy,
-    schedules, and the sequential readiness model. *)
-Require Import prosa.model.readiness.sequential.
-
-(** Furthermore, we assume the fully non-preemptive task model. *)
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.

results/fixed_priority/rta/fully_preemptive.v

@@ -4,15 +4,11 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
-Require Import prosa.model.task.preemption.fully_preemptive.
+Require Export prosa.model.task.preemption.fully_preemptive.
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this section we prove the RTA theorem for the fully preemptive FP model *)
 
-(** Throughout this file, we assume the FP priority policy,
-    schedules, and the sequential readiness model. *)
-Require Import prosa.model.readiness.sequential.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFullyPreemptiveFPModelwithArrivalCurves.

results/fixed_priority/rta/limited_preemptive.v

@@ -3,19 +3,12 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.sequential.
+Require Export prosa.model.task.preemption.limited_preemptive.
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with
     fixed preemption points. *)
 
-(** Throughout this file, we assume the FP priority policy,
-    schedules, and the sequential readiness model. *)
-Require Import prosa.model.readiness.sequential.
-
-(** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
-Require Import prosa.model.task.preemption.limited_preemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.