Commit 42e6a42b authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: move task concept to model.task.concept

parent eca90fdf
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Import rt.util.epsilon.
Require Import rt.util.tactics.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Reduction of the serach space for Abstract RTA *)
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.task.sequential.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.task_arrivals.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.analysis.arrival.workload_bound.
......
Require Import rt.util.sum.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.aggregate.task_arrivals.
Require Import rt.restructuring.model.arrival.arrival_curves.
......
......@@ -2,8 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.valid_schedule.
Require Import rt.restructuring.model.preemption.job.parameters.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
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.util.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.job.
Require Import rt.restructuring.behavior.schedule.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.valid_schedule.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
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.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
......
......@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
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.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
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.util.all.
Require Import rt.restructuring.behavior.all.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.aggregate.workload.
Require Export rt.restructuring.model.aggregate.service_of_jobs.
Require Export rt.restructuring.model.processor.ideal.
......
......@@ -2,7 +2,7 @@ Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.schedule.work_conserving.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
......@@ -2,8 +2,7 @@ Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * No Carry-In *)
......
......@@ -2,7 +2,7 @@ Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.analysis.definitions.busy_interval.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.analysis.definitions.busy_interval.
......
......@@ -2,7 +2,7 @@ Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.analysis.definitions.no_carry_in.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
(** In this file we provide basic definitions related to tasks on arrival sequences. *)
Section TaskArrivals.
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Section TaskMinInterArrivalTime.
Context {Task : TaskType}.
......
Require Export rt.util.all.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
(** Definition of a generic type of parameter relating a task
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.util.rel.
Require Export rt.util.list.
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.model.processor.ideal.
Require Export rt.util.seqset.
Require Export rt.util.rel.
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
(** Given task deadlines and a mapping from jobs to tasks
we provide a generic definition of job_deadline. *)
Instance job_deadline_from_task_deadline (Job : JobType) (Task : TaskType)
......
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.task.concept.
Section PropertyOfSequentiality.
(** Consider any type of job associated with any type of tasks... *)
......
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