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

model reorg: get rid of purely re-export models

With proper re-exports everywhere, this is no longer necessary.
parent 7b64c4b0
...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload. ...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal. Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic. Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves. Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.floating. Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.model.schedule.work_conserving. Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes. Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.analysis.facts.edf. Require Import rt.restructuring.analysis.facts.edf.
......
...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload. ...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal. Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic. Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves. Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.limited. Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.model.schedule.work_conserving. Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes. Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.analysis.facts.edf. Require Import rt.restructuring.analysis.facts.edf.
......
...@@ -19,7 +19,8 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti ...@@ -19,7 +19,8 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive. Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
(** Assume we have a fully non-preemptive model. *) (** Assume we have a fully non-preemptive model. *)
Require Import rt.restructuring.model.preemption.nonpreemptive. Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
...@@ -19,7 +19,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive. ...@@ -19,7 +19,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive. Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
(** Assume we have a fully preemptive model. *) (** Assume we have a fully preemptive model. *)
Require Import rt.restructuring.model.preemption.preemptive. Require Import rt.restructuring.model.task.preemption.fully_preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload. ...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal. Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic. Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves. Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.floating. Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.model.schedule.work_conserving. Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes. Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.schedule.priority_driven. Require Import rt.restructuring.model.schedule.priority_driven.
......
...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload. ...@@ -7,7 +7,8 @@ Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal. Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic. Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves. Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.limited. Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.model.schedule.work_conserving. Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes. Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.schedule.priority_driven. Require Import rt.restructuring.model.schedule.priority_driven.
......
...@@ -18,7 +18,9 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti ...@@ -18,7 +18,9 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreempti
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive. Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
(** Assume we have a fully non-preemptive model. *) (** Assume we have a fully non-preemptive model. *)
Require Import rt.restructuring.model.preemption.nonpreemptive. Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
...@@ -18,7 +18,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive. ...@@ -18,7 +18,7 @@ Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive. Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
(** Assume we have a fully preemptive model. *) (** Assume we have a fully preemptive model. *)
Require Import rt.restructuring.model.preemption.preemptive. Require Import rt.restructuring.model.task.preemption.fully_preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.limited_preemptive.
Require Export rt.restructuring.model.schedule.nonpreemptive.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.fully_preemptive.
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