From 42e6a42bd8c0bd29b115ac59b24f6e7d57847dcb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 18:03:22 +0100
Subject: [PATCH] model reorg: move task concept to model.task.concept

---
 restructuring/analysis/abstract/core/abstract_rta.v            | 2 +-
 restructuring/analysis/abstract/core/abstract_seq_rta.v        | 2 +-
 restructuring/analysis/abstract/core/definitions.v             | 2 +-
 .../analysis/abstract/core/reduction_of_search_space.v         | 3 +--
 .../sufficient_condition_for_run_to_completion_threshold.v     | 2 +-
 .../analysis/abstract/instantiations/ideal_processor.v         | 2 +-
 restructuring/analysis/arrival/rbf.v                           | 2 +-
 restructuring/analysis/arrival/workload_bound.v                | 2 +-
 restructuring/analysis/basic_facts/preemption/job/limited.v    | 3 +--
 .../analysis/basic_facts/preemption/job/nonpreemptive.v        | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/floating.v   | 2 +-
 .../basic_facts/preemption/rtc_threshold/job_preemptable.v     | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/limited.v    | 2 +-
 .../basic_facts/preemption/rtc_threshold/nonpreemptive.v       | 2 +-
 .../analysis/basic_facts/preemption/rtc_threshold/preemptive.v | 2 +-
 restructuring/analysis/basic_facts/preemption/task/floating.v  | 2 +-
 restructuring/analysis/basic_facts/preemption/task/limited.v   | 2 +-
 .../analysis/basic_facts/preemption/task/nonpreemptive.v       | 2 +-
 .../analysis/basic_facts/preemption/task/preemptive.v          | 2 +-
 restructuring/analysis/basic_facts/service_of_jobs.v           | 2 +-
 restructuring/analysis/definitions/busy_interval.v             | 2 +-
 restructuring/analysis/definitions/no_carry_in.v               | 3 +--
 restructuring/analysis/definitions/priority_inversion.v        | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/floating.v      | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/limited.v       | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v    | 2 +-
 restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v | 2 +-
 restructuring/analysis/edf/rta/response_time_bound.v           | 2 +-
 restructuring/analysis/facts/busy_interval_exists.v            | 2 +-
 restructuring/analysis/facts/no_carry_in_exists.v              | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/floating.v    | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/limited.v     | 2 +-
 .../rta/nonpr_reg/concrete_models/nonpreemptive.v              | 2 +-
 .../fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v  | 2 +-
 .../fixed_priority/rta/nonpr_reg/response_time_bound.v         | 2 +-
 .../analysis/fixed_priority/rta/response_time_bound.v          | 2 +-
 restructuring/analysis/task_schedule.v                         | 2 +-
 restructuring/model/aggregate/task_arrivals.v                  | 3 +--
 restructuring/model/arrival/sporadic.v                         | 3 +--
 restructuring/model/preemption/task/parameters.v               | 3 +--
 restructuring/model/priority/classes.v                         | 2 +-
 restructuring/model/schedule/tdma.v                            | 2 +-
 restructuring/model/task/absolute_deadline.v                   | 3 +--
 restructuring/model/{task.v => task/concept.v}                 | 0
 restructuring/model/task/sequential.v                          | 3 +--
 46 files changed, 45 insertions(+), 53 deletions(-)
 rename restructuring/model/{task.v => task/concept.v} (100%)

diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index cdd9633bb..fe5bd0e9e 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index a3c9c2167..b28114eb0 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 22f555066..22116f1dd 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,6 +1,6 @@
 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.
diff --git a/restructuring/analysis/abstract/core/reduction_of_search_space.v b/restructuring/analysis/abstract/core/reduction_of_search_space.v
index d6b403ffd..ec0e02249 100644
--- a/restructuring/analysis/abstract/core/reduction_of_search_space.v
+++ b/restructuring/analysis/abstract/core/reduction_of_search_space.v
@@ -1,7 +1,6 @@
 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 *)
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index cb9f38f5d..00a4644ac 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -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.
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index 41901dc53..6ecd2d694 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -1,5 +1,5 @@
 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.
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index 87f9fcde0..bde7b2ae1 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index bdb5ba43e..07be1832e 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,6 +1,6 @@
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 18f6c9c7c..c10c94133 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index d647b3942..727b6a712 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index b76e25200..31d9f7925 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
index 8e0d187cd..63689bce1 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,6 +1,6 @@
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index c29e09a13..f71f40c61 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 60cdbe495..52153acc9 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index b6577dce3..d84813271 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index da27b50bd..70284babe 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 67fe37f64..7aca2dc61 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index 00a713699..fa2bda3ca 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index 3b19eef2c..771a37d3f 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 93741e6f1..698a63177 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,7 +1,7 @@
 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.
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index d0ab1ec1a..0857ebc79 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -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.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index f9131ff55..2118f1c9f 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -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 *)
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index ff1eca46d..559b0a207 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 6eed5c6bc..71e1e4c66 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 6b77d1bba..b8e4da568 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 2b964a28a..65b36f528 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 9f864f23e..edd6f9162 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index 65b7a144e..ccb737e69 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -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.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 41edf3e0b..931ed0aa6 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -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.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 14748080b..d5600eb1d 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -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.
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 78ca3122e..196b6376c 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index aa8cf8ee9..e48ce1209 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index a7b5a7526..f93f2e8f2 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 6491faac4..e2387d28e 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 792b7badd..9b0e59e26 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index c77c2eddf..85d7f7878 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -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.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index dad6bcae4..18e460ccd 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -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.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index ec3fd834f..2f7eb103e 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,4 +1,4 @@
-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.
diff --git a/restructuring/model/aggregate/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
index 585ff897e..9216784b1 100644
--- a/restructuring/model/aggregate/task_arrivals.v
+++ b/restructuring/model/aggregate/task_arrivals.v
@@ -1,5 +1,4 @@
-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.
 
diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
index 3806e931c..23b36230c 100644
--- a/restructuring/model/arrival/sporadic.v
+++ b/restructuring/model/arrival/sporadic.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 Section TaskMinInterArrivalTime.
   Context {Task : TaskType}.
 
diff --git a/restructuring/model/preemption/task/parameters.v b/restructuring/model/preemption/task/parameters.v
index cb701952f..d4307eacd 100644
--- a/restructuring/model/preemption/task/parameters.v
+++ b/restructuring/model/preemption/task/parameters.v
@@ -1,6 +1,5 @@
 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 
diff --git a/restructuring/model/priority/classes.v b/restructuring/model/priority/classes.v
index cf4bd4b21..138496cee 100644
--- a/restructuring/model/priority/classes.v
+++ b/restructuring/model/priority/classes.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.util.rel.
 Require Export rt.util.list.
 
diff --git a/restructuring/model/schedule/tdma.v b/restructuring/model/schedule/tdma.v
index 12510dfaa..7b32d2dbc 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/restructuring/model/schedule/tdma.v
@@ -1,4 +1,4 @@
-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.
diff --git a/restructuring/model/task/absolute_deadline.v b/restructuring/model/task/absolute_deadline.v
index 7ead8087b..b32ac00e8 100644
--- a/restructuring/model/task/absolute_deadline.v
+++ b/restructuring/model/task/absolute_deadline.v
@@ -1,5 +1,4 @@
-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)
diff --git a/restructuring/model/task.v b/restructuring/model/task/concept.v
similarity index 100%
rename from restructuring/model/task.v
rename to restructuring/model/task/concept.v
diff --git a/restructuring/model/task/sequential.v b/restructuring/model/task/sequential.v
index 4c108a9b5..c52d2c940 100644
--- a/restructuring/model/task/sequential.v
+++ b/restructuring/model/task/sequential.v
@@ -1,5 +1,4 @@
-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... *)
-- 
GitLab