diff --git a/classic/analysis/apa/bertogna_edf_comp.v b/classic/analysis/apa/bertogna_edf_comp.v
index c90a956617545ccccc4b27f843bd608ef1ab2585..7ff85d99e53dc0213e1e60930026597570844696 100755
--- a/classic/analysis/apa/bertogna_edf_comp.v
+++ b/classic/analysis/apa/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.apa.bertogna_edf_theory.
+Require Import rt.classic.analysis.apa.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/classic/analysis/apa/bertogna_edf_theory.v b/classic/analysis/apa/bertogna_edf_theory.v
index 3162a16b563ee6450d3c301e62dd7559c7cadff2..7f264ebac8d7c804c8c7f9316894f432ab620057 100644
--- a/classic/analysis/apa/bertogna_edf_theory.v
+++ b/classic/analysis/apa/bertogna_edf_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.interference
-               rt.model.schedule.apa.affinity rt.model.schedule.apa.constrained_deadlines.
-Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_edf.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.platform rt.classic.model.schedule.apa.interference
+               rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.constrained_deadlines.
+Require Import rt.classic.analysis.apa.workload_bound rt.classic.analysis.apa.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/apa/bertogna_fp_comp.v b/classic/analysis/apa/bertogna_fp_comp.v
index a1b9315e19db0981bed0ac98f0892d9421291b61..4d3876d86ef138e83b7b67b1d594d6ea57997c6f 100644
--- a/classic/analysis/apa/bertogna_fp_comp.v
+++ b/classic/analysis/apa/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.apa.bertogna_fp_theory.
+Require Import rt.classic.analysis.apa.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
diff --git a/classic/analysis/apa/bertogna_fp_theory.v b/classic/analysis/apa/bertogna_fp_theory.v
index 76dda042aaf87c897d0909886658067c9bf037b0..956efe77a2dc4e23be3578a35df8208c51d14a90 100644
--- a/classic/analysis/apa/bertogna_fp_theory.v
+++ b/classic/analysis/apa/bertogna_fp_theory.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
-               rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.constrained_deadlines
-               rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.
-Require Import rt.analysis.apa.workload_bound
-               rt.analysis.apa.interference_bound_fp.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.platform rt.classic.model.schedule.apa.constrained_deadlines
+               rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.affinity.
+Require Import rt.classic.analysis.apa.workload_bound
+               rt.classic.analysis.apa.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/apa/interference_bound.v b/classic/analysis/apa/interference_bound.v
index 0b410d23ca94fdc3352cc686a366079bb13689d9..6387c195eeb1bfacce4ce957c0c3059ca03e7cd3 100644
--- a/classic/analysis/apa/interference_bound.v
+++ b/classic/analysis/apa/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.analysis.apa.workload_bound.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.analysis.apa.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/classic/analysis/apa/interference_bound_edf.v b/classic/analysis/apa/interference_bound_edf.v
index 76c56e8beda4243a244c68254fdbbef917e1fee8..6728d41077368f8637fc69b7b08ef70f51b9b111 100644
--- a/classic/analysis/apa/interference_bound_edf.v
+++ b/classic/analysis/apa/interference_bound_edf.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.platform rt.model.schedule.apa.interference
-               rt.model.schedule.apa.interference_edf rt.model.schedule.apa.affinity.
-Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.platform rt.classic.model.schedule.apa.interference
+               rt.classic.model.schedule.apa.interference_edf rt.classic.model.schedule.apa.affinity.
+Require Import rt.classic.analysis.apa.workload_bound rt.classic.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 (* In this file, we define the reduction-based interference bound for APA
diff --git a/classic/analysis/apa/interference_bound_fp.v b/classic/analysis/apa/interference_bound_fp.v
index 12d3937364628e2427e938285abb103e190c8f0f..1b911e9f745180a66a9dbeb956e69d7e9145aa8c 100644
--- a/classic/analysis/apa/interference_bound_fp.v
+++ b/classic/analysis/apa/interference_bound_fp.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.
-Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.affinity.
+Require Import rt.classic.analysis.apa.workload_bound rt.classic.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/classic/analysis/apa/workload_bound.v b/classic/analysis/apa/workload_bound.v
index 78ac1dc0f6dd5862b467ad109309ab85fdf4d35c..52b553271fcc9e1def20eb9164d15085cb753a20 100644
--- a/classic/analysis/apa/workload_bound.v
+++ b/classic/analysis/apa/workload_bound.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
-               rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/classic/analysis/global/basic/bertogna_edf_comp.v b/classic/analysis/global/basic/bertogna_edf_comp.v
index 9e4b91ebf5a135e20a9d91916c02073488fd87f0..807c624d8bc6a40728b36fd75c2c9e89c99f999e 100755
--- a/classic/analysis/global/basic/bertogna_edf_comp.v
+++ b/classic/analysis/global/basic/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.basic.bertogna_edf_theory.
+Require Import rt.classic.analysis.global.basic.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/classic/analysis/global/basic/bertogna_edf_theory.v b/classic/analysis/global/basic/bertogna_edf_theory.v
index b6bcc8a2b408552fb5ebbe36508f6c2d1d6058ce..f57bb761d8c5223f3df3b26efb9e932dd4b57c26 100644
--- a/classic/analysis/global/basic/bertogna_edf_theory.v
+++ b/classic/analysis/global/basic/bertogna_edf_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
-               rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.constrained_deadlines.
-Require Import rt.analysis.global.basic.workload_bound rt.analysis.global.basic.interference_bound_edf.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.interference rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.constrained_deadlines.
+Require Import rt.classic.analysis.global.basic.workload_bound rt.classic.analysis.global.basic.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/global/basic/bertogna_fp_comp.v b/classic/analysis/global/basic/bertogna_fp_comp.v
index c9114c22e6ad6193390f16df39895750485524a4..6e330d4a9e635fde0bb939001bf3e977be8a9588 100644
--- a/classic/analysis/global/basic/bertogna_fp_comp.v
+++ b/classic/analysis/global/basic/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.basic.bertogna_fp_theory.
+Require Import rt.classic.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/classic/analysis/global/basic/bertogna_fp_theory.v b/classic/analysis/global/basic/bertogna_fp_theory.v
index bd4c074f074d2d757e2f1c86cb941b057ddfb56e..0b2e63e2bae8a8638666dd9d662cdb5ae066c9a1 100644
--- a/classic/analysis/global/basic/bertogna_fp_theory.v
+++ b/classic/analysis/global/basic/bertogna_fp_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
-               rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.constrained_deadlines rt.model.schedule.global.basic.interference.
-Require Import rt.analysis.global.basic.workload_bound
-               rt.analysis.global.basic.interference_bound_fp.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.constrained_deadlines rt.classic.model.schedule.global.basic.interference.
+Require Import rt.classic.analysis.global.basic.workload_bound
+               rt.classic.analysis.global.basic.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/basic/interference_bound.v b/classic/analysis/global/basic/interference_bound.v
index 5a0e6b812b16b13db713a239b4d608aeea7a2c58..47e7db70a53f8a488138c71e336089dea4ebd08d 100644
--- a/classic/analysis/global/basic/interference_bound.v
+++ b/classic/analysis/global/basic/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.analysis.global.basic.workload_bound.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.analysis.global.basic.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/classic/analysis/global/basic/interference_bound_edf.v b/classic/analysis/global/basic/interference_bound_edf.v
index 2b6cf8a647686cd8788684b2888e788cb67ea352..1e8371a3915ff91e45f0c99ce086bd2a63043034 100644
--- a/classic/analysis/global/basic/interference_bound_edf.v
+++ b/classic/analysis/global/basic/interference_bound_edf.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.interference_edf.
-Require Import rt.analysis.global.basic.workload_bound
-               rt.analysis.global.basic.interference_bound.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.workload
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.interference rt.classic.model.schedule.global.basic.interference_edf.
+Require Import rt.classic.analysis.global.basic.workload_bound
+               rt.classic.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.
diff --git a/classic/analysis/global/basic/interference_bound_fp.v b/classic/analysis/global/basic/interference_bound_fp.v
index 5330503579af98e24933d40b6d5497e90f25691d..d8ae5129fff6c9af3aa6cc48c59495d0123b8f72 100644
--- a/classic/analysis/global/basic/interference_bound_fp.v
+++ b/classic/analysis/global/basic/interference_bound_fp.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference.
-Require Import rt.analysis.global.basic.workload_bound
-               rt.analysis.global.basic.interference_bound.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference.
+Require Import rt.classic.analysis.global.basic.workload_bound
+               rt.classic.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/classic/analysis/global/basic/workload_bound.v b/classic/analysis/global/basic/workload_bound.v
index 4d26cef059eaaf4e50f927c7716ef27e55dd88c2..9e88a99bf3dcba845ecb7c02d9d782cade8ff957 100644
--- a/classic/analysis/global/basic/workload_bound.v
+++ b/classic/analysis/global/basic/workload_bound.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/classic/analysis/global/jitter/bertogna_edf_comp.v b/classic/analysis/global/jitter/bertogna_edf_comp.v
index fbd879c4b786eed2b3c97e79a0a68a397b3fc951..d7c1a2537fc52cbab21c535d0097b96c65cc43ad 100755
--- a/classic/analysis/global/jitter/bertogna_edf_comp.v
+++ b/classic/analysis/global/jitter/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.jitter.bertogna_edf_theory.
+Require Import rt.classic.analysis.global.jitter.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/classic/analysis/global/jitter/bertogna_edf_theory.v b/classic/analysis/global/jitter/bertogna_edf_theory.v
index 94f3435c6ab134b5a062782b8904f60e581347a2..0bbbab1dba7d5fa8b3247044d936e708db1bc02d 100644
--- a/classic/analysis/global/jitter/bertogna_edf_theory.v
+++ b/classic/analysis/global/jitter/bertogna_edf_theory.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
-               rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.platform rt.model.schedule.global.jitter.interference
-               rt.model.schedule.global.jitter.constrained_deadlines.
-Require Import rt.analysis.global.jitter.workload_bound
-               rt.analysis.global.jitter.interference_bound_edf.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.platform rt.classic.model.schedule.global.jitter.interference
+               rt.classic.model.schedule.global.jitter.constrained_deadlines.
+Require Import rt.classic.analysis.global.jitter.workload_bound
+               rt.classic.analysis.global.jitter.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDFJitter.
diff --git a/classic/analysis/global/jitter/bertogna_fp_comp.v b/classic/analysis/global/jitter/bertogna_fp_comp.v
index fd69f2d63c4ca61c664ab05f826791031115e3ec..2a59587ab41d57f87dcaa73b2556d349e1cbba2b 100644
--- a/classic/analysis/global/jitter/bertogna_fp_comp.v
+++ b/classic/analysis/global/jitter/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.jitter.bertogna_fp_theory.
+Require Import rt.classic.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/classic/analysis/global/jitter/bertogna_fp_theory.v b/classic/analysis/global/jitter/bertogna_fp_theory.v
index df61fbd32f9a1f7eb5259d138f7cd7e63e0b8d5e..0b23970336fb54c49dc90f7e3df9197cd92399ff 100644
--- a/classic/analysis/global/jitter/bertogna_fp_theory.v
+++ b/classic/analysis/global/jitter/bertogna_fp_theory.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.interference
-               rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.platform
-               rt.model.schedule.global.jitter.constrained_deadlines.
-Require Import rt.analysis.global.jitter.workload_bound
-               rt.analysis.global.jitter.interference_bound_fp.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.interference
+               rt.classic.model.schedule.global.jitter.schedule rt.classic.model.schedule.global.jitter.platform
+               rt.classic.model.schedule.global.jitter.constrained_deadlines.
+Require Import rt.classic.analysis.global.jitter.workload_bound
+               rt.classic.analysis.global.jitter.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/jitter/interference_bound.v b/classic/analysis/global/jitter/interference_bound.v
index ee67171469c820c4dcece7c7abcb0589f8a20c8e..32c71fa998f615f7cfdfc66ab8b061ea8f431f02 100644
--- a/classic/analysis/global/jitter/interference_bound.v
+++ b/classic/analysis/global/jitter/interference_bound.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.priority.
-Require Import rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.interference.
-Require Import rt.analysis.global.jitter.workload_bound.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.jitter.schedule rt.classic.model.schedule.global.jitter.interference.
+Require Import rt.classic.analysis.global.jitter.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundJitter.
diff --git a/classic/analysis/global/jitter/interference_bound_edf.v b/classic/analysis/global/jitter/interference_bound_edf.v
index 266cd3e971732c908496159336634a480cb06a98..2c851f9ff3ba9909ba5a571110391b11e005cefd 100644
--- a/classic/analysis/global/jitter/interference_bound_edf.v
+++ b/classic/analysis/global/jitter/interference_bound_edf.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.platform rt.model.schedule.global.jitter.interference
-               rt.model.schedule.global.jitter.interference_edf.
-Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.workload
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.platform rt.classic.model.schedule.global.jitter.interference
+               rt.classic.model.schedule.global.jitter.interference_edf.
+Require Import rt.classic.analysis.global.jitter.workload_bound rt.classic.analysis.global.jitter.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDFJitter.
diff --git a/classic/analysis/global/jitter/interference_bound_fp.v b/classic/analysis/global/jitter/interference_bound_fp.v
index e0ead057bc492a58b73c77b7a00e8741b2947cd4..2c4d167fe4db6daa6b6bb1cea7f91ca78f938295 100644
--- a/classic/analysis/global/jitter/interference_bound_fp.v
+++ b/classic/analysis/global/jitter/interference_bound_fp.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.jitter.schedule rt.model.schedule.global.jitter.interference.
-Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.jitter.schedule rt.classic.model.schedule.global.jitter.interference.
+Require Import rt.classic.analysis.global.jitter.workload_bound rt.classic.analysis.global.jitter.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/classic/analysis/global/jitter/workload_bound.v b/classic/analysis/global/jitter/workload_bound.v
index 95ba570c7e9e05da3246a73458c2f985f9ba8c4e..17cb5adb43cae5cd53492e1cd58f4f9363dbdee5 100644
--- a/classic/analysis/global/jitter/workload_bound.v
+++ b/classic/analysis/global/jitter/workload_bound.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBoundJitter.
diff --git a/classic/analysis/global/parallel/bertogna_edf_comp.v b/classic/analysis/global/parallel/bertogna_edf_comp.v
index 520341bd78a7f62341c1bc83b08192e44f0386a2..142dc3036da82e20abdd4760f9f65698072e35a6 100755
--- a/classic/analysis/global/parallel/bertogna_edf_comp.v
+++ b/classic/analysis/global/parallel/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.parallel.bertogna_edf_theory.
+Require Import rt.classic.analysis.global.parallel.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/classic/analysis/global/parallel/bertogna_edf_theory.v b/classic/analysis/global/parallel/bertogna_edf_theory.v
index 1967f3ca77d06b0d49eb7a449012087d1134b772..236496e826fd20dc8f25c3795fcb31351f0e260c 100644
--- a/classic/analysis/global/parallel/bertogna_edf_theory.v
+++ b/classic/analysis/global/parallel/bertogna_edf_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
-               rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference
-               rt.model.schedule.global.basic.platform.
-Require Import rt.analysis.global.parallel.workload_bound
-               rt.analysis.global.parallel.interference_bound_edf.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference
+               rt.classic.model.schedule.global.basic.platform.
+Require Import rt.classic.analysis.global.parallel.workload_bound
+               rt.classic.analysis.global.parallel.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/global/parallel/bertogna_fp_comp.v b/classic/analysis/global/parallel/bertogna_fp_comp.v
index b398a1e7847b157064a06cd13471ca6e603f8d63..a4fb624a15ea2cd9fc9f9af321ea81748583baed 100644
--- a/classic/analysis/global/parallel/bertogna_fp_comp.v
+++ b/classic/analysis/global/parallel/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.global.parallel.bertogna_fp_theory.
+Require Import rt.classic.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/classic/analysis/global/parallel/bertogna_fp_theory.v b/classic/analysis/global/parallel/bertogna_fp_theory.v
index f163f51e0ce0635fe950ccbbacf4ec2a0ebf3189..ead6a9d23bb1639aae32b58cfc8fd3c685953a96 100644
--- a/classic/analysis/global/parallel/bertogna_fp_theory.v
+++ b/classic/analysis/global/parallel/bertogna_fp_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival
-        rt.model.priority.
-Require Import rt.model.schedule.global.workload rt.model.schedule.global.schedulability
-               rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.constrained_deadlines rt.model.schedule.global.basic.interference.
-Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound_fp.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival
+        rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
+               rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.constrained_deadlines rt.classic.model.schedule.global.basic.interference.
+Require Import rt.classic.analysis.global.parallel.workload_bound rt.classic.analysis.global.parallel.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/parallel/interference_bound.v b/classic/analysis/global/parallel/interference_bound.v
index d6d968d83c07daf73663c9c6f586cf95336965ae..1f9c29f686ef95839f43552a31c87647416467f9 100644
--- a/classic/analysis/global/parallel/interference_bound.v
+++ b/classic/analysis/global/parallel/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.analysis.global.parallel.workload_bound.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.analysis.global.parallel.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/classic/analysis/global/parallel/interference_bound_edf.v b/classic/analysis/global/parallel/interference_bound_edf.v
index 638d24a56b64d608b8551b31fac05c1beeec35f6..a59a5a6f0d05a2af0c77e20fb8fce6c5a0b7fad8 100644
--- a/classic/analysis/global/parallel/interference_bound_edf.v
+++ b/classic/analysis/global/parallel/interference_bound_edf.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.global.basic.interference rt.model.schedule.global.basic.interference_edf.
-Require Import rt.analysis.global.parallel.workload_bound
-               rt.analysis.global.parallel.interference_bound.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.workload
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.interference rt.classic.model.schedule.global.basic.interference_edf.
+Require Import rt.classic.analysis.global.parallel.workload_bound
+               rt.classic.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.
diff --git a/classic/analysis/global/parallel/interference_bound_fp.v b/classic/analysis/global/parallel/interference_bound_fp.v
index eee8ef10e32e6a41a25c9ad894340d949701510f..d4ac13df1a3b4c7e1593188c9019a9630fff1278 100644
--- a/classic/analysis/global/parallel/interference_bound_fp.v
+++ b/classic/analysis/global/parallel/interference_bound_fp.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference.
-Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference.
+Require Import rt.classic.analysis.global.parallel.workload_bound rt.classic.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/classic/analysis/global/parallel/workload_bound.v b/classic/analysis/global/parallel/workload_bound.v
index 763484372db5e52cb6c0029936d3a1e8e8046100..68d0d1dc3c4b696f2b71b811667f5f4537bba03f 100644
--- a/classic/analysis/global/parallel/workload_bound.v
+++ b/classic/analysis/global/parallel/workload_bound.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.response_time rt.model.schedule.global.workload
-               rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.workload
+               rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/classic/analysis/uni/arrival_curves/workload_bound.v b/classic/analysis/uni/arrival_curves/workload_bound.v
index e0ac7c1bee24033c74acc623edd48f25fa4b4c86..fd90c259e530f5d941428ace195eef642d9ffbc3 100644
--- a/classic/analysis/uni/arrival_curves/workload_bound.v
+++ b/classic/analysis/uni/arrival_curves/workload_bound.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule.
-Require Import rt.model.arrival.curves.bounds. 
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.curves.bounds. 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 Module MaxArrivalsWorkloadBound.
diff --git a/classic/analysis/uni/basic/fp_rta_comp.v b/classic/analysis/uni/basic/fp_rta_comp.v
index a74f4ef95dafc43f7936e577a76b80ba6e08dd39..97cc98f2cf96779d620c7d535dc3e04d03019bbc 100644
--- a/classic/analysis/uni/basic/fp_rta_comp.v
+++ b/classic/analysis/uni/basic/fp_rta_comp.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.basic.platform.
-Require Import rt.analysis.uni.basic.workload_bound_fp rt.analysis.uni.basic.fp_rta_theory.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.analysis.uni.basic.workload_bound_fp rt.classic.analysis.uni.basic.fp_rta_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
 
 Module ResponseTimeIterationFP.
diff --git a/classic/analysis/uni/basic/fp_rta_theory.v b/classic/analysis/uni/basic/fp_rta_theory.v
index 262c13ff0224a045d6720320e199fa7951bbe8fd..062de39de47618149cff9abf5701bde17d91dc2a 100644
--- a/classic/analysis/uni/basic/fp_rta_theory.v
+++ b/classic/analysis/uni/basic/fp_rta_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival
-               rt.model.arrival.basic.arrival_bounds.
-Require Import rt.model.schedule.uni.schedule_of_task rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time
-               rt.model.schedule.uni.service.
-Require Import rt.model.schedule.uni.limited.busy_interval rt.model.schedule.uni.basic.platform.
-Require Import rt.analysis.uni.basic.workload_bound_fp.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.arrival.basic.arrival_bounds.
+Require Import rt.classic.model.schedule.uni.schedule_of_task rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.response_time
+               rt.classic.model.schedule.uni.service.
+Require Import rt.classic.model.schedule.uni.limited.busy_interval rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.analysis.uni.basic.workload_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/uni/basic/tdma_rta_theory.v b/classic/analysis/uni/basic/tdma_rta_theory.v
index c71832679ef8d51d801839839870b63db430fe2e..5e7c40462e61eb0d3df709460b1ede7ab6a7301f 100644
--- a/classic/analysis/uni/basic/tdma_rta_theory.v
+++ b/classic/analysis/uni/basic/tdma_rta_theory.v
@@ -1,13 +1,13 @@
 Require Import Arith.
 Require Import  rt.util.all
-                rt.model.arrival.basic.job
-                rt.model.arrival.basic.task_arrival
-                rt.model.schedule.uni.schedulability
-                rt.model.schedule.uni.schedule_of_task 
-                rt.model.schedule.uni.response_time
-                rt.analysis.uni.basic.tdma_wcrt_analysis.
-Require Import  rt.model.schedule.uni.basic.platform_tdma
-                rt.model.schedule.uni.end_time.
+                rt.classic.model.arrival.basic.job
+                rt.classic.model.arrival.basic.task_arrival
+                rt.classic.model.schedule.uni.schedulability
+                rt.classic.model.schedule.uni.schedule_of_task 
+                rt.classic.model.schedule.uni.response_time
+                rt.classic.analysis.uni.basic.tdma_wcrt_analysis.
+Require Import  rt.classic.model.schedule.uni.basic.platform_tdma
+                rt.classic.model.schedule.uni.end_time.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
 
 Set Bullet Behavior "Strict Subproofs".
diff --git a/classic/analysis/uni/basic/tdma_wcrt_analysis.v b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
index 54845225ac78b170cf7996f81626a82656484794..b0e04c30344dd98459f53fefd49d6a663f747b56 100644
--- a/classic/analysis/uni/basic/tdma_wcrt_analysis.v
+++ b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
@@ -1,12 +1,12 @@
 Require Import Arith Omega Nat.
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.schedule.uni.schedulability
-               rt.model.schedule.uni.schedule_of_task 
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.basic.platform_tdma
-               rt.model.schedule.uni.end_time.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.schedule.uni.schedulability
+               rt.classic.model.schedule.uni.schedule_of_task 
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.basic.platform_tdma
+               rt.classic.model.schedule.uni.end_time.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
 
 Set Bullet Behavior "Strict Subproofs".
diff --git a/classic/analysis/uni/basic/workload_bound_fp.v b/classic/analysis/uni/basic/workload_bound_fp.v
index de92fb9803dccdf616554939c90d4c3f955143ba..af0057af6bd6c28507c3e5ddd9d4be91f7952fc0 100644
--- a/classic/analysis/uni/basic/workload_bound_fp.v
+++ b/classic/analysis/uni/basic/workload_bound_fp.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority
-               rt.model.arrival.basic.task_arrival rt.model.arrival.basic.arrival_bounds.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival rt.classic.model.arrival.basic.arrival_bounds.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.workload.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
 
 Module WorkloadBoundFP.
diff --git a/classic/analysis/uni/jitter/fp_rta_comp.v b/classic/analysis/uni/jitter/fp_rta_comp.v
index 3368541bc731ec966c823ba3e6e88da69df5eb2a..936759c40691a862e3082439fb181806f2c5f72b 100644
--- a/classic/analysis/uni/jitter/fp_rta_comp.v
+++ b/classic/analysis/uni/jitter/fp_rta_comp.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.task.
-Require Import rt.model.arrival.jitter.job rt.model.arrival.jitter.arrival_sequence
-               rt.model.arrival.jitter.task_arrival.
-Require Import rt.model.schedule.uni.schedulability
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.jitter.schedule rt.model.schedule.uni.jitter.platform.
-Require Import rt.analysis.uni.jitter.workload_bound_fp rt.analysis.uni.jitter.fp_rta_theory.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.arrival.jitter.job rt.classic.model.arrival.jitter.arrival_sequence
+               rt.classic.model.arrival.jitter.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedulability
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.jitter.schedule rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.analysis.uni.jitter.workload_bound_fp rt.classic.analysis.uni.jitter.fp_rta_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
 
 Module ResponseTimeIterationFP.
diff --git a/classic/analysis/uni/jitter/fp_rta_theory.v b/classic/analysis/uni/jitter/fp_rta_theory.v
index 73069b6f6926be0be6ee49326a128db0dae25c1c..b9906d61d771ad156fae60eced3d5e11edd20623 100644
--- a/classic/analysis/uni/jitter/fp_rta_theory.v
+++ b/classic/analysis/uni/jitter/fp_rta_theory.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.task.
-Require Import rt.model.arrival.jitter.job rt.model.arrival.jitter.task_arrival
-               rt.model.arrival.jitter.arrival_sequence rt.model.arrival.jitter.arrival_bounds.
-Require Import rt.model.schedule.uni.schedule_of_task rt.model.schedule.uni.service
-               rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.busy_interval
-               rt.model.schedule.uni.jitter.platform.
-Require Import rt.analysis.uni.jitter.workload_bound_fp.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.arrival.jitter.job rt.classic.model.arrival.jitter.task_arrival
+               rt.classic.model.arrival.jitter.arrival_sequence rt.classic.model.arrival.jitter.arrival_bounds.
+Require Import rt.classic.model.schedule.uni.schedule_of_task rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.busy_interval
+               rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.analysis.uni.jitter.workload_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/analysis/uni/jitter/workload_bound_fp.v b/classic/analysis/uni/jitter/workload_bound_fp.v
index 1e5c9358076424f18a4623a32ccb291ff6a71c25..032117fbef00f71b85983831f919587e92a10ab2 100644
--- a/classic/analysis/uni/jitter/workload_bound_fp.v
+++ b/classic/analysis/uni/jitter/workload_bound_fp.v
@@ -1,10 +1,10 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.arrival.jitter.job
-               rt.model.arrival.jitter.task_arrival
-               rt.model.arrival.jitter.arrival_bounds.
-Require Import rt.model.schedule.uni.workload.
-Require Import rt.model.schedule.uni.jitter.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.arrival.jitter.job
+               rt.classic.model.arrival.jitter.task_arrival
+               rt.classic.model.arrival.jitter.arrival_bounds.
+Require Import rt.classic.model.schedule.uni.workload.
+Require Import rt.classic.model.schedule.uni.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
 
 (* In this file, we define the workload bound for jitter-aware FP scheduling. *)
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule.v
index 00494ad4c13f7dc0979869348f84340b2ffcd808..38f949f4e713223653f77a741444c87e62f664a1 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.jitter.schedule.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.jitter.schedule.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* In this file, we formalize a reduction from a suspension-aware schedule
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
index b0be1d89a8a74f8e4b61f8586737945246d3a299..4aa4d6d280b74f425f36467598316a91747c626c 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
@@ -1,20 +1,20 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
-               rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.valid_schedule
-               rt.model.schedule.uni.jitter.platform.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.valid_schedule
-               rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task
+               rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.valid_schedule
+               rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.valid_schedule
+               rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* In this file, we prove several properties about the constructed jitter-aware schedule. *)
@@ -67,7 +67,7 @@ Module JitterScheduleProperties.
     Variable job_suspension_duration: job_suspension Job.
       
     (* Next, consider any valid suspension-aware schedule of this arrival sequence.
-       (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+       (Note: see rt.classic.model.schedule.uni.susp.valid_schedule.v for details) *)
     Variable sched_susp: schedule Job.
     Hypothesis H_valid_schedule:
       valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
index 6bf7db9a9e8a84ac2080cf5a38234f8e0e7bb2e3..90435e688b378bbe050a9cc522ce7cbddea1942f 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
@@ -1,21 +1,21 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
-               rt.model.arrival.basic.task_arrival
-               rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.platform.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.platform
-               rt.model.schedule.uni.susp.valid_schedule.
-Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
-               rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.platform
+               rt.classic.model.schedule.uni.susp.valid_schedule.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* In this file, we compare the service received by the analyzed job j after
@@ -85,7 +85,7 @@ Module JitterScheduleService.
     Variable job_suspension_duration: job_suspension Job.
 
     (* Next, consider any valid suspension-aware schedule of this arrival sequence.
-       (Note: see definition in rt.model.schedule.uni.susp.valid_schedule.v) *)
+       (Note: see definition in rt.classic.model.schedule.uni.susp.valid_schedule.v) *)
     Variable sched_susp: schedule Job.
     Hypothesis H_valid_schedule:
       valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
@@ -101,7 +101,7 @@ Module JitterScheduleService.
     
     (* Recall that we are going to analyze the response time of some job after
        applying the reduction to the jitter-aware schedule as defined in
-       rt.analysis.uni.susp.dynamic.jitter.jitter_schedule. *)
+       rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule. *)
        
     (* Let j be the job to be analyzed. *)
     Variable j: Job.
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
index 4500ed1c1484696fdae72ec9ea155f69849c9fc6..46d1b6278c787549853daf5ef3db120e46ee7e3f 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.jitter.schedule.
-Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.jitter.schedule.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* In this file we construct a jitter-aware task set that contains the
diff --git a/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v b/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
index aadfaeda9ee6ae7c029669a7a7e5b190e18f8f20..16f806e25b96142e68232a259dc9ef10e703fb1e 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
@@ -1,21 +1,21 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
-               rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task_arrival.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.platform.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.valid_schedule
-               rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
-               rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties
-               rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service
-               rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task
+               rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.schedulability rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.valid_schedule
+               rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_service
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* In this file, we determine task response-time bounds in suspension-aware
@@ -87,7 +87,7 @@ Module RTAByReduction.
       forall j, arrives_in arr_seq j -> job_cost j > 0.
     
     (* Next, consider any valid suspension-aware schedule of this arrival sequence.
-       (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+       (Note: see rt.classic.model.schedule.uni.susp.valid_schedule.v for details) *)
     Variable sched_susp: schedule Job.
     Hypothesis H_valid_schedule:
       valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
diff --git a/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v b/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
index f16e79e95927c739d252ebdf4c605b03cab0fa5d..edc275b175e4959f668632e7e23925a49964fbb0 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
@@ -1,16 +1,16 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job
-               rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.platform
-               rt.model.schedule.uni.susp.valid_schedule.
-Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
-               rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
-Require Import rt.analysis.uni.susp.sustainability.singlecost.reduction
-               rt.analysis.uni.susp.sustainability.singlecost.reduction_properties.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.platform
+               rt.classic.model.schedule.uni.susp.valid_schedule.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
+Require Import rt.classic.analysis.uni.susp.sustainability.singlecost.reduction
+               rt.classic.analysis.uni.susp.sustainability.singlecost.reduction_properties.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file we prove that the jitter-aware schedule sched_jitter used in the
@@ -74,7 +74,7 @@ Module TaskSetMembership.
                                       job_suspension_duration.
     
     (* Next, consider any valid suspension-aware schedule of this arrival sequence.
-       (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+       (Note: see rt.classic.model.schedule.uni.susp.valid_schedule.v for details) *)
     Variable sched_susp: schedule Job.
     Hypothesis H_valid_schedule:
       valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
diff --git a/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v b/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
index b16172b1110df6e0825e7928ffa5a78b287fbd71..1655d5174c135084551b347cd82e7c942955d391 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.susp.schedule rt.model.schedule.uni.susp.platform
-               rt.model.schedule.uni.susp.valid_schedule.
-Require Import rt.model.schedule.uni.jitter.valid_schedule.
-Require Import rt.analysis.uni.susp.dynamic.jitter.rta_by_reduction
-               rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation
-               rt.analysis.uni.susp.dynamic.jitter.taskset_membership.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.susp.schedule rt.classic.model.schedule.uni.susp.platform
+               rt.classic.model.schedule.uni.susp.valid_schedule.
+Require Import rt.classic.model.schedule.uni.jitter.valid_schedule.
+Require Import rt.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction
+               rt.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation
+               rt.classic.analysis.uni.susp.dynamic.jitter.taskset_membership.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file we use the reduction to jitter-aware schedule to analyze
diff --git a/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v b/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
index d6c9c49436dd02a0b7d5aa6acf70770a0557196c..6a595095399eb52fe37febad2b63178482b3a0ec 100644
--- a/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
+++ b/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence
-               rt.model.priority rt.model.suspension rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.basic.fp_rta_comp.
-Require Import rt.analysis.uni.susp.dynamic.oblivious.reduction.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority rt.classic.model.suspension rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.basic.fp_rta_comp.
+Require Import rt.classic.analysis.uni.susp.dynamic.oblivious.reduction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module SuspensionObliviousFP.
diff --git a/classic/analysis/uni/susp/dynamic/oblivious/reduction.v b/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
index e956170578754ee78edbc49a069f3de6ea1dadf2..7cacfe2db0a660a2ee4715a512ed13685ff93a1b 100644
--- a/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
+++ b/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence
-               rt.model.priority rt.model.suspension.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.model.schedule.uni.basic.platform.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule rt.model.schedule.uni.susp.platform.
-Require Import rt.model.schedule.uni.transformation.construction.
-Require Import rt.implementation.uni.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
+Require Import rt.classic.implementation.uni.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 Module ReductionToBasicSchedule.
diff --git a/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v b/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
index 44d78e7ee59b74143fca70654e2fc64300b0a7aa..eceeb78d62950a6cb2796e99b70dea7be8fb3cc9 100644
--- a/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
+++ b/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
@@ -1,16 +1,16 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.response_time
-               rt.model.schedule.uni.sustainability.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.valid_schedule
-               rt.model.schedule.uni.susp.build_suspension_table
-               rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.susp.sustainability.allcosts.reduction
-               rt.analysis.uni.susp.sustainability.allcosts.reduction_properties.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.response_time
+               rt.classic.model.schedule.uni.sustainability.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.valid_schedule
+               rt.classic.model.schedule.uni.susp.build_suspension_table
+               rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.susp.sustainability.allcosts.reduction
+               rt.classic.analysis.uni.susp.sustainability.allcosts.reduction_properties.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/analysis/uni/susp/sustainability/allcosts/reduction.v b/classic/analysis/uni/susp/sustainability/allcosts/reduction.v
index 220ee451ab5fc862f2b3d82dbc0005a1420643ac..e5943cc33060e73d647d5678298e468a30775190 100644
--- a/classic/analysis/uni/susp/sustainability/allcosts/reduction.v
+++ b/classic/analysis/uni/susp/sustainability/allcosts/reduction.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.platform
-               rt.model.schedule.uni.susp.build_suspension_table.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.platform
+               rt.classic.model.schedule.uni.susp.build_suspension_table.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
 
 (* In this file, we prove that uniprocessor suspension-aware scheduling is
diff --git a/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v b/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
index 19420efb329930ce7b6316818076e7569ed9fa6f..8a69b115a58bd6fe6086f9f46d2fd78d1a4a7213 100644
--- a/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
+++ b/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.valid_schedule
-               rt.model.schedule.uni.susp.build_suspension_table
-               rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.susp.sustainability.allcosts.reduction.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.valid_schedule
+               rt.classic.model.schedule.uni.susp.build_suspension_table
+               rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.susp.sustainability.allcosts.reduction.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/analysis/uni/susp/sustainability/singlecost/reduction.v b/classic/analysis/uni/susp/sustainability/singlecost/reduction.v
index ace08f94e20234d9e57c4e697af489e995d69df8..ff5fa16df2ccf3b70c2373035095f3f9aa888bdb 100644
--- a/classic/analysis/uni/susp/sustainability/singlecost/reduction.v
+++ b/classic/analysis/uni/susp/sustainability/singlecost/reduction.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.schedule.uni.susp.schedule.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.schedule.uni.susp.schedule.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* In this file, we propose a reduction that converts a suspension-aware
diff --git a/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
index 724974ca172c5873b283612dcf8516b1cf5b9180..d89cc2dbd29a556a95628ede7fa9beeda25f6636 100644
--- a/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
+++ b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.susp.suspension_intervals
-               rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.platform.
-Require Import rt.analysis.uni.susp.sustainability.singlecost.reduction.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals
+               rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.analysis.uni.susp.sustainability.singlecost.reduction.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/implementation/apa/arrival_sequence.v b/classic/implementation/apa/arrival_sequence.v
index 6c68acbe738b107b202ff68f721eb875b3156236..7616487841823174ff8c22fb3b9b69adb603c01b 100644
--- a/classic/implementation/apa/arrival_sequence.v
+++ b/classic/implementation/apa/arrival_sequence.v
@@ -1,7 +1,7 @@
 (* We can reuse the.apa definition of periodic arrival sequence. *)
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
-Require Import rt.implementation.apa.task rt.implementation.apa.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.implementation.apa.task rt.classic.implementation.apa.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/classic/implementation/apa/bertogna_edf_example.v b/classic/implementation/apa/bertogna_edf_example.v
index ebf1a1a3a2082c6e468e4ce5f52fe8ef043f0e9d..f5dfc1e2c5650d2da9d7b8d35ce1fff41c5a82fb 100644
--- a/classic/implementation/apa/bertogna_edf_example.v
+++ b/classic/implementation/apa/bertogna_edf_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference rt.model.schedule.apa.platform.
-Require Import rt.analysis.apa.workload_bound
-               rt.analysis.apa.interference_bound_edf
-               rt.analysis.apa.bertogna_edf_comp.
-Require Import rt.implementation.apa.job
-               rt.implementation.apa.task
-               rt.implementation.apa.schedule
-               rt.implementation.apa.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.platform.
+Require Import rt.classic.analysis.apa.workload_bound
+               rt.classic.analysis.apa.interference_bound_edf
+               rt.classic.analysis.apa.bertogna_edf_comp.
+Require Import rt.classic.implementation.apa.job
+               rt.classic.implementation.apa.task
+               rt.classic.implementation.apa.schedule
+               rt.classic.implementation.apa.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/apa/bertogna_fp_example.v b/classic/implementation/apa/bertogna_fp_example.v
index 3797a35e39cbcebad36f5b29517a6a9160473729..47d85438eb5151df1bb0c60f3c816b7c5c331127 100644
--- a/classic/implementation/apa/bertogna_fp_example.v
+++ b/classic/implementation/apa/bertogna_fp_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference rt.model.schedule.apa.platform.
-Require Import rt.analysis.apa.workload_bound
-               rt.analysis.apa.interference_bound_fp
-               rt.analysis.apa.bertogna_fp_comp.
-Require Import rt.implementation.apa.job
-               rt.implementation.apa.task
-               rt.implementation.apa.schedule
-               rt.implementation.apa.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.platform.
+Require Import rt.classic.analysis.apa.workload_bound
+               rt.classic.analysis.apa.interference_bound_fp
+               rt.classic.analysis.apa.bertogna_fp_comp.
+Require Import rt.classic.implementation.apa.job
+               rt.classic.implementation.apa.task
+               rt.classic.implementation.apa.schedule
+               rt.classic.implementation.apa.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype fintype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/apa/job.v b/classic/implementation/apa/job.v
index 7dbdca065b73cdffaf575f96d9ad610ce7ce6193..69cdd85ded5658c2e47356f4dc5b485f93872590 100644
--- a/classic/implementation/apa/job.v
+++ b/classic/implementation/apa/job.v
@@ -1,5 +1,5 @@
-Require Import rt.model.time rt.util.all.
-Require Import rt.implementation.apa.task.
+Require Import rt.classic.model.time rt.util.all.
+Require Import rt.classic.implementation.apa.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/classic/implementation/apa/schedule.v b/classic/implementation/apa/schedule.v
index 8d7032ab7defdf09cf34a498e1e954f93f1abf8c..77cf364ec7990c9914695600d63232cb8230382e 100644
--- a/classic/implementation/apa/schedule.v
+++ b/classic/implementation/apa/schedule.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.platform.
-Require Import rt.model.schedule.global.transformation.construction.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.platform.
+Require Import rt.classic.model.schedule.global.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/implementation/apa/task.v b/classic/implementation/apa/task.v
index 3f9b718d3b184dd66fe587d229a62a15bd242646..39138861d343b77682bcca148bbb647d7c5b72b7 100644
--- a/classic/implementation/apa/task.v
+++ b/classic/implementation/apa/task.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task.
-Require Import rt.model.schedule.apa.affinity.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/classic/implementation/arrival_sequence.v b/classic/implementation/arrival_sequence.v
index f82b7dd1c3e362a6ae5eb72f2375109a1648bdb6..340c2ab2a9ee37fbceaa7f8199f6a29079dd4f6d 100644
--- a/classic/implementation/arrival_sequence.v
+++ b/classic/implementation/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.job
-               rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
-Require Import rt.implementation.task rt.implementation.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.implementation.task rt.classic.implementation.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/classic/implementation/global/basic/bertogna_edf_example.v b/classic/implementation/global/basic/bertogna_edf_example.v
index 429dba919465211c802b5e94a034a9340f1a090d..787dd71639e13e128212c80ee6ff1e111039ba41 100644
--- a/classic/implementation/global/basic/bertogna_edf_example.v
+++ b/classic/implementation/global/basic/bertogna_edf_example.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.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.job rt.implementation.task
-               rt.implementation.arrival_sequence.
-Require Import rt.implementation.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform.
+Require Import rt.classic.analysis.global.basic.workload_bound
+               rt.classic.analysis.global.basic.interference_bound_edf
+               rt.classic.analysis.global.basic.bertogna_edf_comp.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence.
+Require Import rt.classic.implementation.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/basic/bertogna_fp_example.v b/classic/implementation/global/basic/bertogna_fp_example.v
index 9f8378d7d733381380acfeb374a8864f1b258822..919c855fe98ef5c5ea619ba560efd813286d9759 100644
--- a/classic/implementation/global/basic/bertogna_fp_example.v
+++ b/classic/implementation/global/basic/bertogna_fp_example.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.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.job rt.implementation.task
-               rt.implementation.arrival_sequence.
-Require Import rt.implementation.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform.
+Require Import rt.classic.analysis.global.basic.workload_bound
+               rt.classic.analysis.global.basic.interference_bound_fp
+               rt.classic.analysis.global.basic.bertogna_fp_comp.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence.
+Require Import rt.classic.implementation.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/global/basic/schedule.v b/classic/implementation/global/basic/schedule.v
index 49a86fabf74525ef07cfb490e932f1c19ed3eeb6..c43fbf0ff775036658a48b06c2306c627308b54a 100644
--- a/classic/implementation/global/basic/schedule.v
+++ b/classic/implementation/global/basic/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform.
-Require Import rt.model.schedule.global.transformation.construction.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform.
+Require Import rt.classic.model.schedule.global.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/implementation/global/jitter/arrival_sequence.v b/classic/implementation/global/jitter/arrival_sequence.v
index dd34d7adbe6dbb419facfd46cf57445c0ac78cf5..5429491128bffb0243c2c33fa3ff6e189bc6d200 100644
--- a/classic/implementation/global/jitter/arrival_sequence.v
+++ b/classic/implementation/global/jitter/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.jitter.job.
-Require Import rt.implementation.global.jitter.task rt.implementation.global.jitter.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.jitter.job.
+Require Import rt.classic.implementation.global.jitter.task rt.classic.implementation.global.jitter.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/classic/implementation/global/jitter/bertogna_edf_example.v b/classic/implementation/global/jitter/bertogna_edf_example.v
index 05eb72278f4bd322b066bd35a2fbef251594098a..d42fb626ebf83b70de258f0b96faabd43f6d4463 100644
--- a/classic/implementation/global/jitter/bertogna_edf_example.v
+++ b/classic/implementation/global/jitter/bertogna_edf_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.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.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.platform.
+Require Import rt.classic.analysis.global.jitter.workload_bound
+               rt.classic.analysis.global.jitter.interference_bound_edf
+               rt.classic.analysis.global.jitter.bertogna_edf_comp.
+Require Import rt.classic.implementation.global.jitter.job
+               rt.classic.implementation.global.jitter.task
+               rt.classic.implementation.global.jitter.schedule
+               rt.classic.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/jitter/bertogna_fp_example.v b/classic/implementation/global/jitter/bertogna_fp_example.v
index eca5d0570941402f71870490dd9ea5d5ccb718cb..d39c1814ef7b0fefb9dc28e04f99ab4b45691913 100644
--- a/classic/implementation/global/jitter/bertogna_fp_example.v
+++ b/classic/implementation/global/jitter/bertogna_fp_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.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.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.platform.
+Require Import rt.classic.analysis.global.jitter.workload_bound
+               rt.classic.analysis.global.jitter.interference_bound_fp
+               rt.classic.analysis.global.jitter.bertogna_fp_comp.
+Require Import rt.classic.implementation.global.jitter.job
+               rt.classic.implementation.global.jitter.task
+               rt.classic.implementation.global.jitter.schedule
+               rt.classic.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/global/jitter/job.v b/classic/implementation/global/jitter/job.v
index e60a33c975e2fc9173b338dd0feca74fa7fbce2e..bccf53702768488a0138f0795cbac9e568dbf5bb 100644
--- a/classic/implementation/global/jitter/job.v
+++ b/classic/implementation/global/jitter/job.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.implementation.global.jitter.task.
+Require Import rt.classic.implementation.global.jitter.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/classic/implementation/global/jitter/schedule.v b/classic/implementation/global/jitter/schedule.v
index d8e1ff972b47428f27d89f455a306afd7779bbae..dfd2cc5f78d6afa3b2366bf05dc25a5474b99c88 100644
--- a/classic/implementation/global/jitter/schedule.v
+++ b/classic/implementation/global/jitter/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.jitter.arrival_sequence rt.model.priority.
-Require Import rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.platform.
-Require Import rt.model.schedule.global.transformation.construction.
+Require Import rt.classic.model.arrival.jitter.arrival_sequence rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.platform.
+Require Import rt.classic.model.schedule.global.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/implementation/global/jitter/task.v b/classic/implementation/global/jitter/task.v
index 9788bf8c5c944ee569b116dcbb7e2409519b3232..779479ef0285fca673cb200c7673bd2a4a3f244a 100644
--- a/classic/implementation/global/jitter/task.v
+++ b/classic/implementation/global/jitter/task.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task.
+Require Import rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/classic/implementation/global/parallel/bertogna_edf_example.v b/classic/implementation/global/parallel/bertogna_edf_example.v
index 7790be6d31770aa8d18efac9e83ab6769007e8da..dd2da84558aeda8b50f4aa72d0131c6daae43bc3 100644
--- a/classic/implementation/global/parallel/bertogna_edf_example.v
+++ b/classic/implementation/global/parallel/bertogna_edf_example.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.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.job rt.implementation.task
-               rt.implementation.arrival_sequence.
-Require Import rt.implementation.global.basic.schedule. (* Use sequential scheduler. *)
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform.
+Require Import rt.classic.analysis.global.parallel.workload_bound
+               rt.classic.analysis.global.parallel.interference_bound_edf
+               rt.classic.analysis.global.parallel.bertogna_edf_comp.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence.
+Require Import rt.classic.implementation.global.basic.schedule. (* Use sequential scheduler. *)
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/parallel/bertogna_fp_example.v b/classic/implementation/global/parallel/bertogna_fp_example.v
index f502aa45f025881de2257767850a2ec4b128cb0d..a79674700b5e62c7a0accd46be43ad1ec84cb73d 100644
--- a/classic/implementation/global/parallel/bertogna_fp_example.v
+++ b/classic/implementation/global/parallel/bertogna_fp_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.platform
-               rt.model.schedule.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.job rt.implementation.task
-               rt.implementation.arrival_sequence.
-Require Import rt.implementation.global.basic.schedule. (* Use sequential scheduler. *)
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.platform
+               rt.classic.model.schedule.global.basic.interference.
+Require Import rt.classic.analysis.global.parallel.workload_bound
+               rt.classic.analysis.global.parallel.interference_bound_fp
+               rt.classic.analysis.global.parallel.bertogna_fp_comp.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence.
+Require Import rt.classic.implementation.global.basic.schedule. (* Use sequential scheduler. *)
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/job.v b/classic/implementation/job.v
index 4dfc0ad42e046f84324579265f9716f401b70782..8fd5bc7b578658e3ec857f6c295ccb4c7bcfab57 100644
--- a/classic/implementation/job.v
+++ b/classic/implementation/job.v
@@ -1,5 +1,5 @@
-Require Import rt.model.time rt.util.all.
-Require Import rt.implementation.task.
+Require Import rt.classic.model.time rt.util.all.
+Require Import rt.classic.implementation.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/classic/implementation/task.v b/classic/implementation/task.v
index 75836dc6dd7010f996ceb8563ef52440c13b29df..5983c5b8080f236cf5f59214a2baf5f0c44796c6 100644
--- a/classic/implementation/task.v
+++ b/classic/implementation/task.v
@@ -1,5 +1,5 @@
-Require Import rt.model.time rt.util.all.
-Require Import rt.model.arrival.basic.task.
+Require Import rt.classic.model.time rt.util.all.
+Require Import rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/classic/implementation/uni/basic/extraction_tdma.v b/classic/implementation/uni/basic/extraction_tdma.v
index 73874c841d301df2e64c13bf0296caea517fe8f1..7d4491f9b64571545ba268cd74b503d7b4d62d4d 100644
--- a/classic/implementation/uni/basic/extraction_tdma.v
+++ b/classic/implementation/uni/basic/extraction_tdma.v
@@ -1,5 +1,5 @@
 (* Require Import Extraction. *) (* Required for Coq 8.7 *)
-Require Import rt.analysis.uni.basic.tdma_wcrt_analysis.
+Require Import rt.classic.analysis.uni.basic.tdma_wcrt_analysis.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Set Implicit Arguments.
diff --git a/classic/implementation/uni/basic/fp_rta_example.v b/classic/implementation/uni/basic/fp_rta_example.v
index 57f4932fa3c0df4bb154a2a8de2dcde2983ffb55..068a269b6ad5992a487612187d1ac389e8213754 100644
--- a/classic/implementation/uni/basic/fp_rta_example.v
+++ b/classic/implementation/uni/basic/fp_rta_example.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.analysis.uni.basic.workload_bound_fp
-               rt.analysis.uni.basic.fp_rta_comp.
-Require Import rt.implementation.job rt.implementation.task
-               rt.implementation.arrival_sequence.
-Require Import rt.implementation.uni.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.analysis.uni.basic.workload_bound_fp
+               rt.classic.analysis.uni.basic.fp_rta_comp.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence.
+Require Import rt.classic.implementation.uni.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/basic/schedule.v b/classic/implementation/uni/basic/schedule.v
index 3f7bdbdd00da7a6bb873131995b3a921b4452e8e..0ed55086e489506c0f4c7fb03d06ed664430cd7c 100644
--- a/classic/implementation/uni/basic/schedule.v
+++ b/classic/implementation/uni/basic/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.basic.platform.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/implementation/uni/basic/schedule_tdma.v b/classic/implementation/uni/basic/schedule_tdma.v
index 097c6bc880829e69795ade929589859c9fe54ef6..16255d9820e788bb349800ab5ed3221ba7b57906 100644
--- a/classic/implementation/uni/basic/schedule_tdma.v
+++ b/classic/implementation/uni/basic/schedule_tdma.v
@@ -1,16 +1,16 @@
 Require Import rt.util.all rt.util.find_seq
                Arith.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.arrival_sequence
-               rt.model.schedule.uni.basic.platform_tdma
-               rt.model.arrival.basic.task rt.model.policy_tdma.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.model.priority
-               rt.analysis.uni.basic.tdma_rta_theory
-               rt.model.schedule.uni.transformation.construction.
-Require Import rt.implementation.job rt.implementation.task
-               rt.implementation.arrival_sequence
-               rt.implementation.uni.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.schedule.uni.basic.platform_tdma
+               rt.classic.model.arrival.basic.task rt.classic.model.policy_tdma.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.priority
+               rt.classic.analysis.uni.basic.tdma_rta_theory
+               rt.classic.model.schedule.uni.transformation.construction.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence
+               rt.classic.implementation.uni.basic.schedule.
 
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
diff --git a/classic/implementation/uni/basic/tdma_rta_example.v b/classic/implementation/uni/basic/tdma_rta_example.v
index 6112fa5d7709905ab3c30017987df96fefeeb88e..23c16273ab56501c8de0eb94e191af1cc5e6289f 100644
--- a/classic/implementation/uni/basic/tdma_rta_example.v
+++ b/classic/implementation/uni/basic/tdma_rta_example.v
@@ -1,16 +1,16 @@
 Require Import rt.util.all rt.util.find_seq
                .
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.arrival_sequence
-               rt.model.schedule.uni.basic.platform_tdma
-               rt.model.arrival.basic.task rt.model.policy_tdma.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.model.priority
-               rt.analysis.uni.basic.tdma_rta_theory
-               rt.analysis.uni.basic.tdma_wcrt_analysis.
-Require Import rt.implementation.job rt.implementation.task
-               rt.implementation.arrival_sequence
-               rt.implementation.uni.basic.schedule_tdma.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.schedule.uni.basic.platform_tdma
+               rt.classic.model.arrival.basic.task rt.classic.model.policy_tdma.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.priority
+               rt.classic.analysis.uni.basic.tdma_rta_theory
+               rt.classic.analysis.uni.basic.tdma_wcrt_analysis.
+Require Import rt.classic.implementation.job rt.classic.implementation.task
+               rt.classic.implementation.arrival_sequence
+               rt.classic.implementation.uni.basic.schedule_tdma.
 
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
diff --git a/classic/implementation/uni/jitter/arrival_sequence.v b/classic/implementation/uni/jitter/arrival_sequence.v
index b88bf013f29e4f320632554074e52170376243db..f700ebb1635e7c7a2fb747e1170d02fb79661291 100644
--- a/classic/implementation/uni/jitter/arrival_sequence.v
+++ b/classic/implementation/uni/jitter/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival rt.model.arrival.basic.job.
-Require Import rt.implementation.uni.jitter.task
-               rt.implementation.uni.jitter.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival rt.classic.model.arrival.basic.job.
+Require Import rt.classic.implementation.uni.jitter.task
+               rt.classic.implementation.uni.jitter.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/classic/implementation/uni/jitter/fp_rta_example.v b/classic/implementation/uni/jitter/fp_rta_example.v
index 161f6f8918fe4ba4da3448ea30e935d39f2e89c7..ded2e7c968302e428bf0b723d17c04d07b9aee15 100644
--- a/classic/implementation/uni/jitter/fp_rta_example.v
+++ b/classic/implementation/uni/jitter/fp_rta_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.task.
-Require Import rt.model.schedule.uni.schedulability.
-Require Import rt.model.arrival.jitter.job.
-Require Import rt.model.schedule.uni.jitter.schedule.
-Require Import rt.analysis.uni.jitter.workload_bound_fp
-               rt.analysis.uni.jitter.fp_rta_comp.
-Require Import rt.implementation.uni.jitter.job
-               rt.implementation.uni.jitter.task
-               rt.implementation.uni.jitter.arrival_sequence
-               rt.implementation.uni.jitter.schedule.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.arrival.jitter.job.
+Require Import rt.classic.model.schedule.uni.jitter.schedule.
+Require Import rt.classic.analysis.uni.jitter.workload_bound_fp
+               rt.classic.analysis.uni.jitter.fp_rta_comp.
+Require Import rt.classic.implementation.uni.jitter.job
+               rt.classic.implementation.uni.jitter.task
+               rt.classic.implementation.uni.jitter.arrival_sequence
+               rt.classic.implementation.uni.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/jitter/job.v b/classic/implementation/uni/jitter/job.v
index c72bf1c69d2f9bdc9e0cc4a3ab2000cb83e1a13d..bec45ae4c4d724407f65c6a97390ec6c7821ee53 100644
--- a/classic/implementation/uni/jitter/job.v
+++ b/classic/implementation/uni/jitter/job.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.implementation.uni.jitter.task.
+Require Import rt.classic.implementation.uni.jitter.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/classic/implementation/uni/jitter/schedule.v b/classic/implementation/uni/jitter/schedule.v
index 8f410279a36be8bfcfb47a82e07b2f9d4ab51f0e..79e1e0f66bdb549fb0cd1f25600be0401f7bc47e 100644
--- a/classic/implementation/uni/jitter/schedule.v
+++ b/classic/implementation/uni/jitter/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.platform.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/implementation/uni/jitter/task.v b/classic/implementation/uni/jitter/task.v
index b78d2215128623e8e67b171f6bcad6c3418c2a18..649378de92bd446bf301842db9a8e0d02563e60e 100644
--- a/classic/implementation/uni/jitter/task.v
+++ b/classic/implementation/uni/jitter/task.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task.
+Require Import rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/classic/implementation/uni/susp/dynamic/arrival_sequence.v b/classic/implementation/uni/susp/dynamic/arrival_sequence.v
index 64a12b2630672ca8e8bc3ee956de7c19cebbbf88..2fb5172a2e65e9c62319dd635faa484ed4c88501 100644
--- a/classic/implementation/uni/susp/dynamic/arrival_sequence.v
+++ b/classic/implementation/uni/susp/dynamic/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival rt.model.arrival.basic.job.
-Require Import rt.implementation.uni.susp.dynamic.task
-               rt.implementation.uni.susp.dynamic.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival rt.classic.model.arrival.basic.job.
+Require Import rt.classic.implementation.uni.susp.dynamic.task
+               rt.classic.implementation.uni.susp.dynamic.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/classic/implementation/uni/susp/dynamic/job.v b/classic/implementation/uni/susp/dynamic/job.v
index 07d881a9e25e8da33e564e5c307523cb8224dca4..b4590b70faa8a059098cfe79ebb560dfc335a32e 100644
--- a/classic/implementation/uni/susp/dynamic/job.v
+++ b/classic/implementation/uni/susp/dynamic/job.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.implementation.uni.susp.dynamic.task.
+Require Import rt.classic.implementation.uni.susp.dynamic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v b/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
index 248eb951d62169fe51ea1f370cc0afa9b99734c9..a93d2bef2e2ab36079d10ec8d33b2f82041be63f 100644
--- a/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
+++ b/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
-Require Import rt.model.schedule.uni.susp.suspension_intervals.
-Require Import rt.analysis.uni.basic.workload_bound_fp.
-Require Import rt.analysis.uni.susp.dynamic.oblivious.fp_rta.
-Require Import rt.implementation.uni.susp.dynamic.job
-               rt.implementation.uni.susp.dynamic.task
-               rt.implementation.uni.susp.dynamic.arrival_sequence.
-Require Import rt.implementation.uni.susp.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals.
+Require Import rt.classic.analysis.uni.basic.workload_bound_fp.
+Require Import rt.classic.analysis.uni.susp.dynamic.oblivious.fp_rta.
+Require Import rt.classic.implementation.uni.susp.dynamic.job
+               rt.classic.implementation.uni.susp.dynamic.task
+               rt.classic.implementation.uni.susp.dynamic.arrival_sequence.
+Require Import rt.classic.implementation.uni.susp.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/susp/dynamic/task.v b/classic/implementation/uni/susp/dynamic/task.v
index 4f80478fe791646420123a60dd16bb6297b7f282..721ae238e1b86af62cf69efce5bd107b5407f863 100644
--- a/classic/implementation/uni/susp/dynamic/task.v
+++ b/classic/implementation/uni/susp/dynamic/task.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task.
+Require Import rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/classic/implementation/uni/susp/schedule.v b/classic/implementation/uni/susp/schedule.v
index cf1c7138ab5b8ba4d97e673bd010b69468be6d91..155a59fc2671fadb7e65e3128a6a41891aae533c 100644
--- a/classic/implementation/uni/susp/schedule.v
+++ b/classic/implementation/uni/susp/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.susp.platform.
-Require Import rt.model.schedule.uni.transformation.construction.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.susp.platform.
+Require Import rt.classic.model.schedule.uni.transformation.construction.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/classic/model/arrival/basic/arrival_bounds.v b/classic/model/arrival/basic/arrival_bounds.v
index 8bee5cd0217a7a7414813b2dcf6318ca18d613b0..44100b694ff0bf04c9dc8008a444c97a554ed967 100644
--- a/classic/model/arrival/basic/arrival_bounds.v
+++ b/classic/model/arrival/basic/arrival_bounds.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival
-               rt.model.priority.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
 
 (* Properties of job arrival. *)
diff --git a/classic/model/arrival/basic/arrival_sequence.v b/classic/model/arrival/basic/arrival_sequence.v
index 78e67106d855eb403307f6c7466f5ee45fbeb8e5..e211d6a12dcfb02433e445576f890c5971f5994e 100644
--- a/classic/model/arrival/basic/arrival_sequence.v
+++ b/classic/model/arrival/basic/arrival_sequence.v
@@ -1,4 +1,4 @@
-Require Import rt.util.all rt.model.arrival.basic.task rt.model.time.
+Require Import rt.util.all rt.classic.model.arrival.basic.task rt.classic.model.time.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* Definitions and properties of job arrival sequences. *)
diff --git a/classic/model/arrival/basic/job.v b/classic/model/arrival/basic/job.v
index d01ef941aba9f7854931276f4cc7a5bed77cae7a..f5bb8ff6eded56df8ae5255f57263b7c0476bf1e 100644
--- a/classic/model/arrival/basic/job.v
+++ b/classic/model/arrival/basic/job.v
@@ -1,4 +1,4 @@
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
   
 (* Properties of different types of job: *)
diff --git a/classic/model/arrival/basic/task.v b/classic/model/arrival/basic/task.v
index 6dee9d6a852e5f6a474a12951904ff3e34686524..06617dd8c90ce5840a4869c3206e34464e5b5520 100644
--- a/classic/model/arrival/basic/task.v
+++ b/classic/model/arrival/basic/task.v
@@ -1,4 +1,4 @@
-Require Import rt.model.time rt.util.all.
+Require Import rt.classic.model.time rt.util.all.
 From mathcomp Require Import ssrnat ssrbool eqtype fintype seq.
 
 (* Attributes of a valid sporadic task. *)
diff --git a/classic/model/arrival/basic/task_arrival.v b/classic/model/arrival/basic/task_arrival.v
index 3480dd872870ca0c95cfa38bf7cf6da35690be7d..5ebdb2fe99242782b6138e05ddbc8d24da332f4c 100644
--- a/classic/model/arrival/basic/task_arrival.v
+++ b/classic/model/arrival/basic/task_arrival.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path bigop.
 
 (* Properties of job arrival. *)
diff --git a/classic/model/arrival/curves/bounds.v b/classic/model/arrival/curves/bounds.v
index d7a4c0fb7b132b6f02fa76eb60d0a074740f4f6b..0fbe94404d18c1418f710587a3b7432b0abace29 100644
--- a/classic/model/arrival/curves/bounds.v
+++ b/classic/model/arrival/curves/bounds.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence           
-        rt.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.arrival.basic.arrival_sequence           
+        rt.classic.model.arrival.basic.task_arrival.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.
 
 (* In this section, we define the notion of arrival curves, which
diff --git a/classic/model/arrival/jitter/arrival_bounds.v b/classic/model/arrival/jitter/arrival_bounds.v
index 65de91276cef7c12a170b2c42a5b7f1f9702d1b1..c6b05c87f409f570ebcbdaf2282b02dc28f51259 100644
--- a/classic/model/arrival/jitter/arrival_bounds.v
+++ b/classic/model/arrival/jitter/arrival_bounds.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.arrival.jitter.job
-               rt.model.arrival.jitter.arrival_sequence
-               rt.model.arrival.jitter.task_arrival.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.arrival.jitter.job
+               rt.classic.model.arrival.jitter.arrival_sequence
+               rt.classic.model.arrival.jitter.task_arrival.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
 
 (* In this file, we prove bounds on the number of actual task arrivals, i.e,
diff --git a/classic/model/arrival/jitter/arrival_sequence.v b/classic/model/arrival/jitter/arrival_sequence.v
index 3ddeb69b15a661ef87dffe631a9ef16d035e4cba..1926bc1fec07a1a3b22551286ff0c8df4d0cc186 100644
--- a/classic/model/arrival/jitter/arrival_sequence.v
+++ b/classic/model/arrival/jitter/arrival_sequence.v
@@ -1,4 +1,4 @@
-Require Import rt.util.all rt.model.arrival.basic.arrival_sequence.
+Require Import rt.util.all rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* In this file we provide extra definitions for job arrival sequences with jitter. *)
diff --git a/classic/model/arrival/jitter/job.v b/classic/model/arrival/jitter/job.v
index b254a63ca861faedf1577ee660846f81964bd350..572b54a97fe1d0373bbc0d66bbecf6d87c29fc01 100644
--- a/classic/model/arrival/jitter/job.v
+++ b/classic/model/arrival/jitter/job.v
@@ -1,7 +1,7 @@
-Require Import rt.model.time rt.model.arrival.basic.task.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
-Require Export rt.model.arrival.basic.job.
+Require Export rt.classic.model.arrival.basic.job.
 
 (* In this file, we define properties of jobs with jitter. *)
 Module JobWithJitter.
diff --git a/classic/model/arrival/jitter/task_arrival.v b/classic/model/arrival/jitter/task_arrival.v
index cc27dc598272ed09db702b48f2c9edfbb81b225b..272d93233ab91e58d356a641380ddaec9e42be89 100644
--- a/classic/model/arrival/jitter/task_arrival.v
+++ b/classic/model/arrival/jitter/task_arrival.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job.
-Require Import rt.model.arrival.basic.task_arrival.
-Require Import rt.model.arrival.jitter.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.arrival.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path.
 
 (* In this file, we provide definitions and lemmas about task arrivals
diff --git a/classic/model/policy_tdma.v b/classic/model/policy_tdma.v
index 166001fe82514cd265ec92294de1dd62341b4c0b..4d49c0515e216e6e2ea48f2b4962510a96c6c997 100644
--- a/classic/model/policy_tdma.v
+++ b/classic/model/policy_tdma.v
@@ -1,7 +1,7 @@
 Require Import  rt.util.all.
-Require Import  rt.model.time
-                rt.model.arrival.basic.task 
-                rt.model.arrival.basic.job.
+Require Import  rt.classic.model.time
+                rt.classic.model.arrival.basic.task 
+                rt.classic.model.arrival.basic.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
 
 Module PolicyTDMA.
diff --git a/classic/model/priority.v b/classic/model/priority.v
index 7360cacb31d6af283507fc430f1093e82dac3044..ceedcc667b67100efdbf03bca5d91835d9ba1f06 100644
--- a/classic/model/priority.v
+++ b/classic/model/priority.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* Definitions of FP, JLFP and JLDP priority relations. *)
@@ -122,7 +122,7 @@ Module Priority.
 
     (* Recall that the jobs are sequential if they are executed 
        in the order they arrived (for more details see file 
-       rt.model.schedule.uni.schedule.v). 
+       rt.classic.model.schedule.uni.schedule.v). 
        
        An arbitrary JLFP can violate the sequential jobs hypothesis. 
        For example, consider two jobs j1, j2 of the same task such that 
diff --git a/classic/model/schedule/apa/affinity.v b/classic/model/schedule/apa/affinity.v
index 2ddd529457d796aba2ff43746cc2aeb3e313e5a1..b290740118584168bdc299fae7d7f40c9862cd09 100644
--- a/classic/model/schedule/apa/affinity.v
+++ b/classic/model/schedule/apa/affinity.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition and properties about processor affinities. *)
diff --git a/classic/model/schedule/apa/constrained_deadlines.v b/classic/model/schedule/apa/constrained_deadlines.v
index a768a41b429283d66cfb8a9500b43d6595578099..98ec5ba3423390e7b9e4accb97ea4b64acd4a488 100644
--- a/classic/model/schedule/apa/constrained_deadlines.v
+++ b/classic/model/schedule/apa/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.interference rt.model.schedule.apa.affinity rt.model.schedule.apa.platform.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/classic/model/schedule/apa/interference.v b/classic/model/schedule/apa/interference.v
index 5c524146ff3211e6a538a37c81e38b2b31f1e487..8e6646814c310ee351c2034a15715f63e9a24500 100644
--- a/classic/model/schedule/apa/interference.v
+++ b/classic/model/schedule/apa/interference.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.affinity.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
diff --git a/classic/model/schedule/apa/interference_edf.v b/classic/model/schedule/apa/interference_edf.v
index f4896a2bc5518a7524453af5054615c652f13afc..33f4ca339e49d0db2d1f2c535e9969977405b41c 100644
--- a/classic/model/schedule/apa/interference_edf.v
+++ b/classic/model/schedule/apa/interference_edf.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference
-               rt.model.schedule.apa.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.affinity rt.classic.model.schedule.apa.interference
+               rt.classic.model.schedule.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/classic/model/schedule/apa/platform.v b/classic/model/schedule/apa/platform.v
index 136732d9d744f933be4dd2f1a76b0cc3cb0dfd2d..33356d1897bf82974bfcadaa9894ab851a6cb5f8 100644
--- a/classic/model/schedule/apa/platform.v
+++ b/classic/model/schedule/apa/platform.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.apa.interference rt.classic.model.schedule.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/classic/model/schedule/global/basic/constrained_deadlines.v b/classic/model/schedule/global/basic/constrained_deadlines.v
index 42226bbb83ba3932148c65e18f6000ad20d40250..fb9ef3a19f1e182cc81cbcf4bcaa79324a80dd3b 100644
--- a/classic/model/schedule/global/basic/constrained_deadlines.v
+++ b/classic/model/schedule/global/basic/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference
-               rt.model.schedule.global.basic.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference
+               rt.classic.model.schedule.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/classic/model/schedule/global/basic/interference.v b/classic/model/schedule/global/basic/interference.v
index 14ef4eed3b6d477718484d15f8f0ba2a45fc17dc..d58d53ae4e9edd8e8b39a3a1a7265a73c5c5e7fc 100644
--- a/classic/model/schedule/global/basic/interference.v
+++ b/classic/model/schedule/global/basic/interference.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority.
-Require Import rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority.
+Require Import rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
diff --git a/classic/model/schedule/global/basic/interference_edf.v b/classic/model/schedule/global/basic/interference_edf.v
index 27cba24394909cddd64b80e42432e37f2b306df0..7a1ea6824e77466c5936119a3130e27e33d0b601 100644
--- a/classic/model/schedule/global/basic/interference_edf.v
+++ b/classic/model/schedule/global/basic/interference_edf.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference
-               rt.model.schedule.global.basic.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference
+               rt.classic.model.schedule.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/classic/model/schedule/global/basic/platform.v b/classic/model/schedule/global/basic/platform.v
index 68c489622f3e55a69312e23f71b255cea326d3b1..be7d55d6a4a9cd727feca32b5602fd5026bb2b2a 100644
--- a/classic/model/schedule/global/basic/platform.v
+++ b/classic/model/schedule/global/basic/platform.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule rt.model.schedule.global.basic.interference.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/classic/model/schedule/global/basic/schedule.v b/classic/model/schedule/global/basic/schedule.v
index f93edba882d5307d0c60c7f36e18758c66a34538..7c179110331cf82731e9b6d224bf569c831b4ceb 100644
--- a/classic/model/schedule/global/basic/schedule.v
+++ b/classic/model/schedule/global/basic/schedule.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all
-               rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence.
+               rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition, properties and lemmas about schedules. *)
diff --git a/classic/model/schedule/global/jitter/constrained_deadlines.v b/classic/model/schedule/global/jitter/constrained_deadlines.v
index 9ac68edaf32b7758225eb35de0a84df67ef632d4..fc5342b5e5c8d170215b0ab2ab74493bbbaaa71e 100644
--- a/classic/model/schedule/global/jitter/constrained_deadlines.v
+++ b/classic/model/schedule/global/jitter/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.interference rt.model.schedule.global.jitter.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.interference rt.classic.model.schedule.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/classic/model/schedule/global/jitter/interference.v b/classic/model/schedule/global/jitter/interference.v
index f4525641fafba114e6e965503ea3a0e046c5b521..f74638fed8ce0d1181ead73a4ce8ce9c6f54591c 100644
--- a/classic/model/schedule/global/jitter/interference.v
+++ b/classic/model/schedule/global/jitter/interference.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.schedule.global.workload.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.schedule.global.workload.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-Require rt.model.schedule.global.basic.interference.
+Require rt.classic.model.schedule.global.basic.interference.
 
 Module Interference.
 
@@ -12,7 +12,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. *)
-  Import rt.model.schedule.global.basic.interference.
+  Import rt.classic.model.schedule.global.basic.interference.
   Export Interference.
   
   Section InterferenceDefs.
diff --git a/classic/model/schedule/global/jitter/interference_edf.v b/classic/model/schedule/global/jitter/interference_edf.v
index 84e15929bf2052f7f0efc230ea6c28962e891fa8..0eceea69d56c7821a093df3af3ae747d36d93121 100644
--- a/classic/model/schedule/global/jitter/interference_edf.v
+++ b/classic/model/schedule/global/jitter/interference_edf.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.jitter.job
-               rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.interference
-               rt.model.schedule.global.jitter.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.jitter.job
+               rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.interference
+               rt.classic.model.schedule.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/classic/model/schedule/global/jitter/job.v b/classic/model/schedule/global/jitter/job.v
index 9b1639e1332c0b694a7f03300467d9683eea7713..824cf4192aea8b305fb7c5f878e91a04e47261e0 100644
--- a/classic/model/schedule/global/jitter/job.v
+++ b/classic/model/schedule/global/jitter/job.v
@@ -1,7 +1,7 @@
-Require Import rt.model.time rt.model.arrival.basic.task.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
-Require Export rt.model.arrival.basic.job.
+Require Export rt.classic.model.arrival.basic.job.
 
 (* Properties of different types of job: *)
 Module JobWithJitter.
diff --git a/classic/model/schedule/global/jitter/platform.v b/classic/model/schedule/global/jitter/platform.v
index f2cd32e06ab7d772bf82207a6a49f3a1e335af8c..cda3fd78a53b743415bfc7cce5f4463ede393925 100644
--- a/classic/model/schedule/global/jitter/platform.v
+++ b/classic/model/schedule/global/jitter/platform.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
-               rt.model.schedule.global.jitter.interference.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.schedule.global.jitter.schedule
+               rt.classic.model.schedule.global.jitter.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/classic/model/schedule/global/jitter/schedule.v b/classic/model/schedule/global/jitter/schedule.v
index 18409931ae8b2ab33f7d1041699341fd9454f84c..7ce789989ca2909149d68e86a76b857f55b8c5b9 100644
--- a/classic/model/schedule/global/jitter/schedule.v
+++ b/classic/model/schedule/global/jitter/schedule.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task.
-Require Import rt.model.schedule.global.jitter.job rt.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.global.jitter.job rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-Require rt.model.schedule.global.basic.schedule.
+Require rt.classic.model.schedule.global.basic.schedule.
 
 (* Definition, properties and lemmas about schedules. *)
 Module ScheduleWithJitter.
 
   (* We import the original schedule module and redefine whatever is required. *)
-  Export rt.model.schedule.global.basic.schedule.
+  Export rt.classic.model.schedule.global.basic.schedule.
   Export ArrivalSequence Schedule.
   
   (* We need to redefine the properties of a job that depend on the arrival time. *)
diff --git a/classic/model/schedule/global/response_time.v b/classic/model/schedule/global/response_time.v
index 865d4996187324a812613ae3214f98ca9afaa01a..2d32db9adafdfb4461f58f0e2edc19ac92915a5a 100644
--- a/classic/model/schedule/global/response_time.v
+++ b/classic/model/schedule/global/response_time.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.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/classic/model/schedule/global/schedulability.v b/classic/model/schedule/global/schedulability.v
index 14d59ddc8220898227eaf49e8a5e01c34fc524ea..e7bde17377be08510c5d440e446074d736298da4 100644
--- a/classic/model/schedule/global/schedulability.v
+++ b/classic/model/schedule/global/schedulability.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
 
 (* Definitions of deadline miss. *)
diff --git a/classic/model/schedule/global/transformation/construction.v b/classic/model/schedule/global/transformation/construction.v
index 7eaf5bfb6b51156681cb03eecf2104d9717b9e41..35a80abbd327e144e63da514eb5f4fa2e65b7311 100644
--- a/classic/model/schedule/global/transformation/construction.v
+++ b/classic/model/schedule/global/transformation/construction.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path finfun.
 
 Module ScheduleConstruction.
diff --git a/classic/model/schedule/global/workload.v b/classic/model/schedule/global/workload.v
index fcb606f0681a5594379a16a479a646e8fe72c9db..e4be1f41caa0c6723dc2ff0d27202df34816b718 100644
--- a/classic/model/schedule/global/workload.v
+++ b/classic/model/schedule/global/workload.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.global.schedulability rt.model.schedule.global.response_time.
-Require Import rt.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.global.schedulability rt.classic.model.schedule.global.response_time.
+Require Import rt.classic.model.schedule.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module Workload.
diff --git a/classic/model/schedule/partitioned/schedulability.v b/classic/model/schedule/partitioned/schedulability.v
index acb8d25b74f80a081f4f6d0a6d1bd0cca2d8fcc9..63d9973f3c0a4daaa06299505f0cd2678e7bab5c 100644
--- a/classic/model/schedule/partitioned/schedulability.v
+++ b/classic/model/schedule/partitioned/schedulability.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require Import rt.model.schedule.partitioned.schedule.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require Import rt.classic.model.schedule.partitioned.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-Require rt.model.schedule.uni.schedule.
+Require rt.classic.model.schedule.uni.schedule.
 
 Module PartitionSchedulability.
   
-  Module uni_sched := rt.model.schedule.uni.schedulability.Schedulability.
+  Module uni_sched := rt.classic.model.schedule.uni.schedulability.Schedulability.
   Import ArrivalSequence Partitioned Schedule Schedulability.
 
   Section PartitionedAsUniprocessor.
diff --git a/classic/model/schedule/partitioned/schedule.v b/classic/model/schedule/partitioned/schedule.v
index fc2fa30c5fd105bbc0df6d694c57e68428351af2..4dc8f009b09cd5511261ae3084038660858d975b 100644
--- a/classic/model/schedule/partitioned/schedule.v
+++ b/classic/model/schedule/partitioned/schedule.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job.
-Require Import rt.model.schedule.global.schedulability.
-Require Import rt.model.schedule.global.basic.schedule.
-Require rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.global.schedulability.
+Require Import rt.classic.model.schedule.global.basic.schedule.
+Require rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.schedulability.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Partitioned.
 
-  Module uni := rt.model.schedule.uni.schedule.UniprocessorSchedule.
-  Module uni_sched := rt.model.schedule.uni.schedulability.Schedulability.
+  Module uni := rt.classic.model.schedule.uni.schedule.UniprocessorSchedule.
+  Module uni_sched := rt.classic.model.schedule.uni.schedulability.Schedulability.
   Import SporadicTaskset Schedule Schedulability.
   Export Time.
   
diff --git a/classic/model/schedule/uni/basic/platform.v b/classic/model/schedule/uni/basic/platform.v
index aaf70c03f7bfed65d6ac05f764089ccf13554bd3..f353bf66ab39ecc770adaccbc6bd86f061729c21 100644
--- a/classic/model/schedule/uni/basic/platform.v
+++ b/classic/model/schedule/uni/basic/platform.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/classic/model/schedule/uni/basic/platform_tdma.v b/classic/model/schedule/uni/basic/platform_tdma.v
index c19072d35addf5fdad179d75408aeeac1e10225a..3f42ee39b0303e17bff2e623c3381f2d0d6e9507 100644
--- a/classic/model/schedule/uni/basic/platform_tdma.v
+++ b/classic/model/schedule/uni/basic/platform_tdma.v
@@ -1,9 +1,9 @@
 Require Import  rt.util.all.
-Require Import  rt.model.arrival.basic.task 
-                rt.model.arrival.basic.job rt.model.priority 
-                rt.model.arrival.basic.task_arrival
-                rt.model.schedule.uni.schedule.
-Require Import  rt.model.policy_tdma.
+Require Import  rt.classic.model.arrival.basic.task 
+                rt.classic.model.arrival.basic.job rt.classic.model.priority 
+                rt.classic.model.arrival.basic.task_arrival
+                rt.classic.model.schedule.uni.schedule.
+Require Import  rt.classic.model.policy_tdma.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform_TDMA.
diff --git a/classic/model/schedule/uni/end_time.v b/classic/model/schedule/uni/end_time.v
index 268a45ab8c5ee2aa678acc7aa89229cdec24a886..10f7e227147b5d2e2505d434b960ccf91151827b 100644
--- a/classic/model/schedule/uni/end_time.v
+++ b/classic/model/schedule/uni/end_time.v
@@ -1,9 +1,9 @@
 Require Import Arith Nat. 
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task 
-               rt.model.arrival.basic.job 
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time.
+Require Import rt.classic.model.arrival.basic.task 
+               rt.classic.model.arrival.basic.job 
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Set Bullet Behavior "Strict Subproofs".
diff --git a/classic/model/schedule/uni/jitter/busy_interval.v b/classic/model/schedule/uni/jitter/busy_interval.v
index 78da89d908940844c1ac8ef4d687a73cdc0b499e..78f006631037d116140470af44de899f0d0ea039 100644
--- a/classic/model/schedule/uni/jitter/busy_interval.v
+++ b/classic/model/schedule/uni/jitter/busy_interval.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job
-               rt.model.arrival.basic.arrival_sequence
-               rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.service rt.model.schedule.uni.workload.
-Require Import rt.model.schedule.uni.jitter.schedule rt.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.service rt.classic.model.schedule.uni.workload.
+Require Import rt.classic.model.schedule.uni.jitter.schedule rt.classic.model.schedule.uni.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file, we provide definitions and lemmas about busy intervals
diff --git a/classic/model/schedule/uni/jitter/platform.v b/classic/model/schedule/uni/jitter/platform.v
index 6f1cda4bd94ee316a9fd67d39d520d827c2297c7..05115cb7d417f7b9129bfaedf22089f5aa366529 100644
--- a/classic/model/schedule/uni/jitter/platform.v
+++ b/classic/model/schedule/uni/jitter/platform.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.jitter.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* In this file, we define properties about the platform in jitter-aware schedules. *)
diff --git a/classic/model/schedule/uni/jitter/schedule.v b/classic/model/schedule/uni/jitter/schedule.v
index cfafef9567c4efa285b34594de011afb8021f97e..26c967088900f0f58f9d94bcea6e6ebc6d9633ce 100644
--- a/classic/model/schedule/uni/jitter/schedule.v
+++ b/classic/model/schedule/uni/jitter/schedule.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.arrival.jitter.arrival_sequence.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
diff --git a/classic/model/schedule/uni/jitter/valid_schedule.v b/classic/model/schedule/uni/jitter/valid_schedule.v
index 46c8be09d4abe85ba0d094c6965197c3bb8ab695..dbbff4c6bc3ba7f682f1e31a4929c54fe0d9bd19 100644
--- a/classic/model/schedule/uni/jitter/valid_schedule.v
+++ b/classic/model/schedule/uni/jitter/valid_schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.jitter.schedule
-               rt.model.schedule.uni.jitter.platform.
+Require Import rt.classic.model.priority.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.jitter.schedule
+               rt.classic.model.schedule.uni.jitter.platform.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
index d6bd459e1dcc2f6adcb6d35515d599dd2da1d56f..b8891c8991ef44a43bf9a258374bb364be84ad78 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.abstract_RTA.definitions
-               rt.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
-               rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.abstract_RTA.definitions
+               rt.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
+               rt.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.
  
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index 4c6fe76a1e2246bcbf3caa788adfd54b4b93f778..0261a3c2288c5731e24a0d0740006c4115fe7a22 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -1,19 +1,19 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time
-               rt.model.schedule.uni.schedule_of_task.
-Require Import rt.model.schedule.uni.limited.rbf
-               rt.model.schedule.uni.limited.schedule.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound. 
-Require Import rt.model.schedule.uni.limited.abstract_RTA.definitions
-               rt.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
-               rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
-               rt.model.schedule.uni.limited.abstract_RTA.abstract_rta.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time
+               rt.classic.model.schedule.uni.schedule_of_task.
+Require Import rt.classic.model.schedule.uni.limited.rbf
+               rt.classic.model.schedule.uni.limited.schedule.
+Require Import rt.classic.model.arrival.curves.bounds.
+Require Import rt.classic.analysis.uni.arrival_curves.workload_bound. 
+Require Import rt.classic.model.schedule.uni.limited.abstract_RTA.definitions
+               rt.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
+               rt.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
+               rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/definitions.v b/classic/model/schedule/uni/limited/abstract_RTA/definitions.v
index 09e0cc709a41a71ace35b2255044ea82a3c09c6a..482cd7480fa33c00240aae869197be0cd3313c5d 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/definitions.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/definitions.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.schedule. 
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.schedule. 
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v b/classic/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
index dded10d6cc49632d0292cdc467646f2388ae4b99..3d2b3134466f8cc56e66e3a06e275b75570643b0 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
index 79d740d04eefcf827ccaf08df2b0e8ed86d35116..e624da9a1aca003154406defb5f2e1bd55766fb2 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.abstract_RTA.definitions.
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.abstract_RTA.definitions.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/busy_interval.v b/classic/model/schedule/uni/limited/busy_interval.v
index 2980f961d59039929591ab62f405875d4509175c..7e12548a28ad8a0f1a8d7aae262e37fbbe8bdb1d 100644
--- a/classic/model/schedule/uni/limited/busy_interval.v
+++ b/classic/model/schedule/uni/limited/busy_interval.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task
-               rt.model.arrival.basic.job
-               rt.model.arrival.basic.arrival_sequence
-               rt.model.priority
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.limited.platform.definitions.
+Require Import rt.classic.model.arrival.basic.task
+               rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -96,7 +96,7 @@ Module BusyIntervalJLFP.
 
       (* We say that the job incurs priority inversion if it has higher priority than the scheduled
          job. Note that this definition implicitly assumes that the scheduler is work-conserving in 
-         the sense of the definition given in rt.model.schedule.uni.basic.platform. Therefore, it 
+         the sense of the definition given in rt.classic.model.schedule.uni.basic.platform. Therefore, it 
          cannot be applied to models with jitter or self-suspensions. *)
       Definition is_priority_inversion t :=
         if sched t is Some jlp then
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index 03412a60cabb9561d1154b02074340d9e6d05a38..82c74cbb7e9838e8e19bdb9c869b61aa42c7d05d 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ -1,21 +1,21 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.edf.response_time_bound
-               rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound
-               rt.model.schedule.uni.limited.rbf.
-Require Import rt.model.arrival.curves.bounds
-               rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule
-               rt.model.schedule.uni.limited.platform.limited
-               rt.model.schedule.uni.limited.platform.preemptive
-               rt.model.schedule.uni.limited.platform.nonpreemptive.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.edf.response_time_bound
+               rt.classic.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound
+               rt.classic.model.schedule.uni.limited.rbf.
+Require Import rt.classic.model.arrival.curves.bounds
+               rt.classic.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule
+               rt.classic.model.schedule.uni.limited.platform.limited
+               rt.classic.model.schedule.uni.limited.platform.preemptive
+               rt.classic.model.schedule.uni.limited.platform.nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index c9ee30e43d40e41f657d4167f4a26403f57bafc0..828863f8243842355b178716187abd5813561b39 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -1,19 +1,19 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time. 
-Require Import rt.model.schedule.uni.limited.platform.definitions
-               rt.model.schedule.uni.limited.platform.priority_inversion_is_bounded
-               rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.busy_interval
-               rt.model.schedule.uni.limited.edf.response_time_bound
-               rt.model.schedule.uni.limited.rbf.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time. 
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions
+               rt.classic.model.schedule.uni.limited.platform.priority_inversion_is_bounded
+               rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.busy_interval
+               rt.classic.model.schedule.uni.limited.edf.response_time_bound
+               rt.classic.model.schedule.uni.limited.rbf.
+Require Import rt.classic.model.arrival.curves.bounds.
+Require Import rt.classic.analysis.uni.arrival_curves.workload_bound.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/edf/response_time_bound.v b/classic/model/schedule/uni/limited/edf/response_time_bound.v
index 0ff63e7b401588ecdc489eed1f13185e91c7377b..84af53cd9ac8674f4da18fd1b1058b3caa5adc13 100644
--- a/classic/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/response_time_bound.v
@@ -1,22 +1,22 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time
-               rt.model.schedule.uni.schedule_of_task.
-Require Import rt.model.schedule.uni.limited.platform.definitions
-               rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.busy_interval
-               rt.model.schedule.uni.limited.rbf
-               rt.model.schedule.uni.limited.abstract_RTA.definitions
-               rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
-               rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
-               rt.model.schedule.uni.limited.jlfp_instantiation.
-Require Import rt.model.arrival.curves.bounds. 
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time
+               rt.classic.model.schedule.uni.schedule_of_task.
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions
+               rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.busy_interval
+               rt.classic.model.schedule.uni.limited.rbf
+               rt.classic.model.schedule.uni.limited.abstract_RTA.definitions
+               rt.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
+               rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
+               rt.classic.model.schedule.uni.limited.jlfp_instantiation.
+Require Import rt.classic.model.arrival.curves.bounds. 
+Require Import rt.classic.analysis.uni.arrival_curves.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Abstract RTA for EDF-schedulers *)
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
index 8eef99ccc10bfe769c163aa510078a013db3e2a3..c7ea33b32f722f6bef3a400616a1640dab0fd56e 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -1,20 +1,20 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
-               rt.model.schedule.uni.limited.rbf.
-Require Import rt.model.arrival.curves.bounds
-               rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule
-               rt.model.schedule.uni.limited.platform.limited
-               rt.model.schedule.uni.limited.platform.preemptive
-               rt.model.schedule.uni.limited.platform.nonpreemptive.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
+               rt.classic.model.schedule.uni.limited.rbf.
+Require Import rt.classic.model.arrival.curves.bounds
+               rt.classic.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule
+               rt.classic.model.schedule.uni.limited.platform.limited
+               rt.classic.model.schedule.uni.limited.platform.preemptive
+               rt.classic.model.schedule.uni.limited.platform.nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index d5d27a160308e5d5a97d9398faabe9c6b0a9ec2d..07030975d9bae6c1a2eed9271c4ebad55a7437f7 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -1,19 +1,19 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.arrival.curves.bounds
-               rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.platform.definitions
-               rt.model.schedule.uni.limited.platform.priority_inversion_is_bounded
-               rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.busy_interval
-               rt.model.schedule.uni.limited.fixed_priority.response_time_bound
-               rt.model.schedule.uni.limited.rbf.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.arrival.curves.bounds
+               rt.classic.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time.
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions
+               rt.classic.model.schedule.uni.limited.platform.priority_inversion_is_bounded
+               rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.busy_interval
+               rt.classic.model.schedule.uni.limited.fixed_priority.response_time_bound
+               rt.classic.model.schedule.uni.limited.rbf.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index 12a68413e0123dcbc5cc4ec98adc0820718194b6..3482803ee104b268900e4ad39ac07b022d078fbe 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -1,22 +1,22 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority. 
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.response_time
-               rt.model.schedule.uni.schedule_of_task.
-Require Import rt.model.schedule.uni.limited.platform.definitions
-               rt.model.schedule.uni.limited.schedule
-               rt.model.schedule.uni.limited.rbf
-               rt.model.schedule.uni.limited.abstract_RTA.definitions
-               rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
-               rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
-               rt.model.schedule.uni.limited.jlfp_instantiation.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.limited.busy_interval.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority. 
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.response_time
+               rt.classic.model.schedule.uni.schedule_of_task.
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions
+               rt.classic.model.schedule.uni.limited.schedule
+               rt.classic.model.schedule.uni.limited.rbf
+               rt.classic.model.schedule.uni.limited.abstract_RTA.definitions
+               rt.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
+               rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
+               rt.classic.model.schedule.uni.limited.jlfp_instantiation.
+Require Import rt.classic.model.arrival.curves.bounds.
+Require Import rt.classic.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.schedule.uni.limited.busy_interval.
  
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/jlfp_instantiation.v b/classic/model/schedule/uni/limited/jlfp_instantiation.v
index 53df179d7494d69aff509eac4e16029a02acf7c0..fb3f45086b336f9dea6366fbb21b65b541e21e11 100644
--- a/classic/model/schedule/uni/limited/jlfp_instantiation.v
+++ b/classic/model/schedule/uni/limited/jlfp_instantiation.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.workload
-               rt.model.schedule.uni.schedule_of_task.
-Require Import rt.model.schedule.uni.limited.busy_interval
-               rt.model.schedule.uni.limited.abstract_RTA.definitions
-               rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.workload
+               rt.classic.model.schedule.uni.schedule_of_task.
+Require Import rt.classic.model.schedule.uni.limited.busy_interval
+               rt.classic.model.schedule.uni.limited.abstract_RTA.definitions
+               rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * JLFP instantiation of Interference and Interfering Workload *)
diff --git a/classic/model/schedule/uni/limited/platform/definitions.v b/classic/model/schedule/uni/limited/platform/definitions.v
index c9ceedfe314e3ff057e681090bd3182622287f26..a09cf7c4bbd191a6942d939b4ab2da9b3ff428ff 100644
--- a/classic/model/schedule/uni/limited/platform/definitions.v
+++ b/classic/model/schedule/uni/limited/platform/definitions.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task
-               rt.model.priority
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.service
-               rt.model.schedule.uni.basic.platform.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task
+               rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/platform/limited.v b/classic/model/schedule/uni/limited/platform/limited.v
index dfd07a387a0fcc9931a17be6195a9300a3d67a0a..7abffbc54ed77ad7e6b7209193e9a066061f9eb2 100644
--- a/classic/model/schedule/uni/limited/platform/limited.v
+++ b/classic/model/schedule/uni/limited/platform/limited.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.  
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task.
-Require Import rt.model.schedule.uni.schedule. 
-Require Export rt.model.schedule.uni.limited.platform.definitions.
-Require Export rt.model.schedule.uni.limited.platform.util.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task.
+Require Import rt.classic.model.schedule.uni.schedule. 
+Require Export rt.classic.model.schedule.uni.limited.platform.definitions.
+Require Export rt.classic.model.schedule.uni.limited.platform.util.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/platform/nonpreemptive.v b/classic/model/schedule/uni/limited/platform/nonpreemptive.v
index 28db0113204721eb4ebdba6d998b041b730c83b5..73625285a0d2a121c669923b161b97f2e65e33fd 100644
--- a/classic/model/schedule/uni/limited/platform/nonpreemptive.v
+++ b/classic/model/schedule/uni/limited/platform/nonpreemptive.v
@@ -1,13 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task 
-               rt.model.priority
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.service
-               rt.model.schedule.uni.basic.platform.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule.
-Require Export rt.model.schedule.uni.limited.platform.definitions.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task 
+               rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule.
+Require Export rt.classic.model.schedule.uni.limited.platform.definitions.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/platform/preemptive.v b/classic/model/schedule/uni/limited/platform/preemptive.v
index 83ea02c82501e8fb8f3ea9aea78095acc67fc9ce..6a56de0126e8c11cf4c4e2fd16b2943d3210c43b 100644
--- a/classic/model/schedule/uni/limited/platform/preemptive.v
+++ b/classic/model/schedule/uni/limited/platform/preemptive.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task
-               rt.model.priority
-               rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.service
-               rt.model.schedule.uni.basic.platform.
-Require Export rt.model.schedule.uni.limited.platform.definitions.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task
+               rt.classic.model.priority
+               rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.basic.platform.
+Require Export rt.classic.model.schedule.uni.limited.platform.definitions.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
index 35dce5a9e4004b8c549f67d34ff28b94ab832ae8..a0467f039e1b17f6440877f950a64f482f6a4c49 100644
--- a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
+++ b/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
@@ -1,17 +1,17 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.limited.platform.definitions
-               rt.model.schedule.uni.limited.busy_interval.
+Require Import rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.limited.platform.definitions
+               rt.classic.model.schedule.uni.limited.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Priority inversion is bounded *)
 (** In this module we prove that any priority inversion that occurs in the model with bounded 
-    nonpreemptive segments defined in module rt.model.schedule.uni.limited.platform.definitions 
+    nonpreemptive segments defined in module rt.classic.model.schedule.uni.limited.platform.definitions 
     is bounded. *)
 Module PriorityInversionIsBounded.
 
diff --git a/classic/model/schedule/uni/limited/rbf.v b/classic/model/schedule/uni/limited/rbf.v
index bb3c5931b5f1ff219a27c1e971754b2f7dad49ed..c84c90ba879f1b14f4fd5c9bf1c4f6d4428c7a11 100644
--- a/classic/model/schedule/uni/limited/rbf.v
+++ b/classic/model/schedule/uni/limited/rbf.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.job
-               rt.model.arrival.basic.task_arrival
-               rt.model.priority
-               rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.job
+               rt.classic.model.arrival.basic.task_arrival
+               rt.classic.model.priority
+               rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.curves.bounds.
+Require Import rt.classic.analysis.uni.arrival_curves.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 Module RBF.
diff --git a/classic/model/schedule/uni/limited/schedule.v b/classic/model/schedule/uni/limited/schedule.v
index f09ea867cc6ed6e20e7ea132cc824ec8f1325a6c..4feb38db72a2cc18787b53829defe89b5f592aba 100644
--- a/classic/model/schedule/uni/limited/schedule.v
+++ b/classic/model/schedule/uni/limited/schedule.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all. 
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.service
-               rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.service
+               rt.classic.model.schedule.uni.schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -133,7 +133,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
       Let job_lock_in_service (j: Job) := ε.
 
       (* Let's import definition of nonpreemptive schedule. *)
-      Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+      Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule.
 
       (* Next, we assume that the schedule is fully nonpreemptive. *) 
       Hypothesis H_is_nonpreemptive_schedule: 
diff --git a/classic/model/schedule/uni/nonpreemptive/platform.v b/classic/model/schedule/uni/nonpreemptive/platform.v
index 45b8a76f6230a758ccf1433df52f9951e40a9be9..a2a136546758efd206ecdd55c5234f1d7279c822 100644
--- a/classic/model/schedule/uni/nonpreemptive/platform.v
+++ b/classic/model/schedule/uni/nonpreemptive/platform.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.basic.platform.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.basic.platform.
+Require Import rt.classic.model.schedule.uni.nonpreemptive.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
  
 Module NonpreemptivePlatform.
diff --git a/classic/model/schedule/uni/nonpreemptive/schedule.v b/classic/model/schedule/uni/nonpreemptive/schedule.v
index 3048327daf6083ea80963afb581980e1fb11809e..53190c62e3838b12a7078df6130ce8fc60187bd8 100644
--- a/classic/model/schedule/uni/nonpreemptive/schedule.v
+++ b/classic/model/schedule/uni/nonpreemptive/schedule.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.job.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module NonpreemptiveSchedule.
diff --git a/classic/model/schedule/uni/response_time.v b/classic/model/schedule/uni/response_time.v
index 1d46b877fa45437f2b7fffce339a9d20684c5b85..de473b5bc94817197c5b9b3ae751d3ac2f93ceef 100644
--- a/classic/model/schedule/uni/response_time.v
+++ b/classic/model/schedule/uni/response_time.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ResponseTime.
diff --git a/classic/model/schedule/uni/schedulability.v b/classic/model/schedule/uni/schedulability.v
index bb187359784d33e96055e160c6c6f9cba99d4b3d..a47e5e2b4eaf402e6562cc9ec5867f4e184b00c3 100644
--- a/classic/model/schedule/uni/schedulability.v
+++ b/classic/model/schedule/uni/schedulability.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
-               rt.model.schedule.uni.schedule rt.model.schedule.uni.response_time.
+Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.response_time.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Schedulability.
diff --git a/classic/model/schedule/uni/schedule.v b/classic/model/schedule/uni/schedule.v
index f7af531b5751eef093ae6473fa2ae07731040553..84983fbbe265d6af82e7989530174d190c535e88 100644
--- a/classic/model/schedule/uni/schedule.v
+++ b/classic/model/schedule/uni/schedule.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module UniprocessorSchedule.
diff --git a/classic/model/schedule/uni/schedule_of_task.v b/classic/model/schedule/uni/schedule_of_task.v
index 41448b839f90b20dac338eb54eba86bcb5a52bdb..034f234b0d817a65e461e463871b86242757d35a 100644
--- a/classic/model/schedule/uni/schedule_of_task.v
+++ b/classic/model/schedule/uni/schedule_of_task.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ScheduleOfTask.
diff --git a/classic/model/schedule/uni/service.v b/classic/model/schedule/uni/service.v
index 3abcb64bed6c5d3461d2db29ccac565efcfc312d..0534dc4a86500678d351788bab481a92e23a9b98 100644
--- a/classic/model/schedule/uni/service.v
+++ b/classic/model/schedule/uni/service.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
-               rt.model.priority.
-Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule rt.classic.model.schedule.uni.workload.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Service.
diff --git a/classic/model/schedule/uni/susp/build_suspension_table.v b/classic/model/schedule/uni/susp/build_suspension_table.v
index 0e7a1411c2af49a4ccd407c1bf3fdeaab9b79ca4..2587e65fca788be381e7be4b7b6c6cde2453edac 100644
--- a/classic/model/schedule/uni/susp/build_suspension_table.v
+++ b/classic/model/schedule/uni/susp/build_suspension_table.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.suspension.
-Require Import rt.model.schedule.uni.susp.schedule.
+Require Import rt.classic.model.suspension.
+Require Import rt.classic.model.schedule.uni.susp.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
 
 (* In this file, we take any predicate that defines whether a job
diff --git a/classic/model/schedule/uni/susp/last_execution.v b/classic/model/schedule/uni/susp/last_execution.v
index 0a9c270c16d3eb7782f4967cc01005b228c742bf..862479e730cbd4b97b7917eeeeecb8563c612444 100644
--- a/classic/model/schedule/uni/susp/last_execution.v
+++ b/classic/model/schedule/uni/susp/last_execution.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file, we show how to compute the time instant after the last
diff --git a/classic/model/schedule/uni/susp/platform.v b/classic/model/schedule/uni/susp/platform.v
index a54d9cd792f6bab4b01afbfa9ad2983005126e25..b74392ad41796f61cf86dd5c09833aba2a31fc2a 100644
--- a/classic/model/schedule/uni/susp/platform.v
+++ b/classic/model/schedule/uni/susp/platform.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.suspension
-               rt.model.priority.
-Require Import rt.model.schedule.uni.susp.schedule.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.suspension
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.susp.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module PlatformWithSuspensions.
diff --git a/classic/model/schedule/uni/susp/schedule.v b/classic/model/schedule/uni/susp/schedule.v
index eb9547714b56ebdca469e96928bc151fc0e93ab4..34fbc3c0a2f39a399bec91fe1e2e0c1c99888b11 100644
--- a/classic/model/schedule/uni/susp/schedule.v
+++ b/classic/model/schedule/uni/susp/schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.suspension
-               rt.model.priority.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.susp.suspension_intervals.
+Require Import rt.classic.model.arrival.basic.arrival_sequence rt.classic.model.suspension
+               rt.classic.model.priority.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.susp.suspension_intervals.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ScheduleWithSuspensions.
diff --git a/classic/model/schedule/uni/susp/suspension_intervals.v b/classic/model/schedule/uni/susp/suspension_intervals.v
index 7e5851a94e22b8fc011e3be5c80a86c3e500985c..32be91371fba5f3c66382b8fd964668e7805da71 100644
--- a/classic/model/schedule/uni/susp/suspension_intervals.v
+++ b/classic/model/schedule/uni/susp/suspension_intervals.v
@@ -1,9 +1,9 @@
 Require Import rt.util.all.
 
-Require Import rt.model.suspension.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.schedule.
-Require Import rt.model.schedule.uni.susp.last_execution.
+Require Import rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.schedule.
+Require Import rt.classic.model.schedule.uni.susp.last_execution.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module SuspensionIntervals.
diff --git a/classic/model/schedule/uni/susp/valid_schedule.v b/classic/model/schedule/uni/susp/valid_schedule.v
index 2ce70a2725fbb9d0300d832bce1a0961a69f3ab5..2c7975ef02b474aabb9503972c7d9ea2d2f7b997 100644
--- a/classic/model/schedule/uni/susp/valid_schedule.v
+++ b/classic/model/schedule/uni/susp/valid_schedule.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.priority rt.model.suspension.
-Require Import rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.susp.schedule
-               rt.model.schedule.uni.susp.platform.
+Require Import rt.classic.model.priority rt.classic.model.suspension.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.susp.schedule
+               rt.classic.model.schedule.uni.susp.platform.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/model/schedule/uni/sustainability.v b/classic/model/schedule/uni/sustainability.v
index fe76fa4c7f7dbfa0f0ac2f1b99c3ccb34d131f75..7a6c4d9f5738ab42514b6bd2e555667b07ae8328 100644
--- a/classic/model/schedule/uni/sustainability.v
+++ b/classic/model/schedule/uni/sustainability.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence
-               rt.model.schedule.uni.schedule
-               rt.model.schedule.uni.schedulability.
+Require Import rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.schedule.uni.schedule
+               rt.classic.model.schedule.uni.schedulability.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Sustainability.
diff --git a/classic/model/schedule/uni/transformation/construction.v b/classic/model/schedule/uni/transformation/construction.v
index c5e4099c20c2be146b022602cde32fed93fe3b51..665c8f874eaed9b3526e329860e528c3025cc4b6 100644
--- a/classic/model/schedule/uni/transformation/construction.v
+++ b/classic/model/schedule/uni/transformation/construction.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
-Require Import rt.model.schedule.uni.schedule.
+Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.schedule.uni.schedule.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path finfun.
 
 Module ScheduleConstruction.
diff --git a/classic/model/schedule/uni/workload.v b/classic/model/schedule/uni/workload.v
index 65bc4254c81f3ca3463ca7e16ed2da3a4888e313..0c2098531ded53299d7f9481348ca29b466a9ea3 100644
--- a/classic/model/schedule/uni/workload.v
+++ b/classic/model/schedule/uni/workload.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
-               rt.model.priority.
+Require Import rt.classic.model.time rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.arrival_sequence
+               rt.classic.model.priority.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Workload.
diff --git a/classic/model/suspension.v b/classic/model/suspension.v
index cce479f9d3f943fa8ef242a7f0df50748838fa9b..dbebb29f253f68d773fb860243bdb9fc01a82fb7 100644
--- a/classic/model/suspension.v
+++ b/classic/model/suspension.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.classic.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop.
 
 Module Suspension.