From df6ebb503d27c7c2505e523e144750ae9c5e2c1e Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Wed, 3 Aug 2016 19:39:41 +0200
Subject: [PATCH] Add hierarchy to the modules

---
 Makefile                                      | 192 ++++++++----------
 README.md                                     |  36 +++-
 analysis/apa/bertogna_edf_theory.v            |   9 +-
 analysis/apa/bertogna_fp_theory.v             |  17 +-
 analysis/apa/interference_bound.v             |   2 +-
 analysis/apa/interference_bound_edf.v         |  11 +-
 analysis/apa/interference_bound_fp.v          |   6 +-
 analysis/apa/workload_bound.v                 |   7 +-
 .../{ => global}/basic/bertogna_edf_comp.v    |   2 +-
 .../{ => global}/basic/bertogna_edf_theory.v  |  13 +-
 .../{ => global}/basic/bertogna_fp_comp.v     |   2 +-
 .../{ => global}/basic/bertogna_fp_theory.v   |  12 +-
 .../{ => global}/basic/interference_bound.v   |   4 +-
 .../basic/interference_bound_edf.v            |  12 +-
 .../basic/interference_bound_fp.v             |   8 +-
 analysis/{ => global}/basic/workload_bound.v  |   7 +-
 .../{ => global}/jitter/bertogna_edf_comp.v   |   2 +-
 .../{ => global}/jitter/bertogna_edf_theory.v |  15 +-
 .../{ => global}/jitter/bertogna_fp_comp.v    |   2 +-
 .../{ => global}/jitter/bertogna_fp_theory.v  |  13 +-
 .../{ => global}/jitter/interference_bound.v  |   6 +-
 .../jitter/interference_bound_edf.v           |  12 +-
 .../jitter/interference_bound_fp.v            |   7 +-
 analysis/{ => global}/jitter/workload_bound.v |   7 +-
 .../{ => global}/parallel/bertogna_edf_comp.v |   2 +-
 .../parallel/bertogna_edf_theory.v            |  12 +-
 .../{ => global}/parallel/bertogna_fp_comp.v  |   2 +-
 .../parallel/bertogna_fp_theory.v             |  14 +-
 .../parallel/interference_bound.v             |   4 +-
 .../parallel/interference_bound_edf.v         |  12 +-
 .../parallel/interference_bound_fp.v          |   7 +-
 .../{ => global}/parallel/workload_bound.v    |   7 +-
 implementation/apa/arrival_sequence.v         |   3 +-
 implementation/apa/bertogna_edf_example.v     |   8 +-
 implementation/apa/bertogna_fp_example.v      |   8 +-
 implementation/apa/job.v                      |   2 +-
 implementation/apa/schedule.v                 |   7 +-
 implementation/apa/task.v                     |   5 +-
 .../{ => global}/basic/arrival_sequence.v     |   6 +-
 .../{ => global}/basic/bertogna_edf_example.v |  20 +-
 .../{ => global}/basic/bertogna_fp_example.v  |  20 +-
 implementation/{ => global}/basic/job.v       |   4 +-
 implementation/{ => global}/basic/schedule.v  |   4 +-
 implementation/{ => global}/basic/task.v      |   4 +-
 .../{ => global}/jitter/arrival_sequence.v    |   6 +-
 .../jitter/bertogna_edf_example.v             |  21 +-
 .../{ => global}/jitter/bertogna_fp_example.v |  21 +-
 implementation/{ => global}/jitter/job.v      |   2 +-
 implementation/{ => global}/jitter/schedule.v |   5 +-
 implementation/{ => global}/jitter/task.v     |   2 +-
 .../global/parallel/arrival_sequence.v        |   2 +
 .../parallel/bertogna_edf_example.v           |  20 +-
 .../parallel/bertogna_fp_example.v            |  22 +-
 implementation/global/parallel/job.v          |   2 +
 .../{ => global}/parallel/schedule.v          |   2 +-
 implementation/global/parallel/task.v         |   2 +
 implementation/parallel/arrival_sequence.v    |   2 -
 implementation/parallel/job.v                 |   2 -
 implementation/parallel/task.v                |   2 -
 model/apa/affinity.v                          |   4 +-
 model/apa/arrival_sequence.v                  |   2 -
 model/apa/constrained_deadlines.v             |   7 +-
 model/apa/interference.v                      |   6 +-
 model/apa/interference_edf.v                  |   8 +-
 model/apa/job.v                               |   2 -
 model/apa/platform.v                          |   6 +-
 model/apa/priority.v                          |   2 -
 model/apa/response_time.v                     |   2 -
 model/apa/schedulability.v                    |   2 -
 model/apa/schedule.v                          |   2 -
 model/apa/task.v                              |   2 -
 model/apa/task_arrival.v                      |   2 -
 model/apa/time.v                              |   2 -
 model/apa/workload.v                          |   2 -
 model/{basic => }/arrival_sequence.v          |   2 +-
 .../basic/constrained_deadlines.v             |   6 +-
 model/{ => global}/basic/interference.v       |  48 +----
 model/{ => global}/basic/interference_edf.v   |   6 +-
 model/{ => global}/basic/platform.v           |   4 +-
 model/{ => global}/basic/schedule.v           |   2 +-
 .../jitter/constrained_deadlines.v            |   6 +-
 model/{ => global}/jitter/interference.v      |   7 +-
 model/{ => global}/jitter/interference_edf.v  |   8 +-
 model/{ => global}/jitter/job.v               |   4 +-
 model/{ => global}/jitter/platform.v          |   5 +-
 model/{ => global}/jitter/schedule.v          |   5 +-
 model/{basic => global}/response_time.v       |   4 +-
 model/{basic => global}/schedulability.v      |   3 +-
 model/{basic => global}/workload.v            |   6 +-
 model/jitter/arrival_sequence.v               |   3 -
 model/jitter/priority.v                       |   3 -
 model/jitter/response_time.v                  |   4 -
 model/jitter/schedulability.v                 |   4 -
 model/jitter/task.v                           |   4 -
 model/jitter/task_arrival.v                   |   4 -
 model/jitter/time.v                           |   3 -
 model/jitter/workload.v                       |   3 -
 model/{basic => }/job.v                       |   2 +-
 model/{basic => }/jobin_eqdec.v               |   0
 model/{basic => }/priority.v                  |  47 ++++-
 model/{basic => }/task.v                      |   2 +-
 model/{basic => }/task_arrival.v              |   4 +-
 model/{basic => }/time.v                      |   0
 103 files changed, 457 insertions(+), 461 deletions(-)
 rename analysis/{ => global}/basic/bertogna_edf_comp.v (99%)
 rename analysis/{ => global}/basic/bertogna_edf_theory.v (98%)
 rename analysis/{ => global}/basic/bertogna_fp_comp.v (99%)
 rename analysis/{ => global}/basic/bertogna_fp_theory.v (98%)
 rename analysis/{ => global}/basic/interference_bound.v (92%)
 rename analysis/{ => global}/basic/interference_bound_edf.v (99%)
 rename analysis/{ => global}/basic/interference_bound_fp.v (83%)
 rename analysis/{ => global}/basic/workload_bound.v (99%)
 rename analysis/{ => global}/jitter/bertogna_edf_comp.v (99%)
 rename analysis/{ => global}/jitter/bertogna_edf_theory.v (98%)
 rename analysis/{ => global}/jitter/bertogna_fp_comp.v (99%)
 rename analysis/{ => global}/jitter/bertogna_fp_theory.v (98%)
 rename analysis/{ => global}/jitter/interference_bound.v (86%)
 rename analysis/{ => global}/jitter/interference_bound_edf.v (99%)
 rename analysis/{ => global}/jitter/interference_bound_fp.v (84%)
 rename analysis/{ => global}/jitter/workload_bound.v (99%)
 rename analysis/{ => global}/parallel/bertogna_edf_comp.v (99%)
 rename analysis/{ => global}/parallel/bertogna_edf_theory.v (98%)
 rename analysis/{ => global}/parallel/bertogna_fp_comp.v (99%)
 rename analysis/{ => global}/parallel/bertogna_fp_theory.v (97%)
 rename analysis/{ => global}/parallel/interference_bound.v (91%)
 rename analysis/{ => global}/parallel/interference_bound_edf.v (98%)
 rename analysis/{ => global}/parallel/interference_bound_fp.v (83%)
 rename analysis/{ => global}/parallel/workload_bound.v (98%)
 rename implementation/{ => global}/basic/arrival_sequence.v (95%)
 rename implementation/{ => global}/basic/bertogna_edf_example.v (89%)
 rename implementation/{ => global}/basic/bertogna_fp_example.v (91%)
 rename implementation/{ => global}/basic/job.v (95%)
 rename implementation/{ => global}/basic/schedule.v (98%)
 rename implementation/{ => global}/basic/task.v (95%)
 rename implementation/{ => global}/jitter/arrival_sequence.v (95%)
 rename implementation/{ => global}/jitter/bertogna_edf_example.v (88%)
 rename implementation/{ => global}/jitter/bertogna_fp_example.v (91%)
 rename implementation/{ => global}/jitter/job.v (97%)
 rename implementation/{ => global}/jitter/schedule.v (98%)
 rename implementation/{ => global}/jitter/task.v (98%)
 create mode 100644 implementation/global/parallel/arrival_sequence.v
 rename implementation/{ => global}/parallel/bertogna_edf_example.v (89%)
 rename implementation/{ => global}/parallel/bertogna_fp_example.v (91%)
 create mode 100644 implementation/global/parallel/job.v
 rename implementation/{ => global}/parallel/schedule.v (74%)
 create mode 100644 implementation/global/parallel/task.v
 delete mode 100644 implementation/parallel/arrival_sequence.v
 delete mode 100644 implementation/parallel/job.v
 delete mode 100644 implementation/parallel/task.v
 delete mode 100644 model/apa/arrival_sequence.v
 delete mode 100644 model/apa/job.v
 delete mode 100644 model/apa/priority.v
 delete mode 100644 model/apa/response_time.v
 delete mode 100644 model/apa/schedulability.v
 delete mode 100644 model/apa/schedule.v
 delete mode 100644 model/apa/task.v
 delete mode 100644 model/apa/task_arrival.v
 delete mode 100644 model/apa/time.v
 delete mode 100644 model/apa/workload.v
 rename model/{basic => }/arrival_sequence.v (98%)
 rename model/{ => global}/basic/constrained_deadlines.v (98%)
 rename model/{ => global}/basic/interference.v (84%)
 rename model/{ => global}/basic/interference_edf.v (91%)
 rename model/{ => global}/basic/platform.v (97%)
 rename model/{ => global}/basic/schedule.v (99%)
 rename model/{ => global}/jitter/constrained_deadlines.v (98%)
 rename model/{ => global}/jitter/interference.v (97%)
 rename model/{ => global}/jitter/interference_edf.v (90%)
 rename model/{ => global}/jitter/job.v (92%)
 rename model/{ => global}/jitter/platform.v (97%)
 rename model/{ => global}/jitter/schedule.v (98%)
 rename model/{basic => global}/response_time.v (97%)
 rename model/{basic => global}/schedulability.v (98%)
 rename model/{basic => global}/workload.v (94%)
 delete mode 100644 model/jitter/arrival_sequence.v
 delete mode 100644 model/jitter/priority.v
 delete mode 100644 model/jitter/response_time.v
 delete mode 100644 model/jitter/schedulability.v
 delete mode 100644 model/jitter/task.v
 delete mode 100644 model/jitter/task_arrival.v
 delete mode 100644 model/jitter/time.v
 delete mode 100644 model/jitter/workload.v
 rename model/{basic => }/job.v (97%)
 rename model/{basic => }/jobin_eqdec.v (100%)
 rename model/{basic => }/priority.v (83%)
 rename model/{basic => }/task.v (98%)
 rename model/{basic => }/task_arrival.v (90%)
 rename model/{basic => }/time.v (100%)

diff --git a/Makefile b/Makefile
index 0fb66166a..5b33988c7 100644
--- a/Makefile
+++ b/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))
diff --git a/README.md b/README.md
index 11e943375..8d5003a12 100644
--- a/README.md
+++ b/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
diff --git a/analysis/apa/bertogna_edf_theory.v b/analysis/apa/bertogna_edf_theory.v
index 97485a09c..096c3e8e7 100644
--- a/analysis/apa/bertogna_edf_theory.v
+++ b/analysis/apa/bertogna_edf_theory.v
@@ -1,8 +1,9 @@
 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.
diff --git a/analysis/apa/bertogna_fp_theory.v b/analysis/apa/bertogna_fp_theory.v
index f3a912c84..4c25c5e3c 100644
--- a/analysis/apa/bertogna_fp_theory.v
+++ b/analysis/apa/bertogna_fp_theory.v
@@ -1,10 +1,12 @@
-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:
diff --git a/analysis/apa/interference_bound.v b/analysis/apa/interference_bound.v
index 8814c15fd..a3971721f 100644
--- a/analysis/apa/interference_bound.v
+++ b/analysis/apa/interference_bound.v
@@ -1,5 +1,5 @@
 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.
 
diff --git a/analysis/apa/interference_bound_edf.v b/analysis/apa/interference_bound_edf.v
index ef241c8cc..f34967822 100644
--- a/analysis/apa/interference_bound_edf.v
+++ b/analysis/apa/interference_bound_edf.v
@@ -1,9 +1,10 @@
 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.
 
diff --git a/analysis/apa/interference_bound_fp.v b/analysis/apa/interference_bound_fp.v
index 542308461..b23243a59 100644
--- a/analysis/apa/interference_bound_fp.v
+++ b/analysis/apa/interference_bound_fp.v
@@ -1,6 +1,8 @@
 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.
 
diff --git a/analysis/apa/workload_bound.v b/analysis/apa/workload_bound.v
index ce0b84847..1d9a4c869 100644
--- a/analysis/apa/workload_bound.v
+++ b/analysis/apa/workload_bound.v
@@ -1,7 +1,8 @@
 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.
diff --git a/analysis/basic/bertogna_edf_comp.v b/analysis/global/basic/bertogna_edf_comp.v
similarity index 99%
rename from analysis/basic/bertogna_edf_comp.v
rename to analysis/global/basic/bertogna_edf_comp.v
index 3bc47989a..ad6f43082 100755
--- a/analysis/basic/bertogna_edf_comp.v
+++ b/analysis/global/basic/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 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.
diff --git a/analysis/basic/bertogna_edf_theory.v b/analysis/global/basic/bertogna_edf_theory.v
similarity index 98%
rename from analysis/basic/bertogna_edf_theory.v
rename to analysis/global/basic/bertogna_edf_theory.v
index b35dc6039..8b01b6f74 100644
--- a/analysis/basic/bertogna_edf_theory.v
+++ b/analysis/global/basic/bertogna_edf_theory.v
@@ -1,10 +1,11 @@
 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.
diff --git a/analysis/basic/bertogna_fp_comp.v b/analysis/global/basic/bertogna_fp_comp.v
similarity index 99%
rename from analysis/basic/bertogna_fp_comp.v
rename to analysis/global/basic/bertogna_fp_comp.v
index 7208a9ee6..6bc0e4d64 100644
--- a/analysis/basic/bertogna_fp_comp.v
+++ b/analysis/global/basic/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 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.
diff --git a/analysis/basic/bertogna_fp_theory.v b/analysis/global/basic/bertogna_fp_theory.v
similarity index 98%
rename from analysis/basic/bertogna_fp_theory.v
rename to analysis/global/basic/bertogna_fp_theory.v
index 637f1f5f4..2df63d4f1 100644
--- a/analysis/basic/bertogna_fp_theory.v
+++ b/analysis/global/basic/bertogna_fp_theory.v
@@ -1,9 +1,11 @@
 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.
diff --git a/analysis/basic/interference_bound.v b/analysis/global/basic/interference_bound.v
similarity index 92%
rename from analysis/basic/interference_bound.v
rename to analysis/global/basic/interference_bound.v
index c5ecc342d..8edaa74f4 100644
--- a/analysis/basic/interference_bound.v
+++ b/analysis/global/basic/interference_bound.v
@@ -1,6 +1,6 @@
 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.
diff --git a/analysis/basic/interference_bound_edf.v b/analysis/global/basic/interference_bound_edf.v
similarity index 99%
rename from analysis/basic/interference_bound_edf.v
rename to analysis/global/basic/interference_bound_edf.v
index 592123f1b..d2f674847 100644
--- a/analysis/basic/interference_bound_edf.v
+++ b/analysis/global/basic/interference_bound_edf.v
@@ -1,9 +1,11 @@
 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.
diff --git a/analysis/basic/interference_bound_fp.v b/analysis/global/basic/interference_bound_fp.v
similarity index 83%
rename from analysis/basic/interference_bound_fp.v
rename to analysis/global/basic/interference_bound_fp.v
index da6ad7ca3..8f3537742 100644
--- a/analysis/basic/interference_bound_fp.v
+++ b/analysis/global/basic/interference_bound_fp.v
@@ -1,7 +1,9 @@
 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.
diff --git a/analysis/basic/workload_bound.v b/analysis/global/basic/workload_bound.v
similarity index 99%
rename from analysis/basic/workload_bound.v
rename to analysis/global/basic/workload_bound.v
index 70b0436ac..f086c9104 100644
--- a/analysis/basic/workload_bound.v
+++ b/analysis/global/basic/workload_bound.v
@@ -1,7 +1,8 @@
 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.
diff --git a/analysis/jitter/bertogna_edf_comp.v b/analysis/global/jitter/bertogna_edf_comp.v
similarity index 99%
rename from analysis/jitter/bertogna_edf_comp.v
rename to analysis/global/jitter/bertogna_edf_comp.v
index 980b598ff..31701e5aa 100755
--- a/analysis/jitter/bertogna_edf_comp.v
+++ b/analysis/global/jitter/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 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.
diff --git a/analysis/jitter/bertogna_edf_theory.v b/analysis/global/jitter/bertogna_edf_theory.v
similarity index 98%
rename from analysis/jitter/bertogna_edf_theory.v
rename to analysis/global/jitter/bertogna_edf_theory.v
index 71cd4dcba..96112a054 100644
--- a/analysis/jitter/bertogna_edf_theory.v
+++ b/analysis/global/jitter/bertogna_edf_theory.v
@@ -1,11 +1,12 @@
 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.
diff --git a/analysis/jitter/bertogna_fp_comp.v b/analysis/global/jitter/bertogna_fp_comp.v
similarity index 99%
rename from analysis/jitter/bertogna_fp_comp.v
rename to analysis/global/jitter/bertogna_fp_comp.v
index 5e9f58214..13b5b83f5 100644
--- a/analysis/jitter/bertogna_fp_comp.v
+++ b/analysis/global/jitter/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 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.
diff --git a/analysis/jitter/bertogna_fp_theory.v b/analysis/global/jitter/bertogna_fp_theory.v
similarity index 98%
rename from analysis/jitter/bertogna_fp_theory.v
rename to analysis/global/jitter/bertogna_fp_theory.v
index c4abdd9bc..d9f5cf956 100644
--- a/analysis/jitter/bertogna_fp_theory.v
+++ b/analysis/global/jitter/bertogna_fp_theory.v
@@ -1,9 +1,12 @@
 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.
diff --git a/analysis/jitter/interference_bound.v b/analysis/global/jitter/interference_bound.v
similarity index 86%
rename from analysis/jitter/interference_bound.v
rename to analysis/global/jitter/interference_bound.v
index 27b9de550..d91cdc9a9 100644
--- a/analysis/jitter/interference_bound.v
+++ b/analysis/global/jitter/interference_bound.v
@@ -1,7 +1,7 @@
 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.
diff --git a/analysis/jitter/interference_bound_edf.v b/analysis/global/jitter/interference_bound_edf.v
similarity index 99%
rename from analysis/jitter/interference_bound_edf.v
rename to analysis/global/jitter/interference_bound_edf.v
index 48d2fad71..65e0820f8 100644
--- a/analysis/jitter/interference_bound_edf.v
+++ b/analysis/global/jitter/interference_bound_edf.v
@@ -1,9 +1,11 @@
 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.
diff --git a/analysis/jitter/interference_bound_fp.v b/analysis/global/jitter/interference_bound_fp.v
similarity index 84%
rename from analysis/jitter/interference_bound_fp.v
rename to analysis/global/jitter/interference_bound_fp.v
index 4bc8c267e..3167a62b1 100644
--- a/analysis/jitter/interference_bound_fp.v
+++ b/analysis/global/jitter/interference_bound_fp.v
@@ -1,7 +1,8 @@
 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.
+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.
 
 Module InterferenceBoundFP.
diff --git a/analysis/jitter/workload_bound.v b/analysis/global/jitter/workload_bound.v
similarity index 99%
rename from analysis/jitter/workload_bound.v
rename to analysis/global/jitter/workload_bound.v
index 66bf9677b..e12fbd2e6 100644
--- a/analysis/jitter/workload_bound.v
+++ b/analysis/global/jitter/workload_bound.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.task_arrival rt.model.jitter.response_time
-               rt.model.jitter.schedulability rt.model.jitter.workload.
+Require Import rt.model.task 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.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBoundJitter.
diff --git a/analysis/parallel/bertogna_edf_comp.v b/analysis/global/parallel/bertogna_edf_comp.v
similarity index 99%
rename from analysis/parallel/bertogna_edf_comp.v
rename to analysis/global/parallel/bertogna_edf_comp.v
index 5ec5b9b70..32c5f7898 100755
--- a/analysis/parallel/bertogna_edf_comp.v
+++ b/analysis/global/parallel/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.parallel.bertogna_edf_theory.
+Require Import rt.analysis.global.parallel.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/analysis/parallel/bertogna_edf_theory.v b/analysis/global/parallel/bertogna_edf_theory.v
similarity index 98%
rename from analysis/parallel/bertogna_edf_theory.v
rename to analysis/global/parallel/bertogna_edf_theory.v
index 3a7fafdff..0e939a957 100644
--- a/analysis/parallel/bertogna_edf_theory.v
+++ b/analysis/global/parallel/bertogna_edf_theory.v
@@ -1,9 +1,11 @@
 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.
-Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.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.interference
+               rt.model.global.basic.platform.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/analysis/parallel/bertogna_fp_comp.v b/analysis/global/parallel/bertogna_fp_comp.v
similarity index 99%
rename from analysis/parallel/bertogna_fp_comp.v
rename to analysis/global/parallel/bertogna_fp_comp.v
index 0656ea907..b7fa67b9b 100644
--- a/analysis/parallel/bertogna_fp_comp.v
+++ b/analysis/global/parallel/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.parallel.bertogna_fp_theory.
+Require Import rt.analysis.global.parallel.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
diff --git a/analysis/parallel/bertogna_fp_theory.v b/analysis/global/parallel/bertogna_fp_theory.v
similarity index 97%
rename from analysis/parallel/bertogna_fp_theory.v
rename to analysis/global/parallel/bertogna_fp_theory.v
index 64db0dab1..71941b6c2 100644
--- a/analysis/parallel/bertogna_fp_theory.v
+++ b/analysis/global/parallel/bertogna_fp_theory.v
@@ -1,11 +1,11 @@
 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.parallel.workload_bound rt.analysis.parallel.interference_bound_fp.
+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.constrained_deadlines rt.model.global.basic.interference.
+Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/analysis/parallel/interference_bound.v b/analysis/global/parallel/interference_bound.v
similarity index 91%
rename from analysis/parallel/interference_bound.v
rename to analysis/global/parallel/interference_bound.v
index 63fed9291..28a7e8a63 100644
--- a/analysis/parallel/interference_bound.v
+++ b/analysis/global/parallel/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.schedule.
-Require Import rt.analysis.parallel.workload_bound.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.analysis.global.parallel.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/analysis/parallel/interference_bound_edf.v b/analysis/global/parallel/interference_bound_edf.v
similarity index 98%
rename from analysis/parallel/interference_bound_edf.v
rename to analysis/global/parallel/interference_bound_edf.v
index f0f2c6a33..4b11160f4 100644
--- a/analysis/parallel/interference_bound_edf.v
+++ b/analysis/global/parallel/interference_bound_edf.v
@@ -1,9 +1,11 @@
 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.parallel.workload_bound rt.analysis.parallel.interference_bound.
+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.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.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.
diff --git a/analysis/parallel/interference_bound_fp.v b/analysis/global/parallel/interference_bound_fp.v
similarity index 83%
rename from analysis/parallel/interference_bound_fp.v
rename to analysis/global/parallel/interference_bound_fp.v
index e6aa91d6f..e976b390e 100644
--- a/analysis/parallel/interference_bound_fp.v
+++ b/analysis/global/parallel/interference_bound_fp.v
@@ -1,7 +1,8 @@
 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.parallel.workload_bound rt.analysis.parallel.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.parallel.workload_bound rt.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/analysis/parallel/workload_bound.v b/analysis/global/parallel/workload_bound.v
similarity index 98%
rename from analysis/parallel/workload_bound.v
rename to analysis/global/parallel/workload_bound.v
index 6cae44aec..ea291fb19 100644
--- a/analysis/parallel/workload_bound.v
+++ b/analysis/global/parallel/workload_bound.v
@@ -1,7 +1,8 @@
 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.response_time rt.model.global.workload
+               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.
diff --git a/implementation/apa/arrival_sequence.v b/implementation/apa/arrival_sequence.v
index ef341ef73..ddee41bb3 100644
--- a/implementation/apa/arrival_sequence.v
+++ b/implementation/apa/arrival_sequence.v
@@ -1,7 +1,6 @@
 (* We can reuse the.apa definition of periodic arrival sequence. *)
 Require Import rt.util.all.
-Require Import rt.model.apa.arrival_sequence rt.model.apa.job
-               rt.model.apa.task rt.model.apa.task_arrival.
+Require Import rt.model.arrival_sequence rt.model.job rt.model.task rt.model.task_arrival.
 Require Import rt.implementation.apa.task rt.implementation.apa.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
diff --git a/implementation/apa/bertogna_edf_example.v b/implementation/apa/bertogna_edf_example.v
index c922446a9..98defcb39 100644
--- a/implementation/apa/bertogna_edf_example.v
+++ b/implementation/apa/bertogna_edf_example.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.schedule rt.model.apa.interference
-               rt.model.apa.schedulability
-               rt.model.apa.priority rt.model.apa.platform.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference rt.model.apa.platform.
 Require Import rt.analysis.apa.workload_bound
                rt.analysis.apa.interference_bound_edf
                rt.analysis.apa.bertogna_edf_comp.
diff --git a/implementation/apa/bertogna_fp_example.v b/implementation/apa/bertogna_fp_example.v
index e2dc3f547..4896677a6 100644
--- a/implementation/apa/bertogna_fp_example.v
+++ b/implementation/apa/bertogna_fp_example.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.schedule rt.model.apa.schedulability
-               rt.model.apa.priority rt.model.apa.platform
-               rt.model.apa.interference.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference rt.model.apa.platform.
 Require Import rt.analysis.apa.workload_bound
                rt.analysis.apa.interference_bound_fp
                rt.analysis.apa.bertogna_fp_comp.
diff --git a/implementation/apa/job.v b/implementation/apa/job.v
index bf22a52ac..1bb339470 100644
--- a/implementation/apa/job.v
+++ b/implementation/apa/job.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.util.all.
+Require Import rt.model.time rt.util.all.
 Require Import rt.implementation.apa.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
diff --git a/implementation/apa/schedule.v b/implementation/apa/schedule.v
index 80014bdb2..266e6d6e7 100644
--- a/implementation/apa/schedule.v
+++ b/implementation/apa/schedule.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.arrival_sequence rt.model.apa.schedule
-               rt.model.apa.platform rt.model.apa.priority.
+Require Import rt.model.arrival_sequence rt.model.job rt.model.task rt.model.priority
+               rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/apa/task.v b/implementation/apa/task.v
index 6281667a8..e5f356501 100644
--- a/implementation/apa/task.v
+++ b/implementation/apa/task.v
@@ -1,5 +1,6 @@
-Require Import rt.model.apa.time rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.affinity.
+Require Import rt.util.all.
+Require Import rt.model.time rt.model.task.
+Require Import rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/basic/arrival_sequence.v b/implementation/global/basic/arrival_sequence.v
similarity index 95%
rename from implementation/basic/arrival_sequence.v
rename to implementation/global/basic/arrival_sequence.v
index 8e17a0d7c..22f97bb7f 100644
--- a/implementation/basic/arrival_sequence.v
+++ b/implementation/global/basic/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.arrival_sequence rt.model.basic.job
-               rt.model.basic.task rt.model.basic.task_arrival.
-Require Import rt.implementation.basic.task rt.implementation.basic.job.
+Require Import rt.model.arrival_sequence rt.model.job
+               rt.model.task rt.model.task_arrival.
+Require Import rt.implementation.global.basic.task rt.implementation.global.basic.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/implementation/basic/bertogna_edf_example.v b/implementation/global/basic/bertogna_edf_example.v
similarity index 89%
rename from implementation/basic/bertogna_edf_example.v
rename to implementation/global/basic/bertogna_edf_example.v
index dfd5e8f99..b418fd885 100644
--- a/implementation/basic/bertogna_edf_example.v
+++ b/implementation/global/basic/bertogna_edf_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.basic.workload_bound
-               rt.analysis.basic.interference_bound_edf
-               rt.analysis.basic.bertogna_edf_comp.
-Require Import rt.implementation.basic.job
-               rt.implementation.basic.task
-               rt.implementation.basic.schedule
-               rt.implementation.basic.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_edf
+               rt.analysis.global.basic.bertogna_edf_comp.
+Require Import rt.implementation.global.basic.job
+               rt.implementation.global.basic.task
+               rt.implementation.global.basic.schedule
+               rt.implementation.global.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/basic/bertogna_fp_example.v b/implementation/global/basic/bertogna_fp_example.v
similarity index 91%
rename from implementation/basic/bertogna_fp_example.v
rename to implementation/global/basic/bertogna_fp_example.v
index e6f766bb7..173131fea 100644
--- a/implementation/basic/bertogna_fp_example.v
+++ b/implementation/global/basic/bertogna_fp_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.basic.workload_bound
-               rt.analysis.basic.interference_bound_fp
-               rt.analysis.basic.bertogna_fp_comp.
-Require Import rt.implementation.basic.job
-               rt.implementation.basic.task
-               rt.implementation.basic.schedule
-               rt.implementation.basic.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_fp
+               rt.analysis.global.basic.bertogna_fp_comp.
+Require Import rt.implementation.global.basic.job
+               rt.implementation.global.basic.task
+               rt.implementation.global.basic.schedule
+               rt.implementation.global.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/basic/job.v b/implementation/global/basic/job.v
similarity index 95%
rename from implementation/basic/job.v
rename to implementation/global/basic/job.v
index db1a3c372..cd24f6d85 100644
--- a/implementation/basic/job.v
+++ b/implementation/global/basic/job.v
@@ -1,5 +1,5 @@
-Require Import rt.model.basic.time rt.util.all.
-Require Import rt.implementation.basic.task.
+Require Import rt.model.time rt.util.all.
+Require Import rt.implementation.global.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/implementation/basic/schedule.v b/implementation/global/basic/schedule.v
similarity index 98%
rename from implementation/basic/schedule.v
rename to implementation/global/basic/schedule.v
index 99adb9705..a8df880d0 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/global/basic/schedule.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.arrival_sequence rt.model.basic.schedule
-               rt.model.basic.platform rt.model.basic.priority.
+Require Import rt.model.job rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/basic/task.v b/implementation/global/basic/task.v
similarity index 95%
rename from implementation/basic/task.v
rename to implementation/global/basic/task.v
index fe158837b..532e4bcbf 100644
--- a/implementation/basic/task.v
+++ b/implementation/global/basic/task.v
@@ -1,5 +1,5 @@
-Require Import rt.model.basic.time rt.util.all.
-Require Import rt.model.basic.task.
+Require Import rt.model.time rt.util.all.
+Require Import rt.model.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/global/jitter/arrival_sequence.v
similarity index 95%
rename from implementation/jitter/arrival_sequence.v
rename to implementation/global/jitter/arrival_sequence.v
index 4fb3a3c96..90d5b8b9b 100644
--- a/implementation/jitter/arrival_sequence.v
+++ b/implementation/global/jitter/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.arrival_sequence rt.model.jitter.job
-               rt.model.jitter.task rt.model.jitter.task_arrival.
-Require Import rt.implementation.jitter.task rt.implementation.jitter.job.
+Require Import rt.model.arrival_sequence rt.model.task rt.model.task_arrival.
+Require Import rt.model.global.jitter.job.
+Require Import rt.implementation.global.jitter.task rt.implementation.global.jitter.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/implementation/jitter/bertogna_edf_example.v b/implementation/global/jitter/bertogna_edf_example.v
similarity index 88%
rename from implementation/jitter/bertogna_edf_example.v
rename to implementation/global/jitter/bertogna_edf_example.v
index 4763d22d9..384b64c0b 100644
--- a/implementation/jitter/bertogna_edf_example.v
+++ b/implementation/global/jitter/bertogna_edf_example.v
@@ -1,14 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task
-               rt.model.jitter.schedule rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.platform.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_edf
-               rt.analysis.jitter.bertogna_edf_comp.
-Require Import rt.implementation.jitter.job
-               rt.implementation.jitter.task
-               rt.implementation.jitter.schedule
-               rt.implementation.jitter.arrival_sequence.
+Require Import rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_edf
+               rt.analysis.global.jitter.bertogna_edf_comp.
+Require Import rt.implementation.global.jitter.job
+               rt.implementation.global.jitter.task
+               rt.implementation.global.jitter.schedule
+               rt.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/jitter/bertogna_fp_example.v b/implementation/global/jitter/bertogna_fp_example.v
similarity index 91%
rename from implementation/jitter/bertogna_fp_example.v
rename to implementation/global/jitter/bertogna_fp_example.v
index da15c4d31..023dc7bd9 100644
--- a/implementation/jitter/bertogna_fp_example.v
+++ b/implementation/global/jitter/bertogna_fp_example.v
@@ -1,14 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task
-               rt.model.jitter.schedule rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.platform.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_fp
-               rt.analysis.jitter.bertogna_fp_comp.
-Require Import rt.implementation.jitter.job
-               rt.implementation.jitter.task
-               rt.implementation.jitter.schedule
-               rt.implementation.jitter.arrival_sequence.
+Require Import rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_fp
+               rt.analysis.global.jitter.bertogna_fp_comp.
+Require Import rt.implementation.global.jitter.job
+               rt.implementation.global.jitter.task
+               rt.implementation.global.jitter.schedule
+               rt.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/jitter/job.v b/implementation/global/jitter/job.v
similarity index 97%
rename from implementation/jitter/job.v
rename to implementation/global/jitter/job.v
index 3eb0633ca..abe5e300a 100644
--- a/implementation/jitter/job.v
+++ b/implementation/global/jitter/job.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.implementation.jitter.task.
+Require Import rt.implementation.global.jitter.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/implementation/jitter/schedule.v b/implementation/global/jitter/schedule.v
similarity index 98%
rename from implementation/jitter/schedule.v
rename to implementation/global/jitter/schedule.v
index 58268053b..ebee74bee 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/global/jitter/schedule.v
@@ -1,6 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.arrival_sequence rt.model.jitter.schedule
-               rt.model.jitter.platform rt.model.jitter.priority.
+Require Import rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/jitter/task.v b/implementation/global/jitter/task.v
similarity index 98%
rename from implementation/jitter/task.v
rename to implementation/global/jitter/task.v
index 4e0238f39..07802b708 100644
--- a/implementation/jitter/task.v
+++ b/implementation/global/jitter/task.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task.
+Require Import rt.model.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/global/parallel/arrival_sequence.v b/implementation/global/parallel/arrival_sequence.v
new file mode 100644
index 000000000..8d51d82cb
--- /dev/null
+++ b/implementation/global/parallel/arrival_sequence.v
@@ -0,0 +1,2 @@
+(* We reuse the arrival sequence from the basic model. *)
+Require Export rt.implementation.global.basic.arrival_sequence.
\ No newline at end of file
diff --git a/implementation/parallel/bertogna_edf_example.v b/implementation/global/parallel/bertogna_edf_example.v
similarity index 89%
rename from implementation/parallel/bertogna_edf_example.v
rename to implementation/global/parallel/bertogna_edf_example.v
index d2398d72d..cb7793c13 100644
--- a/implementation/parallel/bertogna_edf_example.v
+++ b/implementation/global/parallel/bertogna_edf_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.parallel.workload_bound
-               rt.analysis.parallel.interference_bound_edf
-               rt.analysis.parallel.bertogna_edf_comp.
-Require Import rt.implementation.parallel.job
-               rt.implementation.parallel.task
-               rt.implementation.parallel.schedule
-               rt.implementation.parallel.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_edf
+               rt.analysis.global.parallel.bertogna_edf_comp.
+Require Import rt.implementation.global.parallel.job
+               rt.implementation.global.parallel.task
+               rt.implementation.global.parallel.schedule
+               rt.implementation.global.parallel.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/parallel/bertogna_fp_example.v b/implementation/global/parallel/bertogna_fp_example.v
similarity index 91%
rename from implementation/parallel/bertogna_fp_example.v
rename to implementation/global/parallel/bertogna_fp_example.v
index aef7d69a4..630eb6c02 100644
--- a/implementation/parallel/bertogna_fp_example.v
+++ b/implementation/global/parallel/bertogna_fp_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform
-               rt.model.basic.interference.
-Require Import rt.analysis.parallel.workload_bound
-               rt.analysis.parallel.interference_bound_fp
-               rt.analysis.parallel.bertogna_fp_comp.
-Require Import rt.implementation.parallel.job
-               rt.implementation.parallel.task
-               rt.implementation.parallel.schedule
-               rt.implementation.parallel.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_fp
+               rt.analysis.global.parallel.bertogna_fp_comp.
+Require Import rt.implementation.global.parallel.job
+               rt.implementation.global.parallel.task
+               rt.implementation.global.parallel.schedule
+               rt.implementation.global.parallel.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/global/parallel/job.v b/implementation/global/parallel/job.v
new file mode 100644
index 000000000..db7513c16
--- /dev/null
+++ b/implementation/global/parallel/job.v
@@ -0,0 +1,2 @@
+(* We reuse the job from the basic model. *)
+Require Export rt.implementation.global.basic.job.
\ No newline at end of file
diff --git a/implementation/parallel/schedule.v b/implementation/global/parallel/schedule.v
similarity index 74%
rename from implementation/parallel/schedule.v
rename to implementation/global/parallel/schedule.v
index fdfac7039..81cf67067 100644
--- a/implementation/parallel/schedule.v
+++ b/implementation/global/parallel/schedule.v
@@ -1,4 +1,4 @@
 (* For simplicity, we reuse the scheduler from the basic model.
    Although it does not exploit parallelism, it is a restricted case
    of a parallel scheduler. *)
-Require Export rt.implementation.basic.schedule.
\ No newline at end of file
+Require Export rt.implementation.global.basic.schedule.
\ No newline at end of file
diff --git a/implementation/global/parallel/task.v b/implementation/global/parallel/task.v
new file mode 100644
index 000000000..d176fe900
--- /dev/null
+++ b/implementation/global/parallel/task.v
@@ -0,0 +1,2 @@
+(* We reuse the task from the basic model. *)
+Require Export rt.implementation.global.basic.task.
\ No newline at end of file
diff --git a/implementation/parallel/arrival_sequence.v b/implementation/parallel/arrival_sequence.v
deleted file mode 100644
index 4f6f2213a..000000000
--- a/implementation/parallel/arrival_sequence.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the arrival sequence from the basic model. *)
-Require Export rt.implementation.basic.arrival_sequence.
\ No newline at end of file
diff --git a/implementation/parallel/job.v b/implementation/parallel/job.v
deleted file mode 100644
index 78b0bd655..000000000
--- a/implementation/parallel/job.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the job from the basic model. *)
-Require Export rt.implementation.basic.job.
\ No newline at end of file
diff --git a/implementation/parallel/task.v b/implementation/parallel/task.v
deleted file mode 100644
index d4eb8e27d..000000000
--- a/implementation/parallel/task.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the task from the basic model. *)
-Require Export rt.implementation.basic.task.
\ No newline at end of file
diff --git a/model/apa/affinity.v b/model/apa/affinity.v
index f819d86a5..3d670dbc8 100644
--- a/model/apa/affinity.v
+++ b/model/apa/affinity.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task
-               rt.model.apa.arrival_sequence rt.model.apa.schedule.
+Require Import rt.model.job rt.model.task rt.model.arrival_sequence.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition and properties about processor affinities. *)
diff --git a/model/apa/arrival_sequence.v b/model/apa/arrival_sequence.v
deleted file mode 100644
index 0ab7d9296..000000000
--- a/model/apa/arrival_sequence.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The arrival sequence remains the same under APA scheduling. *)
-Require Export rt.model.basic.arrival_sequence.
\ No newline at end of file
diff --git a/model/apa/constrained_deadlines.v b/model/apa/constrained_deadlines.v
index 55b1abc63..d4811fd12 100644
--- a/model/apa/constrained_deadlines.v
+++ b/model/apa/constrained_deadlines.v
@@ -1,8 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival
-               rt.model.apa.interference rt.model.apa.affinity
-               rt.model.apa.platform.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/apa/interference.v b/model/apa/interference.v
index f0a2fe842..f566b6553 100644
--- a/model/apa/interference.v
+++ b/model/apa/interference.v
@@ -1,6 +1,8 @@
 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.priority rt.model.apa.workload rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
diff --git a/model/apa/interference_edf.v b/model/apa/interference_edf.v
index c1bb429ec..fcd1ee9df 100644
--- a/model/apa/interference_edf.v
+++ b/model/apa/interference_edf.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival rt.model.apa.interference
-               rt.model.apa.arrival_sequence rt.model.apa.platform
-               rt.model.apa.affinity.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference
+               rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/apa/job.v b/model/apa/job.v
deleted file mode 100644
index 3e6878902..000000000
--- a/model/apa/job.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of a valid job remains the same under APA scheduling. *)
-Require Export rt.model.basic.job.
\ No newline at end of file
diff --git a/model/apa/platform.v b/model/apa/platform.v
index d73433929..3399e330e 100644
--- a/model/apa/platform.v
+++ b/model/apa/platform.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival
-               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/apa/priority.v b/model/apa/priority.v
deleted file mode 100644
index ee2fe4187..000000000
--- a/model/apa/priority.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of priority remains the same under APA scheduling. *)
-Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/apa/response_time.v b/model/apa/response_time.v
deleted file mode 100644
index 06c3c32c6..000000000
--- a/model/apa/response_time.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of response time remains the same under APA scheduling. *)
-Require Export rt.model.basic.response_time.
\ No newline at end of file
diff --git a/model/apa/schedulability.v b/model/apa/schedulability.v
deleted file mode 100644
index db9b150a5..000000000
--- a/model/apa/schedulability.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of schedulability remains the same under APA scheduling. *)
-Require Export rt.model.basic.schedulability.
\ No newline at end of file
diff --git a/model/apa/schedule.v b/model/apa/schedule.v
deleted file mode 100644
index 80aa78b0d..000000000
--- a/model/apa/schedule.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of schedule remains the same under APA scheduling. *)
-Require Export rt.model.basic.schedule.
\ No newline at end of file
diff --git a/model/apa/task.v b/model/apa/task.v
deleted file mode 100644
index 12257fa08..000000000
--- a/model/apa/task.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of a valid task remains the same under APA scheduling. *)
-Require Export rt.model.basic.task.
\ No newline at end of file
diff --git a/model/apa/task_arrival.v b/model/apa/task_arrival.v
deleted file mode 100644
index d7299e014..000000000
--- a/model/apa/task_arrival.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of interarrival times does not change under APA scheduling. *)
-Require Export rt.model.basic.task_arrival.
\ No newline at end of file
diff --git a/model/apa/time.v b/model/apa/time.v
deleted file mode 100644
index 394817a0f..000000000
--- a/model/apa/time.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of time is the same. *)
-Require Export rt.model.basic.time.
\ No newline at end of file
diff --git a/model/apa/workload.v b/model/apa/workload.v
deleted file mode 100644
index b3482234e..000000000
--- a/model/apa/workload.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of workload does not change under APA scheduling. *)
-Require Export rt.model.basic.workload.
\ No newline at end of file
diff --git a/model/basic/arrival_sequence.v b/model/arrival_sequence.v
similarity index 98%
rename from model/basic/arrival_sequence.v
rename to model/arrival_sequence.v
index dcb43d387..a38e3ea8c 100644
--- a/model/basic/arrival_sequence.v
+++ b/model/arrival_sequence.v
@@ -1,4 +1,4 @@
-Require Import rt.util.all rt.model.basic.task rt.model.basic.time.
+Require Import rt.util.all rt.model.task rt.model.time.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* Definitions and properties of job arrival sequences. *)
diff --git a/model/basic/constrained_deadlines.v b/model/global/basic/constrained_deadlines.v
similarity index 98%
rename from model/basic/constrained_deadlines.v
rename to model/global/basic/constrained_deadlines.v
index 04d6105d5..30b843df3 100644
--- a/model/basic/constrained_deadlines.v
+++ b/model/global/basic/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival
-               rt.model.basic.interference rt.model.basic.platform.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
+               rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/basic/interference.v b/model/global/basic/interference.v
similarity index 84%
rename from model/basic/interference.v
rename to model/global/basic/interference.v
index b1d1031be..6998812ec 100644
--- a/model/basic/interference.v
+++ b/model/global/basic/interference.v
@@ -1,55 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.workload.
+Require Import rt.model.task rt.model.job rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
 
   Import Schedule ScheduleOfSporadicTask Priority Workload.
 
-  (* In this section, we define the notion of a possible interfering task. *)
-  Section PossibleInterferingTasks.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> time.
-    Variable task_period: sporadic_task -> time.
-    Variable task_deadline: sporadic_task -> time.
-
-    Section FP.
-
-      (* Assume an FP policy. *)
-      Variable higher_eq_priority: FP_policy sporadic_task.
-
-      (* Let tsk be the task to be analyzed ... *)
-      Variable tsk: sporadic_task.
-
-      (* ...and let tsk_other be another task. *)
-      Variable tsk_other: sporadic_task.
-
-      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
-         with tsk if it is a different task with higher priority. *)
-      Definition higher_priority_task :=
-        higher_eq_priority tsk_other tsk &&
-        (tsk_other != tsk).
-
-    End FP.
-
-    Section JLFP.
-
-      (* Let tsk be the task to be analyzed ... *)
-      Variable tsk: sporadic_task.
-
-      (* ...and let tsk_other be another task. *)
-      Variable tsk_other: sporadic_task.
-
-      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
-         with tsk if it is a different task. *)
-      Definition different_task := tsk_other != tsk.
-
-    End JLFP.
-    
-  End PossibleInterferingTasks.
-  
   Section InterferenceDefs.
 
     Context {sporadic_task: eqType}.
diff --git a/model/basic/interference_edf.v b/model/global/basic/interference_edf.v
similarity index 91%
rename from model/basic/interference_edf.v
rename to model/global/basic/interference_edf.v
index 1058ed3ed..7ff6c14e6 100644
--- a/model/basic/interference_edf.v
+++ b/model/global/basic/interference_edf.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference
-               rt.model.basic.arrival_sequence rt.model.basic.platform.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
+               rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/basic/platform.v b/model/global/basic/platform.v
similarity index 97%
rename from model/basic/platform.v
rename to model/global/basic/platform.v
index d7e31764f..77c7757d7 100644
--- a/model/basic/platform.v
+++ b/model/global/basic/platform.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/basic/schedule.v b/model/global/basic/schedule.v
similarity index 99%
rename from model/basic/schedule.v
rename to model/global/basic/schedule.v
index 59a423fb2..838e491ad 100644
--- a/model/basic/schedule.v
+++ b/model/global/basic/schedule.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all
-               rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
+               rt.model.job rt.model.task rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition, properties and lemmas about schedules. *)
diff --git a/model/jitter/constrained_deadlines.v b/model/global/jitter/constrained_deadlines.v
similarity index 98%
rename from model/jitter/constrained_deadlines.v
rename to model/global/jitter/constrained_deadlines.v
index 807164d5f..33f5977ed 100644
--- a/model/jitter/constrained_deadlines.v
+++ b/model/global/jitter/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival
-               rt.model.jitter.interference rt.model.jitter.platform.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/jitter/interference.v b/model/global/jitter/interference.v
similarity index 97%
rename from model/jitter/interference.v
rename to model/global/jitter/interference.v
index f6ee8eed7..0afd8a122 100644
--- a/model/jitter/interference.v
+++ b/model/global/jitter/interference.v
@@ -1,7 +1,6 @@
-
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.workload.
+Require Import rt.model.task rt.model.priority rt.model.global.workload.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
@@ -11,7 +10,7 @@ Module Interference.
   (* We import some of the basic definitions, but we need to re-define almost everything
      since the definition of backlogged (and thus the definition of interference)
      changes with jitter. *)
-  Require Import rt.model.basic.interference.
+  Require Import rt.model.global.basic.interference.
   Export Interference.
   
   Section InterferenceDefs.
diff --git a/model/jitter/interference_edf.v b/model/global/jitter/interference_edf.v
similarity index 90%
rename from model/jitter/interference_edf.v
rename to model/global/jitter/interference_edf.v
index 6a9d4d1e2..09ada9aa7 100644
--- a/model/jitter/interference_edf.v
+++ b/model/global/jitter/interference_edf.v
@@ -1,7 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference
-               rt.model.jitter.arrival_sequence rt.model.jitter.platform.
+Require Import rt.model.task rt.model.arrival_sequence rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job
+               rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference
+               rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/jitter/job.v b/model/global/jitter/job.v
similarity index 92%
rename from model/jitter/job.v
rename to model/global/jitter/job.v
index 35e395f38..2771fe8bc 100644
--- a/model/jitter/job.v
+++ b/model/global/jitter/job.v
@@ -1,7 +1,7 @@
-Require Import rt.model.jitter.time rt.model.jitter.task.
+Require Import rt.model.time rt.model.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
-Require Export rt.model.basic.job.
+Require Export rt.model.job.
 
 (* Properties of different types of job: *)
 Module JobWithJitter.
diff --git a/model/jitter/platform.v b/model/global/jitter/platform.v
similarity index 97%
rename from model/jitter/platform.v
rename to model/global/jitter/platform.v
index cb916f908..bd8c4a18b 100644
--- a/model/jitter/platform.v
+++ b/model/global/jitter/platform.v
@@ -1,6 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/jitter/schedule.v b/model/global/jitter/schedule.v
similarity index 98%
rename from model/jitter/schedule.v
rename to model/global/jitter/schedule.v
index fdb901671..0a59571db 100644
--- a/model/jitter/schedule.v
+++ b/model/global/jitter/schedule.v
@@ -1,12 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.arrival_sequence.
+Require Import rt.model.task.
+Require Import rt.model.global.jitter.job rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition, properties and lemmas about schedules. *)
 Module ScheduleWithJitter.
 
   (* We import the original schedule module and redefine whatever is required. *)
-  Require Export rt.model.basic.schedule.
+  Require Export rt.model.global.basic.schedule.
   Export ArrivalSequence Schedule.
   
   (* We need to redefine the properties of a job that depend on the arrival time. *)
diff --git a/model/basic/response_time.v b/model/global/response_time.v
similarity index 97%
rename from model/basic/response_time.v
rename to model/global/response_time.v
index 68fd3a16d..f8735ef71 100644
--- a/model/basic/response_time.v
+++ b/model/global/response_time.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition of response-time bound and some simple lemmas. *)
diff --git a/model/basic/schedulability.v b/model/global/schedulability.v
similarity index 98%
rename from model/basic/schedulability.v
rename to model/global/schedulability.v
index 88bdb99d3..69255dce8 100644
--- a/model/basic/schedulability.v
+++ b/model/global/schedulability.v
@@ -1,5 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule.
+Require Import rt.model.job rt.model.task.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
 
 (* Definitions of deadline miss. *)
diff --git a/model/basic/workload.v b/model/global/workload.v
similarity index 94%
rename from model/basic/workload.v
rename to model/global/workload.v
index 78f8f1a60..b762d8d7d 100644
--- a/model/basic/workload.v
+++ b/model/global/workload.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.response_time
-               rt.model.basic.schedulability.
+Require Import rt.model.job rt.model.task rt.model.task_arrival.
+Require Import rt.model.global.schedulability rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module Workload.
diff --git a/model/jitter/arrival_sequence.v b/model/jitter/arrival_sequence.v
deleted file mode 100644
index 316a75b8a..000000000
--- a/model/jitter/arrival_sequence.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* All definitions from arrival sequence can be safely imported. *)
-Require Export rt.model.basic.arrival_sequence.
\ No newline at end of file
diff --git a/model/jitter/priority.v b/model/jitter/priority.v
deleted file mode 100644
index 1a59a29ed..000000000
--- a/model/jitter/priority.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* Because we define EDF using the *actual job arrivals*, we can safely import the original of priority. *)
-Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/jitter/response_time.v b/model/jitter/response_time.v
deleted file mode 100644
index 673085f1b..000000000
--- a/model/jitter/response_time.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Since jitter does not change the notion of response time, we keep
-   the original definitions. *)
-Require Export rt.model.basic.response_time.
\ No newline at end of file
diff --git a/model/jitter/schedulability.v b/model/jitter/schedulability.v
deleted file mode 100644
index 7dfa86aff..000000000
--- a/model/jitter/schedulability.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Jitter doesn't affect the notion of deadline miss, so we can safely
-   import the basic definitions. *)
-Require Export rt.model.basic.schedulability.
\ No newline at end of file
diff --git a/model/jitter/task.v b/model/jitter/task.v
deleted file mode 100644
index 73037fe62..000000000
--- a/model/jitter/task.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Since the worst-case jitter of a task is unbounded, we don't need to
-   define any specific properties for a task with jitter.*)
-Require Export rt.model.basic.task.
\ No newline at end of file
diff --git a/model/jitter/task_arrival.v b/model/jitter/task_arrival.v
deleted file mode 100644
index d2db320ed..000000000
--- a/model/jitter/task_arrival.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Interarrival times are specified by the environment and are based on the
-   original arrival times. We can import the original definitions. *)
-Require Export rt.model.basic.task_arrival.
\ No newline at end of file
diff --git a/model/jitter/time.v b/model/jitter/time.v
deleted file mode 100644
index 06ad193b5..000000000
--- a/model/jitter/time.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* The definition of time is the same. *)
-Require Export rt.model.basic.time.
\ No newline at end of file
diff --git a/model/jitter/workload.v b/model/jitter/workload.v
deleted file mode 100644
index 280cc69eb..000000000
--- a/model/jitter/workload.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* The workload of a task doesn't depend on jitter, so we keep the original definitions. *)
-Require Export rt.model.basic.workload.
\ No newline at end of file
diff --git a/model/basic/job.v b/model/job.v
similarity index 97%
rename from model/basic/job.v
rename to model/job.v
index f2fa98852..db9227f60 100644
--- a/model/basic/job.v
+++ b/model/job.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.model.basic.task.
+Require Import rt.model.time rt.model.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
 (* Properties of different types of job: *)
diff --git a/model/basic/jobin_eqdec.v b/model/jobin_eqdec.v
similarity index 100%
rename from model/basic/jobin_eqdec.v
rename to model/jobin_eqdec.v
diff --git a/model/basic/priority.v b/model/priority.v
similarity index 83%
rename from model/basic/priority.v
rename to model/priority.v
index f2898b518..9dc73ad24 100644
--- a/model/basic/priority.v
+++ b/model/priority.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
+Require Import rt.model.task rt.model.job rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 Set Implicit Arguments.
 
 (* Definitions of FP and JLFP/JLDP priority relations. *)
 Module Priority.
 
-  Import SporadicTaskset Schedule.
+  Import SporadicTaskset ArrivalSequence.
 
   Section PriorityDefs.
 
@@ -247,4 +247,47 @@ Module Priority.
 
   End KnownJLFPPolicies.
 
+  (* In this section, we define the notion of a possible interfering task. *)
+  Section PossibleInterferingTasks.
+
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> time.
+    Variable task_period: sporadic_task -> time.
+    Variable task_deadline: sporadic_task -> time.
+
+    Section FP.
+
+      (* Assume an FP policy. *)
+      Variable higher_eq_priority: FP_policy sporadic_task.
+
+      (* Let tsk be the task to be analyzed ... *)
+      Variable tsk: sporadic_task.
+
+      (* ...and let tsk_other be another task. *)
+      Variable tsk_other: sporadic_task.
+
+      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
+         with tsk if it is a different task with higher priority. *)
+      Definition higher_priority_task :=
+        higher_eq_priority tsk_other tsk &&
+        (tsk_other != tsk).
+
+    End FP.
+
+    Section JLFP.
+
+      (* Let tsk be the task to be analyzed ... *)
+      Variable tsk: sporadic_task.
+
+      (* ...and let tsk_other be another task. *)
+      Variable tsk_other: sporadic_task.
+
+      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
+         with tsk if it is a different task. *)
+      Definition different_task := tsk_other != tsk.
+
+    End JLFP.
+    
+  End PossibleInterferingTasks.  
+
 End Priority.
\ No newline at end of file
diff --git a/model/basic/task.v b/model/task.v
similarity index 98%
rename from model/basic/task.v
rename to model/task.v
index f6c3f0d85..6dee9d6a8 100644
--- a/model/basic/task.v
+++ b/model/task.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.util.all.
+Require Import rt.model.time rt.util.all.
 From mathcomp Require Import ssrnat ssrbool eqtype fintype seq.
 
 (* Attributes of a valid sporadic task. *)
diff --git a/model/basic/task_arrival.v b/model/task_arrival.v
similarity index 90%
rename from model/basic/task_arrival.v
rename to model/task_arrival.v
index 44a769db2..e65ff3794 100644
--- a/model/basic/task_arrival.v
+++ b/model/task_arrival.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
+Require Import rt.model.arrival_sequence rt.model.task rt.model.job.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* Properties of the job arrival. *)
 Module SporadicTaskArrival.
 
-Import SporadicTaskset Schedule.
+Import ArrivalSequence SporadicTaskset.
   
   Section ArrivalModels.
 
diff --git a/model/basic/time.v b/model/time.v
similarity index 100%
rename from model/basic/time.v
rename to model/time.v
-- 
GitLab