Improve comments in analysis

restructuring/analysis/abstract/core/definitions.v

 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) 

restructuring/analysis/definitions/busy_interval.v

 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.

restructuring/analysis/definitions/no_carry_in.v

 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.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v

 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.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v

 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.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v

-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. *)

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v

-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 *)

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 *)
 

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

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. *)

restructuring/analysis/facts/no_carry_in_exists.v

 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 

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v

 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. *)

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v

 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. *)

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v

 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.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v

 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. *)

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

restructuring/analysis/fixed_priority/rta/response_time_bound.v

 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

restructuring/model/task/preemption/limited_preemptive.v

 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