Commit 1306c75c authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: flatten model.preemption

parent 4d5c9497
......@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
......
......@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
......@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
Require Import rt.restructuring.model.preemption.fully_preemptive.
(** * Preemptions in Fully Premptive Model *)
(** In this section, we prove that instantiation of predicate
......
......@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
......
......@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
......
......@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
......
......@@ -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.instance.preemptive.
Require Import rt.restructuring.model.preemption.fully_preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
......
......@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.parameter.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
......
......@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.basic_facts.all.
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.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
......
......@@ -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.instance.preemptive.
Require Import rt.restructuring.model.preemption.fully_preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
......
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.limited_preemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.preemption.job.instance.limited.
Require Export rt.restructuring.model.preemption.limited_preemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
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