model reorg: move task preemption parameters to model.task.preemption

restructuring/analysis/abstract/core/abstract_rta.v

@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.schedulability.

restructuring/analysis/abstract/core/abstract_seq_rta.v

@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+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.
 

restructuring/analysis/basic_facts/preemption/job/limited.v

@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 

restructuring/analysis/basic_facts/preemption/job/preemptive.v

@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 
 (** * Preemptions in Fully Premptive Model *)

restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v

@@ -3,7 +3,7 @@ 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.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.floating.

restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v

@@ -4,7 +4,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
 (** In this section, we provide a few basic properties 

restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v

@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.
 Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.

restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v

@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 Require Import rt.restructuring.model.preemption.task.instance.nonpreemptive.

restructuring/analysis/basic_facts/preemption/task/floating.v

@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.valid_schedule.

restructuring/analysis/basic_facts/preemption/task/limited.v

@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.

restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v

@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.

restructuring/analysis/edf/rta/response_time_bound.v

@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.schedule.work_conserving.

restructuring/analysis/facts/priority_inversion_is_bounded.v

@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.schedule.preemption_time.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+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.

restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v

@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.

restructuring/analysis/fixed_priority/rta/response_time_bound.v

@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.

restructuring/model/preemption/job/instance/limited.v

 Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** Definition of a parameter relating a job
     to the sequence of its preemption points. *)

restructuring/model/preemption/rtc_threshold/instance/floating.v

-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion

restructuring/model/preemption/rtc_threshold/instance/limited.v

-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion

restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v

-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 

restructuring/model/preemption/rtc_threshold/instance/preemptive.v

-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion