Commit ff119057 authored by Björn Brandenburg's avatar Björn Brandenburg

fix dependency of preemption model on analysis facts

By our newly adopted convention, the model/ module should not depend on analysis facts.
parent a97aad24
......@@ -15,6 +15,11 @@ 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.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
......@@ -15,6 +15,9 @@ 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.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
......@@ -14,6 +14,9 @@ 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.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
(** Assume we have a fully non-preemptive model. *)
Require Import rt.restructuring.model.preemption.nonpreemptive.
......
......@@ -14,6 +14,9 @@ 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.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
(** Assume we have a fully preemptive model. *)
Require Import rt.restructuring.model.preemption.preemptive.
......
......@@ -14,6 +14,10 @@ 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.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
......@@ -14,6 +14,9 @@ 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.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
......@@ -13,6 +13,9 @@ 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.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
(** Assume we have a fully non-preemptive model. *)
Require Import rt.restructuring.model.preemption.nonpreemptive.
......
......@@ -13,6 +13,9 @@ 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.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
(** Assume we have a fully preemptive model. *)
Require Import rt.restructuring.model.preemption.preemptive.
......
......@@ -4,10 +4,6 @@ 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.processor.ideal.
Require Import rt.restructuring.analysis.basic_facts.workload.
Require Import rt.restructuring.analysis.basic_facts.arrivals.
Require Import rt.restructuring.analysis.basic_facts.completion.
Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
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.analysis.basic_facts.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
......@@ -7,9 +7,3 @@ Require Export rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.task.instance.floating.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
......@@ -7,7 +7,3 @@ Require Export rt.restructuring.model.preemption.task.parameters.
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.task.instance.limited.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
......@@ -7,7 +7,3 @@ Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.preemption.task.instance.nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
......@@ -5,6 +5,3 @@ Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.preemption.task.instance.preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Export
job.preemptive task.preemptive rtc_threshold.preemptive.
\ No newline at end of file
......@@ -2,7 +2,6 @@ Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment