Add hierarchy to the modules

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/induction.v ./util/ord_quantifier.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/bertogna_fp_example.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/parallel/bertogna_edf_example.v ./implementation/parallel/task.v ./implementation/parallel/schedule.v ./implementation/parallel/bertogna_fp_example.v ./implementation/parallel/job.v ./implementation/parallel/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/bertogna_fp_example.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/task.v ./implementation/apa/schedule.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/job.v ./implementation/apa/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/interference_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/apa/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/constrained_deadlines.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/constrained_deadlines.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/apa/time.v ./model/apa/schedulability.v ./model/apa/task.v ./model/apa/task_arrival.v ./model/apa/platform.v ./model/apa/schedule.v ./model/apa/priority.v ./model/apa/affinity.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/constrained_deadlines.v ./model/apa/workload.v ./model/apa/job.v ./model/apa/arrival_sequence.v ./model/apa/response_time.v -o Makefile 
+# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/arrival_sequence.v ./implementation/global/parallel/task.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/job.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/parallel/schedule.v ./implementation/global/basic/arrival_sequence.v ./implementation/global/basic/task.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/job.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -94,122 +94,104 @@ endif
 #                    #
 ######################
 
-VFILES:=util/fixedpoint.v\
-  util/ssromega.v\
-  util/bigcat.v\
-  util/nat.v\
+VFILES:=util/ssromega.v\
   util/seqset.v\
-  util/notation.v\
-  util/list.v\
+  util/sorting.v\
   util/powerset.v\
   util/all.v\
-  util/sorting.v\
-  util/tactics.v\
-  util/bigord.v\
-  util/induction.v\
   util/ord_quantifier.v\
+  util/nat.v\
   util/sum.v\
-  util/divround.v\
+  util/bigord.v\
   util/counting.v\
-  implementation/basic/bertogna_edf_example.v\
-  implementation/basic/task.v\
-  implementation/basic/schedule.v\
-  implementation/basic/bertogna_fp_example.v\
-  implementation/basic/job.v\
-  implementation/basic/arrival_sequence.v\
-  implementation/parallel/bertogna_edf_example.v\
-  implementation/parallel/task.v\
-  implementation/parallel/schedule.v\
-  implementation/parallel/bertogna_fp_example.v\
-  implementation/parallel/job.v\
-  implementation/parallel/arrival_sequence.v\
-  implementation/jitter/bertogna_edf_example.v\
-  implementation/jitter/task.v\
-  implementation/jitter/schedule.v\
-  implementation/jitter/bertogna_fp_example.v\
-  implementation/jitter/job.v\
-  implementation/jitter/arrival_sequence.v\
-  implementation/apa/bertogna_edf_example.v\
-  implementation/apa/task.v\
-  implementation/apa/schedule.v\
-  implementation/apa/bertogna_fp_example.v\
-  implementation/apa/job.v\
-  implementation/apa/arrival_sequence.v\
-  analysis/basic/bertogna_fp_theory.v\
-  analysis/basic/interference_bound_edf.v\
-  analysis/basic/interference_bound_fp.v\
-  analysis/basic/interference_bound.v\
-  analysis/basic/bertogna_edf_comp.v\
-  analysis/basic/bertogna_fp_comp.v\
-  analysis/basic/bertogna_edf_theory.v\
-  analysis/basic/workload_bound.v\
-  analysis/parallel/bertogna_fp_theory.v\
-  analysis/parallel/interference_bound_edf.v\
-  analysis/parallel/interference_bound_fp.v\
-  analysis/parallel/interference_bound.v\
-  analysis/parallel/bertogna_edf_comp.v\
-  analysis/parallel/bertogna_fp_comp.v\
-  analysis/parallel/bertogna_edf_theory.v\
-  analysis/parallel/workload_bound.v\
-  analysis/jitter/bertogna_fp_theory.v\
-  analysis/jitter/interference_bound_edf.v\
-  analysis/jitter/interference_bound_fp.v\
-  analysis/jitter/interference_bound.v\
-  analysis/jitter/bertogna_edf_comp.v\
-  analysis/jitter/bertogna_fp_comp.v\
-  analysis/jitter/bertogna_edf_theory.v\
-  analysis/jitter/workload_bound.v\
-  analysis/apa/bertogna_fp_theory.v\
+  util/tactics.v\
+  util/induction.v\
+  util/list.v\
+  util/divround.v\
+  util/bigcat.v\
+  util/fixedpoint.v\
+  util/notation.v\
+  analysis/global/jitter/bertogna_fp_comp.v\
+  analysis/global/jitter/interference_bound_edf.v\
+  analysis/global/jitter/workload_bound.v\
+  analysis/global/jitter/bertogna_edf_comp.v\
+  analysis/global/jitter/bertogna_fp_theory.v\
+  analysis/global/jitter/interference_bound.v\
+  analysis/global/jitter/interference_bound_fp.v\
+  analysis/global/jitter/bertogna_edf_theory.v\
+  analysis/global/parallel/bertogna_fp_comp.v\
+  analysis/global/parallel/interference_bound_edf.v\
+  analysis/global/parallel/workload_bound.v\
+  analysis/global/parallel/bertogna_edf_comp.v\
+  analysis/global/parallel/bertogna_fp_theory.v\
+  analysis/global/parallel/interference_bound.v\
+  analysis/global/parallel/interference_bound_fp.v\
+  analysis/global/parallel/bertogna_edf_theory.v\
+  analysis/global/basic/bertogna_fp_comp.v\
+  analysis/global/basic/interference_bound_edf.v\
+  analysis/global/basic/workload_bound.v\
+  analysis/global/basic/bertogna_edf_comp.v\
+  analysis/global/basic/bertogna_fp_theory.v\
+  analysis/global/basic/interference_bound.v\
+  analysis/global/basic/interference_bound_fp.v\
+  analysis/global/basic/bertogna_edf_theory.v\
+  analysis/apa/bertogna_fp_comp.v\
   analysis/apa/interference_bound_edf.v\
-  analysis/apa/interference_bound_fp.v\
-  analysis/apa/interference_bound.v\
+  analysis/apa/workload_bound.v\
   analysis/apa/bertogna_edf_comp.v\
-  analysis/apa/bertogna_fp_comp.v\
+  analysis/apa/bertogna_fp_theory.v\
+  analysis/apa/interference_bound.v\
+  analysis/apa/interference_bound_fp.v\
   analysis/apa/bertogna_edf_theory.v\
-  analysis/apa/workload_bound.v\
-  model/basic/time.v\
-  model/basic/schedulability.v\
-  model/basic/task.v\
-  model/basic/task_arrival.v\
-  model/basic/platform.v\
-  model/basic/schedule.v\
-  model/basic/priority.v\
-  model/basic/interference_edf.v\
-  model/basic/interference.v\
-  model/basic/constrained_deadlines.v\
-  model/basic/workload.v\
-  model/basic/job.v\
-  model/basic/arrival_sequence.v\
-  model/basic/response_time.v\
-  model/jitter/time.v\
-  model/jitter/schedulability.v\
-  model/jitter/task.v\
-  model/jitter/task_arrival.v\
-  model/jitter/platform.v\
-  model/jitter/schedule.v\
-  model/jitter/priority.v\
-  model/jitter/interference_edf.v\
-  model/jitter/interference.v\
-  model/jitter/constrained_deadlines.v\
-  model/jitter/workload.v\
-  model/jitter/job.v\
-  model/jitter/arrival_sequence.v\
-  model/jitter/response_time.v\
-  model/apa/time.v\
-  model/apa/schedulability.v\
-  model/apa/task.v\
-  model/apa/task_arrival.v\
-  model/apa/platform.v\
-  model/apa/schedule.v\
-  model/apa/priority.v\
-  model/apa/affinity.v\
+  model/arrival_sequence.v\
+  model/task.v\
+  model/task_arrival.v\
+  model/priority.v\
+  model/global/workload.v\
+  model/global/schedulability.v\
+  model/global/jitter/interference_edf.v\
+  model/global/jitter/interference.v\
+  model/global/jitter/job.v\
+  model/global/jitter/constrained_deadlines.v\
+  model/global/jitter/schedule.v\
+  model/global/jitter/platform.v\
+  model/global/response_time.v\
+  model/global/basic/interference_edf.v\
+  model/global/basic/interference.v\
+  model/global/basic/constrained_deadlines.v\
+  model/global/basic/schedule.v\
+  model/global/basic/platform.v\
+  model/job.v\
+  model/time.v\
   model/apa/interference_edf.v\
   model/apa/interference.v\
+  model/apa/affinity.v\
   model/apa/constrained_deadlines.v\
-  model/apa/workload.v\
-  model/apa/job.v\
-  model/apa/arrival_sequence.v\
-  model/apa/response_time.v
+  model/apa/platform.v\
+  implementation/global/jitter/arrival_sequence.v\
+  implementation/global/jitter/task.v\
+  implementation/global/jitter/bertogna_edf_example.v\
+  implementation/global/jitter/job.v\
+  implementation/global/jitter/bertogna_fp_example.v\
+  implementation/global/jitter/schedule.v\
+  implementation/global/parallel/arrival_sequence.v\
+  implementation/global/parallel/task.v\
+  implementation/global/parallel/bertogna_edf_example.v\
+  implementation/global/parallel/job.v\
+  implementation/global/parallel/bertogna_fp_example.v\
+  implementation/global/parallel/schedule.v\
+  implementation/global/basic/arrival_sequence.v\
+  implementation/global/basic/task.v\
+  implementation/global/basic/bertogna_edf_example.v\
+  implementation/global/basic/job.v\
+  implementation/global/basic/bertogna_fp_example.v\
+  implementation/global/basic/schedule.v\
+  implementation/apa/arrival_sequence.v\
+  implementation/apa/task.v\
+  implementation/apa/bertogna_edf_example.v\
+  implementation/apa/job.v\
+  implementation/apa/bertogna_fp_example.v\
+  implementation/apa/schedule.v
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(VFILES))

README.md

@@ -2,17 +2,39 @@
 
 This repository contains the main Coq proof spec & proof development of the RT-PROOFS project.
 
+## Directory Structure
 
-## Plan
+The Prosa directory is organized in a hierarchy: while generic, reusable foundations stay in
+the upper levels, definitions for specific analyses should go deeper into the directory tree.
 
-For now, this is more or less just a "code dump" with a flat hierarchy to get things started.
+### Base Directories
 
-Going forward, the goal is to both
+Currently, Prosa contains the following base directories:
 
-- restructure the repository as it grows in scope, and to
+- **model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling.
+	  
+- **analysis/:** Definition, proofs and implementation of schedulability analyses.
 
-- add significant documentation to make it easier to bring new collaborators who are not yet familiar with Coq into the project.
+- **implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations.
+		       Testing the main theorems in an assumption free environment shows the absence of contradictions.
 
+### Internal Directories
+
+Within each base directory you can find the different classes of schedulers.
+
+- **model/uni:** Uniprocessor scheduling.
+- **model/global:** Global scheduling.
+- **model/partitioned:** Partitioned scheduling.
+- **model/apa:** APA scheduling.
+
+### Extending Prosa
+
+When adding a new model or analysis to Prosa, please extend the corresponding directory.
+For example, the schedulability analysis for global scheduling with release jitter is organized as follows.
+
+- **model/global/jitter:** Definitions and lemmas for global scheduling with release jitter.
+- **analysis/global/jitter:** Analysis for global scheduling with release jitter.
+- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. 
 
 ## Commit and Development Rules
 
@@ -26,4 +48,6 @@ Going forward, the goal is to both
 
 5. Pushing fixes, small improvements, etc. is always ok. 
 
-6. Document the tactics that you use in the [list of tactics](doc/tactics.md).
\ No newline at end of file
+6. Document the tactics that you use in the [list of tactics](doc/tactics.md).
+
+7. Whenever you have time available, please help with extending the documentation. :-)
\ No newline at end of file

analysis/apa/bertogna_edf_theory.v

 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.task_arrival
-               rt.model.apa.schedule rt.model.apa.platform rt.model.apa.interference
-               rt.model.apa.workload rt.model.apa.schedulability rt.model.apa.priority
-               rt.model.apa.platform rt.model.apa.response_time
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.interference
                rt.model.apa.affinity rt.model.apa.constrained_deadlines.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.

analysis/apa/bertogna_fp_theory.v

-Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.task_arrival
-               rt.model.apa.schedule rt.model.apa.platform rt.model.apa.constrained_deadlines
-               rt.model.apa.workload rt.model.apa.schedulability rt.model.apa.priority
-               rt.model.apa.response_time rt.model.apa.interference
-               rt.model.apa.affinity rt.model.apa.constrained_deadlines.
-Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_fp.
+Require Import rt.util.all.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.schedulability
+               rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.constrained_deadlines
+               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.analysis.apa.workload_bound
+               rt.analysis.apa.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
@@ -13,7 +15,6 @@ Module ResponseTimeAnalysisFP.
          Platform Schedulability ResponseTime Priority
          SporadicTaskArrival WorkloadBound Affinity ConstrainedDeadlines.
     
-
   (* In this section, we prove that any fixed point in the APA-reduction of Bertogna
      and Cirinei's RTA for FP scheduling with slack updates is a safe response-time
      bound. This result corresponds to Lemma 9 in the revised version of the APA paper:

analysis/apa/interference_bound.v

 Require Import rt.util.all.
-Require Import rt.model.apa.schedule.
+Require Import rt.model.global.basic.schedule.
 Require Import rt.analysis.apa.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 

analysis/apa/interference_bound_edf.v

 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.task_arrival rt.model.apa.platform rt.model.apa.response_time
-               rt.model.apa.workload rt.model.apa.priority rt.model.apa.schedulability
-               rt.model.apa.interference rt.model.apa.interference_edf
-               rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.interference
+               rt.model.apa.interference_edf rt.model.apa.affinity.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 

analysis/apa/interference_bound_fp.v

 Require Import rt.util.all.
-Require Import rt.model.apa.schedule rt.model.apa.priority rt.model.apa.workload
-               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 

analysis/apa/workload_bound.v

 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.task_arrival rt.model.apa.response_time
-               rt.model.apa.workload rt.model.apa.schedulability.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.schedulability
+               rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.

analysis/basic/bertogna_edf_comp.v → analysis/global/basic/bertogna_edf_comp.v

 Require Import rt.util.all.
-Require Import rt.analysis.basic.bertogna_edf_theory.
+Require Import rt.analysis.global.basic.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.

analysis/basic/bertogna_edf_theory.v → analysis/global/basic/bertogna_edf_theory.v

 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
-               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
-               rt.model.basic.platform rt.model.basic.response_time
-               rt.model.basic.constrained_deadlines.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
+Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference rt.model.global.basic.platform
+               rt.model.global.basic.constrained_deadlines.
+Require Import rt.analysis.global.basic.workload_bound rt.analysis.global.basic.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.

analysis/basic/bertogna_fp_comp.v → analysis/global/basic/bertogna_fp_comp.v

 Require Import rt.util.all.
-Require Import rt.analysis.basic.bertogna_fp_theory.
+Require Import rt.analysis.global.basic.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.

analysis/basic/bertogna_fp_theory.v → analysis/global/basic/bertogna_fp_theory.v

 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.constrained_deadlines
-               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
-               rt.model.basic.response_time rt.model.basic.interference.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.constrained_deadlines rt.model.global.basic.interference.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.

analysis/basic/interference_bound.v → analysis/global/basic/interference_bound.v

 Require Import rt.util.all.
-Require Import rt.model.basic.schedule.
-Require Import rt.analysis.basic.workload_bound.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.analysis.global.basic.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.

analysis/basic/interference_bound_edf.v → analysis/global/basic/interference_bound_edf.v

 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
-               rt.model.basic.interference rt.model.basic.interference_edf.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
+Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference rt.model.global.basic.interference_edf.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.

analysis/basic/interference_bound_fp.v → analysis/global/basic/interference_bound_fp.v

 Require Import rt.util.all.
-Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
-               rt.model.basic.interference.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.

analysis/basic/workload_bound.v → analysis/global/basic/workload_bound.v

 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.schedulability.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.

analysis/jitter/bertogna_edf_comp.v → analysis/global/jitter/bertogna_edf_comp.v

 Require Import rt.util.all.
-Require Import rt.analysis.jitter.bertogna_edf_theory.
+Require Import rt.analysis.global.jitter.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.

analysis/jitter/bertogna_edf_theory.v → analysis/global/jitter/bertogna_edf_theory.v

 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference
-               rt.model.jitter.workload rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.constrained_deadlines
-               rt.model.jitter.response_time.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_edf.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform rt.model.global.jitter.interference
+               rt.model.global.jitter.constrained_deadlines.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDFJitter.

analysis/jitter/bertogna_fp_comp.v → analysis/global/jitter/bertogna_fp_comp.v

 Require Import rt.util.all.
-Require Import rt.analysis.jitter.bertogna_fp_theory.
+Require Import rt.analysis.global.jitter.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.

analysis/jitter/bertogna_fp_theory.v → analysis/global/jitter/bertogna_fp_theory.v

 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.constrained_deadlines
-               rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority
-               rt.model.jitter.response_time rt.model.jitter.interference.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound_fp.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.interference
+               rt.model.global.jitter.schedule rt.model.global.jitter.platform
+               rt.model.global.jitter.constrained_deadlines.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.

analysis/jitter/interference_bound.v → analysis/global/jitter/interference_bound.v

 Require Import rt.util.all.
-Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule
-               rt.model.jitter.interference rt.model.jitter.priority.
-Require Import rt.analysis.jitter.workload_bound.
+Require Import rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.
+Require Import rt.analysis.global.jitter.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundJitter.

analysis/jitter/interference_bound_edf.v → analysis/global/jitter/interference_bound_edf.v

 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
-               rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
-               rt.model.jitter.interference rt.model.jitter.interference_edf.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform rt.model.global.jitter.interference
+               rt.model.global.jitter.interference_edf.
+Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDFJitter.

analysis/jitter/interference_bound_fp.v → analysis/global/jitter/interference_bound_fp.v

 Require Import rt.util.all.
-Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload
-               rt.model.jitter.interference.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.