Commit 25754fea authored by Björn Brandenburg's avatar Björn Brandenburg

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

parent 9c7b4f30
......@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.preemption.job.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.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
......
......@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.preemption.valid_schedule.
Require Import rt.restructuring.model.preemption.job.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.task.preemption.limited_preemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
......
......@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.preemption.job.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.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
......
......@@ -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.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
Require Import rt.restructuring.model.preemption.task.instance.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -9,7 +9,7 @@ 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.
Require Import rt.restructuring.model.preemption.task.instance.floating.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
......@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.preemption.job.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.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
(** * Platform for Models with Limited Preemptions *)
......
......@@ -6,7 +6,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Import rt.restructuring.model.preemption.task.instance.nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
......@@ -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.instance.preemptive.
Require Import rt.restructuring.model.preemption.task.instance.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
(** * Platform for Fully Premptive Model *)
......
......@@ -143,7 +143,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Proof.
have BLOCK: blocking_bound ts tsk = 0.
{ by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/preemptive.fully_preemptive_model subnn big1_eq. }
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) .
all: eauto 2 with basic_facts.
- move => A /andP [LT NEQ].
......@@ -155,4 +155,4 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
+ by rewrite subnn addn0.
Qed.
End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
\ No newline at end of file
End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
......@@ -121,7 +121,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
Proof.
have BLOCK: blocking_bound higher_eq_priority ts tsk = 0.
{ by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/preemptive.fully_preemptive_model subnn big1_eq. }
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
all: eauto 2 with basic_facts.
- by rewrite BLOCK add0n.
......
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.task.instance.floating.
Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.preemption.valid_schedule.
Require Export rt.restructuring.model.preemption.task.instance.limited.
Require Export rt.restructuring.model.task.preemption.limited_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
......@@ -2,5 +2,5 @@ Require Export rt.restructuring.model.schedule.nonpreemptive.
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.task.preemption.fully_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
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.task.preemption.fully_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.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