model reorg: move priorities definition to own folder

restructuring/analysis/abstract/instantiations/ideal_processor.v

@@ -3,7 +3,7 @@ Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.schedule.sequential.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+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.

restructuring/analysis/arrival/workload_bound.v

 Require Import rt.util.sum.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.model.task.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+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.

restructuring/analysis/basic_facts/service_of_jobs.v

@@ -6,7 +6,7 @@ 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.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 Require Import rt.restructuring.analysis.basic_facts.service.

restructuring/analysis/basic_facts/workload.v

 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

restructuring/analysis/definitions/priority_inversion.v

@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+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.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

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

@@ -8,7 +8,7 @@ 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.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

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

@@ -8,7 +8,7 @@ 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.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

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

@@ -14,7 +14,7 @@ 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.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

restructuring/analysis/edf/rta/response_time_bound.v

@@ -14,7 +14,7 @@ Require Import rt.restructuring.model.preemption.task.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.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.

restructuring/analysis/facts/busy_interval_exists.v

@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
 

restructuring/analysis/facts/no_carry_in_exists.v

@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+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.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

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

@@ -8,7 +8,7 @@ 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.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

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

@@ -8,7 +8,7 @@ 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.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

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

@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

restructuring/analysis/fixed_priority/rta/response_time_bound.v

@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.

restructuring/model/aggregate/service_of_jobs.v

-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.model.processor.ideal.
      
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.