From 9271931f0ff5a1e4b1deca491556b475428e2053 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 18 Dec 2019 01:59:24 +0100
Subject: [PATCH] move restructured Prosa to top level
The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.
---
.gitlab-ci.yml | 4 ++--
README.md | 13 ++++++++++--
.../abstract/abstract_rta.v | 6 +++---
.../abstract/abstract_seq_rta.v | 8 ++++----
.../abstract/definitions.v | 4 ++--
.../abstract/ideal_jlfp_rta.v | 8 ++++----
.../abstract/run_to_completion.v | 4 ++--
.../abstract/search_space.v | 2 +-
.../concepts/busy_interval.v | 6 +++---
.../concepts/priority_inversion.v | 2 +-
.../concepts/request_bound_function.v | 6 +++---
.../concepts/schedulability.v | 4 ++--
.../definitions/carry_in.v | 4 ++--
.../definitions/job_properties.v | 2 +-
.../definitions/progress.v | 2 +-
.../definitions/task_schedule.v | 4 ++--
analysis/facts/behavior/all.v | 8 ++++++++
.../facts/behavior/arrivals.v | 2 +-
.../facts/behavior/completion.v | 4 ++--
.../facts/behavior/deadlines.v | 2 +-
.../facts/behavior/ideal_schedule.v | 6 +++---
.../facts/behavior/sequential.v | 2 +-
.../facts/behavior/service.v | 4 ++--
.../facts/behavior/service_of_jobs.v | 10 +++++-----
.../facts/behavior/task_arrivals.v | 2 +-
.../facts/behavior/workload.v | 4 ++--
.../facts/busy_interval.v | 12 +++++------
.../analysis => analysis}/facts/carry_in.v | 8 ++++----
.../analysis => analysis}/facts/edf.v | 4 ++--
.../facts/preemption/job/limited.v | 8 ++++----
.../facts/preemption/job/nonpreemptive.v | 8 ++++----
.../facts/preemption/job/preemptive.v | 4 ++--
.../facts/preemption/rtc_threshold/floating.v | 8 ++++----
.../rtc_threshold/job_preemptable.v | 6 +++---
.../facts/preemption/rtc_threshold/limited.v | 8 ++++----
.../preemption/rtc_threshold/nonpreemptive.v | 6 +++---
.../preemption/rtc_threshold/preemptive.v | 6 +++---
.../facts/preemption/task/floating.v | 6 +++---
.../facts/preemption/task/limited.v | 6 +++---
.../facts/preemption/task/nonpreemptive.v | 6 +++---
.../facts/preemption/task/preemptive.v | 6 +++---
.../facts/priority_inversion.v | 18 ++++++++---------
.../analysis => analysis}/facts/rbf.v | 6 +++---
.../facts/readiness/basic.v | 4 ++--
.../analysis => analysis}/facts/tdma.v | 2 +-
.../facts/transform/edf_opt.v | 14 ++++++-------
.../facts/transform/replace_at.v | 4 ++--
.../facts/transform/swaps.v | 4 ++--
.../transform/edf_trans.v | 4 ++--
.../analysis => analysis}/transform/prefix.v | 2 +-
.../analysis => analysis}/transform/swap.v | 2 +-
.../behavior => behavior}/README.md | 0
behavior/all.v | 6 ++++++
.../behavior => behavior}/arrival_sequence.v | 2 +-
{restructuring/behavior => behavior}/job.v | 2 +-
{restructuring/behavior => behavior}/ready.v | 2 +-
.../behavior => behavior}/schedule.v | 2 +-
.../behavior => behavior}/service.v | 2 +-
{restructuring/behavior => behavior}/time.v | 0
create_makefile.sh | 2 +-
{restructuring/model => model}/README.md | 0
.../aggregate/service_of_jobs.v | 2 +-
.../model => model}/aggregate/workload.v | 2 +-
.../preemption/fully_nonpreemptive.v | 2 +-
.../preemption/fully_preemptive.v | 2 +-
.../preemption/limited_preemptive.v | 2 +-
.../model => model}/preemption/parameter.v | 2 +-
.../model => model}/priority/classes.v | 2 +-
.../priority/deadline_monotonic.v | 2 +-
{restructuring/model => model}/priority/edf.v | 2 +-
.../model => model}/priority/fifo.v | 2 +-
.../priority/numeric_fixed_priority.v | 2 +-
.../model => model}/priority/rate_monotonic.v | 4 ++--
.../model => model}/processor/ideal.v | 2 +-
.../processor/multiprocessor.v | 2 +-
.../processor/platform_properties.v | 2 +-
.../model => model}/processor/spin.v | 2 +-
.../model => model}/processor/varspeed.v | 2 +-
.../model => model}/readiness/basic.v | 2 +-
.../model => model}/readiness/jitter.v | 2 +-
.../model => model}/readiness/suspension.v | 4 ++--
{restructuring/model => model}/schedule/edf.v | 2 +-
.../schedule/limited_preemptive.v | 2 +-
.../model => model}/schedule/nonpreemptive.v | 2 +-
.../schedule/preemption_time.v | 4 ++--
.../schedule/priority_driven.v | 6 +++---
.../model => model}/schedule/tdma.v | 4 ++--
.../schedule/work_conserving.v | 2 +-
.../model => model}/task/absolute_deadline.v | 2 +-
.../model => model}/task/arrival/curves.v | 2 +-
.../model => model}/task/arrival/sporadic.v | 2 +-
.../model => model}/task/arrivals.v | 2 +-
{restructuring/model => model}/task/concept.v | 2 +-
.../task/preemption/floating_nonpreemptive.v | 4 ++--
.../task/preemption/fully_nonpreemptive.v | 2 +-
.../task/preemption/fully_preemptive.v | 2 +-
.../task/preemption/limited_preemptive.v | 4 ++--
.../task/preemption/parameters.v | 4 ++--
.../model => model}/task/sequentiality.v | 2 +-
.../model => model}/task/suspension/dynamic.v | 4 ++--
restructuring/README.md | 17 ----------------
restructuring/analysis/facts/behavior/all.v | 8 --------
restructuring/behavior/all.v | 6 ------
.../results => results}/edf/optimality.v | 6 +++---
.../results => results}/edf/rta/bounded_nps.v | 12 +++++------
.../results => results}/edf/rta/bounded_pi.v | 20 +++++++++----------
.../edf/rta/floating_nonpreemptive.v | 14 ++++++-------
.../edf/rta/fully_nonpreemptive.v | 14 ++++++-------
.../edf/rta/fully_preemptive.v | 14 ++++++-------
.../edf/rta/limited_preemptive.v | 14 ++++++-------
.../fixed_priority/rta/bounded_nps.v | 12 +++++------
.../fixed_priority/rta/bounded_pi.v | 10 +++++-----
.../rta/floating_nonpreemptive.v | 12 +++++------
.../fixed_priority/rta/fully_nonpreemptive.v | 12 +++++------
.../fixed_priority/rta/fully_preemptive.v | 12 +++++------
.../fixed_priority/rta/limited_preemptive.v | 12 +++++------
116 files changed, 294 insertions(+), 302 deletions(-)
rename {restructuring/analysis => analysis}/abstract/abstract_rta.v (99%)
rename {restructuring/analysis => analysis}/abstract/abstract_seq_rta.v (99%)
rename {restructuring/analysis => analysis}/abstract/definitions.v (99%)
rename {restructuring/analysis => analysis}/abstract/ideal_jlfp_rta.v (99%)
rename {restructuring/analysis => analysis}/abstract/run_to_completion.v (98%)
rename {restructuring/analysis => analysis}/abstract/search_space.v (99%)
rename {restructuring/analysis => analysis}/concepts/busy_interval.v (95%)
rename {restructuring/analysis => analysis}/concepts/priority_inversion.v (97%)
rename {restructuring/analysis => analysis}/concepts/request_bound_function.v (94%)
rename {restructuring/analysis => analysis}/concepts/schedulability.v (97%)
rename {restructuring/analysis => analysis}/definitions/carry_in.v (91%)
rename {restructuring/analysis => analysis}/definitions/job_properties.v (89%)
rename {restructuring/analysis => analysis}/definitions/progress.v (97%)
rename {restructuring/analysis => analysis}/definitions/task_schedule.v (93%)
create mode 100644 analysis/facts/behavior/all.v
rename {restructuring/analysis => analysis}/facts/behavior/arrivals.v (99%)
rename {restructuring/analysis => analysis}/facts/behavior/completion.v (98%)
rename {restructuring/analysis => analysis}/facts/behavior/deadlines.v (97%)
rename {restructuring/analysis => analysis}/facts/behavior/ideal_schedule.v (97%)
rename {restructuring/analysis => analysis}/facts/behavior/sequential.v (95%)
rename {restructuring/analysis => analysis}/facts/behavior/service.v (99%)
rename {restructuring/analysis => analysis}/facts/behavior/service_of_jobs.v (97%)
rename {restructuring/analysis => analysis}/facts/behavior/task_arrivals.v (94%)
rename {restructuring/analysis => analysis}/facts/behavior/workload.v (90%)
rename {restructuring/analysis => analysis}/facts/busy_interval.v (98%)
rename {restructuring/analysis => analysis}/facts/carry_in.v (98%)
rename {restructuring/analysis => analysis}/facts/edf.v (89%)
rename {restructuring/analysis => analysis}/facts/preemption/job/limited.v (97%)
rename {restructuring/analysis => analysis}/facts/preemption/job/nonpreemptive.v (95%)
rename {restructuring/analysis => analysis}/facts/preemption/job/preemptive.v (93%)
rename {restructuring/analysis => analysis}/facts/preemption/rtc_threshold/floating.v (81%)
rename {restructuring/analysis => analysis}/facts/preemption/rtc_threshold/job_preemptable.v (98%)
rename {restructuring/analysis => analysis}/facts/preemption/rtc_threshold/limited.v (95%)
rename {restructuring/analysis => analysis}/facts/preemption/rtc_threshold/nonpreemptive.v (92%)
rename {restructuring/analysis => analysis}/facts/preemption/rtc_threshold/preemptive.v (85%)
rename {restructuring/analysis => analysis}/facts/preemption/task/floating.v (96%)
rename {restructuring/analysis => analysis}/facts/preemption/task/limited.v (96%)
rename {restructuring/analysis => analysis}/facts/preemption/task/nonpreemptive.v (94%)
rename {restructuring/analysis => analysis}/facts/preemption/task/preemptive.v (91%)
rename {restructuring/analysis => analysis}/facts/priority_inversion.v (98%)
rename {restructuring/analysis => analysis}/facts/rbf.v (98%)
rename {restructuring/analysis => analysis}/facts/readiness/basic.v (90%)
rename {restructuring/analysis => analysis}/facts/tdma.v (99%)
rename {restructuring/analysis => analysis}/facts/transform/edf_opt.v (98%)
rename {restructuring/analysis => analysis}/facts/transform/replace_at.v (96%)
rename {restructuring/analysis => analysis}/facts/transform/swaps.v (99%)
rename {restructuring/analysis => analysis}/transform/edf_trans.v (96%)
rename {restructuring/analysis => analysis}/transform/prefix.v (98%)
rename {restructuring/analysis => analysis}/transform/swap.v (97%)
rename {restructuring/behavior => behavior}/README.md (100%)
create mode 100644 behavior/all.v
rename {restructuring/behavior => behavior}/arrival_sequence.v (98%)
rename {restructuring/behavior => behavior}/job.v (94%)
rename {restructuring/behavior => behavior}/ready.v (98%)
rename {restructuring/behavior => behavior}/schedule.v (98%)
rename {restructuring/behavior => behavior}/service.v (98%)
rename {restructuring/behavior => behavior}/time.v (100%)
rename {restructuring/model => model}/README.md (100%)
rename {restructuring/model => model}/aggregate/service_of_jobs.v (98%)
rename {restructuring/model => model}/aggregate/workload.v (97%)
rename {restructuring/model => model}/preemption/fully_nonpreemptive.v (91%)
rename {restructuring/model => model}/preemption/fully_preemptive.v (90%)
rename {restructuring/model => model}/preemption/limited_preemptive.v (97%)
rename {restructuring/model => model}/preemption/parameter.v (99%)
rename {restructuring/model => model}/priority/classes.v (99%)
rename {restructuring/model => model}/priority/deadline_monotonic.v (95%)
rename {restructuring/model => model}/priority/edf.v (95%)
rename {restructuring/model => model}/priority/fifo.v (95%)
rename {restructuring/model => model}/priority/numeric_fixed_priority.v (97%)
rename {restructuring/model => model}/priority/rate_monotonic.v (92%)
rename {restructuring/model => model}/processor/ideal.v (98%)
rename {restructuring/model => model}/processor/multiprocessor.v (98%)
rename {restructuring/model => model}/processor/platform_properties.v (96%)
rename {restructuring/model => model}/processor/spin.v (97%)
rename {restructuring/model => model}/processor/varspeed.v (97%)
rename {restructuring/model => model}/readiness/basic.v (94%)
rename {restructuring/model => model}/readiness/jitter.v (97%)
rename {restructuring/model => model}/readiness/suspension.v (96%)
rename {restructuring/model => model}/schedule/edf.v (98%)
rename {restructuring/model => model}/schedule/limited_preemptive.v (94%)
rename {restructuring/model => model}/schedule/nonpreemptive.v (95%)
rename {restructuring/model => model}/schedule/preemption_time.v (93%)
rename {restructuring/model => model}/schedule/priority_driven.v (91%)
rename {restructuring/model => model}/schedule/tdma.v (98%)
rename {restructuring/model => model}/schedule/work_conserving.v (97%)
rename {restructuring/model => model}/task/absolute_deadline.v (89%)
rename {restructuring/model => model}/task/arrival/curves.v (99%)
rename {restructuring/model => model}/task/arrival/sporadic.v (98%)
rename {restructuring/model => model}/task/arrivals.v (95%)
rename {restructuring/model => model}/task/concept.v (98%)
rename {restructuring/model => model}/task/preemption/floating_nonpreemptive.v (95%)
rename {restructuring/model => model}/task/preemption/fully_nonpreemptive.v (95%)
rename {restructuring/model => model}/task/preemption/fully_preemptive.v (95%)
rename {restructuring/model => model}/task/preemption/limited_preemptive.v (97%)
rename {restructuring/model => model}/task/preemption/parameters.v (98%)
rename {restructuring/model => model}/task/sequentiality.v (95%)
rename {restructuring/model => model}/task/suspension/dynamic.v (91%)
delete mode 100644 restructuring/README.md
delete mode 100644 restructuring/analysis/facts/behavior/all.v
delete mode 100644 restructuring/behavior/all.v
rename {restructuring/results => results}/edf/optimality.v (95%)
rename {restructuring/results => results}/edf/rta/bounded_nps.v (97%)
rename {restructuring/results => results}/edf/rta/bounded_pi.v (98%)
rename {restructuring/results => results}/edf/rta/floating_nonpreemptive.v (93%)
rename {restructuring/results => results}/edf/rta/fully_nonpreemptive.v (93%)
rename {restructuring/results => results}/edf/rta/fully_preemptive.v (93%)
rename {restructuring/results => results}/edf/rta/limited_preemptive.v (94%)
rename {restructuring/results => results}/fixed_priority/rta/bounded_nps.v (96%)
rename {restructuring/results => results}/fixed_priority/rta/bounded_pi.v (98%)
rename {restructuring/results => results}/fixed_priority/rta/floating_nonpreemptive.v (93%)
rename {restructuring/results => results}/fixed_priority/rta/fully_nonpreemptive.v (93%)
rename {restructuring/results => results}/fixed_priority/rta/fully_preemptive.v (92%)
rename {restructuring/results => results}/fixed_priority/rta/limited_preemptive.v (94%)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0100d9605..717fffe3a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -143,8 +143,8 @@ proof-state:
dependencies:
- 1.9.0-coq-8.10
script:
- - find restructuring util -iname *.v | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
- - scripts/intersperse-proof-state.py `find restructuring util -iname *.v`
+ - find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
+ - scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
- cd with-proof-state/
- ln -s ../scripts/
- ln -s ../_CoqProject
diff --git a/README.md b/README.md
index befa2f077..dc7427a9a 100644
--- a/README.md
+++ b/README.md
@@ -16,12 +16,21 @@ Please see the [list of publications](http://prosa.mpi-sws.org/documentation.htm
## Directory and Module Structure
-The directory and module structure is currently undergoing a fundamental reorganization.
+The directory and module structure is organized as follows. First, the main parts, of which there are currently four.
+
+- [behavior/](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
+- [model/](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate.
+- [analysis/](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
+- [results/](results/): The `results` namespace contains all **high-level analysis results**.
+
+
+In future work, there will also (again) be an `implementation` or `examples` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
+
+Furthermore, there are a couple of additional folders and namespaces.
- [classic/](classic/): This module contains the "classic" version of Prosa as first presented at ECRTS'16.
All results published prior to 2020 build on this "classic" version of Prosa.
- [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
-- [restructuring/](restructuring/): The new, refactored version of Prosa. Currently still under heavy development. This part of Prosa will soon move out of the `restructuring` namespace.
- [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
## Dependencies
diff --git a/restructuring/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/abstract_rta.v
rename to analysis/abstract/abstract_rta.v
index 9351b3056..446eff6eb 100644
--- a/restructuring/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.abstract.search_space.
-Require Export rt.restructuring.analysis.abstract.run_to_completion.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.abstract.search_space.
+Require Export rt.analysis.abstract.run_to_completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/abstract_seq_rta.v
rename to analysis/abstract/abstract_seq_rta.v
index 5946e2aca..bb09b5d2c 100644
--- a/restructuring/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.definitions.task_schedule.
-Require Export rt.restructuring.analysis.facts.rbf.
-Require Export rt.restructuring.analysis.facts.behavior.task_arrivals.
-Require Export rt.restructuring.analysis.abstract.abstract_rta.
+Require Export rt.analysis.definitions.task_schedule.
+Require Export rt.analysis.facts.rbf.
+Require Export rt.analysis.facts.behavior.task_arrivals.
+Require Export rt.analysis.abstract.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
similarity index 99%
rename from restructuring/analysis/abstract/definitions.v
rename to analysis/abstract/definitions.v
index 3d3d5c05e..5bbb12e05 100644
--- a/restructuring/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** * Definitions for Abstract Response-Time Analysis *)
(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA)
diff --git a/restructuring/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/ideal_jlfp_rta.v
rename to analysis/abstract/ideal_jlfp_rta.v
index 8b1d173e8..153df7665 100644
--- a/restructuring/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,13 +1,13 @@
-Require Export rt.restructuring.analysis.concepts.priority_inversion.
-Require Export rt.restructuring.analysis.abstract.abstract_seq_rta.
+Require Export rt.analysis.concepts.priority_inversion.
+Require Export rt.analysis.abstract.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** In this file we consider an ideal uni-processor ... *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** ... and classic model of readiness without jitter and no
self-suspensions, where pending jobs are always ready. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
(** In this module we instantiate functions Interference and Interfering Workload
diff --git a/restructuring/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
similarity index 98%
rename from restructuring/analysis/abstract/run_to_completion.v
rename to analysis/abstract/run_to_completion.v
index 53597c8e6..e00ebe39b 100644
--- a/restructuring/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Export rt.restructuring.analysis.abstract.definitions.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.analysis.abstract.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
similarity index 99%
rename from restructuring/analysis/abstract/search_space.v
rename to analysis/abstract/search_space.v
index f40ecc21a..8bc34c281 100644
--- a/restructuring/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,6 +1,6 @@
Require Import rt.util.epsilon.
Require Import rt.util.tactics.
-Require Import rt.restructuring.model.task.concept.
+Require Import rt.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Reduction of the search space for Abstract RTA *)
diff --git a/restructuring/analysis/concepts/busy_interval.v b/analysis/concepts/busy_interval.v
similarity index 95%
rename from restructuring/analysis/concepts/busy_interval.v
rename to analysis/concepts/busy_interval.v
index 84620629c..5e613bdaf 100644
--- a/restructuring/analysis/concepts/busy_interval.v
+++ b/analysis/concepts/busy_interval.v
@@ -1,9 +1,9 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.model.priority.classes.
+Require Export rt.analysis.facts.behavior.completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** * Busy Interval for JLFP-models *)
(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
diff --git a/restructuring/analysis/concepts/priority_inversion.v b/analysis/concepts/priority_inversion.v
similarity index 97%
rename from restructuring/analysis/concepts/priority_inversion.v
rename to analysis/concepts/priority_inversion.v
index a90e9f672..6278e9730 100644
--- a/restructuring/analysis/concepts/priority_inversion.v
+++ b/analysis/concepts/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.concepts.busy_interval.
+Require Export rt.analysis.concepts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/analysis/concepts/request_bound_function.v
similarity index 94%
rename from restructuring/analysis/concepts/request_bound_function.v
rename to analysis/concepts/request_bound_function.v
index 13aab3c1e..f531fa0fa 100644
--- a/restructuring/analysis/concepts/request_bound_function.v
+++ b/analysis/concepts/request_bound_function.v
@@ -1,10 +1,10 @@
-Require Export rt.restructuring.model.task.arrival.curves.
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.task.arrival.curves.
+Require Export rt.model.priority.classes.
(** The following definitions assume ideal uni-processor schedules. This
restriction exists for historic reasons; the defined concepts could be
generalized in future work. *)
-Require Import rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Import rt.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/concepts/schedulability.v b/analysis/concepts/schedulability.v
similarity index 97%
rename from restructuring/analysis/concepts/schedulability.v
rename to analysis/concepts/schedulability.v
index 8ecedc8d0..4cffcb4f8 100644
--- a/restructuring/analysis/concepts/schedulability.v
+++ b/analysis/concepts/schedulability.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Import rt.restructuring.model.task.absolute_deadline.
+Require Export rt.analysis.facts.behavior.completion.
+Require Import rt.model.task.absolute_deadline.
Section Task.
Context {Task : TaskType}.
diff --git a/restructuring/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
similarity index 91%
rename from restructuring/analysis/definitions/carry_in.v
rename to analysis/definitions/carry_in.v
index ac0eee1af..55a3453c5 100644
--- a/restructuring/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** * No Carry-In *)
(** In this module we define the notion of no carry-in time for uni-processor schedulers. *)
diff --git a/restructuring/analysis/definitions/job_properties.v b/analysis/definitions/job_properties.v
similarity index 89%
rename from restructuring/analysis/definitions/job_properties.v
rename to analysis/definitions/job_properties.v
index 543f91039..707ebee08 100644
--- a/restructuring/analysis/definitions/job_properties.v
+++ b/analysis/definitions/job_properties.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
From mathcomp Require Export eqtype ssrnat.
(** In this section, we introduce properties of a job. *)
diff --git a/restructuring/analysis/definitions/progress.v b/analysis/definitions/progress.v
similarity index 97%
rename from restructuring/analysis/definitions/progress.v
rename to analysis/definitions/progress.v
index de794d26c..f36e412c2 100644
--- a/restructuring/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.service.
(** * Job Progress (or Lack Thereof) *)
diff --git a/restructuring/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
similarity index 93%
rename from restructuring/analysis/definitions/task_schedule.v
rename to analysis/definitions/task_schedule.v
index a5ee28f97..19d851306 100644
--- a/restructuring/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Export rt.model.task.concept.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/analysis/facts/behavior/all.v b/analysis/facts/behavior/all.v
new file mode 100644
index 000000000..b5904f4ea
--- /dev/null
+++ b/analysis/facts/behavior/all.v
@@ -0,0 +1,8 @@
+Require Export rt.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.service_of_jobs.
+Require Export rt.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Export rt.analysis.facts.behavior.sequential.
+Require Export rt.analysis.facts.behavior.arrivals.
+Require Export rt.analysis.facts.behavior.deadlines.
+Require Export rt.analysis.facts.behavior.workload.
diff --git a/restructuring/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
similarity index 99%
rename from restructuring/analysis/facts/behavior/arrivals.v
rename to analysis/facts/behavior/arrivals.v
index a9eb167ab..fbb7bf68f 100644
--- a/restructuring/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
Require Export rt.util.all.
(** In this section, we relate job readiness to [has_arrived]. *)
diff --git a/restructuring/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
similarity index 98%
rename from restructuring/analysis/facts/behavior/completion.v
rename to analysis/facts/behavior/completion.v
index d32bb55fb..f9d9a6ce4 100644
--- a/restructuring/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.analysis.facts.behavior.service.
+Require Export rt.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
diff --git a/restructuring/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/deadlines.v
rename to analysis/facts/behavior/deadlines.v
index 777c92c79..097c6d6a6 100644
--- a/restructuring/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.completion.
(** In this file, we observe basic properties of the behavioral job
model w.r.t. deadlines. *)
diff --git a/restructuring/analysis/facts/behavior/ideal_schedule.v b/analysis/facts/behavior/ideal_schedule.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/ideal_schedule.v
rename to analysis/facts/behavior/ideal_schedule.v
index ee7d8f705..b1bdca2a4 100644
--- a/restructuring/analysis/facts/behavior/ideal_schedule.v
+++ b/analysis/facts/behavior/ideal_schedule.v
@@ -1,10 +1,10 @@
From mathcomp Require Import all_ssreflect.
Require Export rt.util.all.
-Require Export rt.restructuring.model.processor.platform_properties.
-Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.model.processor.platform_properties.
+Require Export rt.analysis.facts.behavior.service.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
diff --git a/restructuring/analysis/facts/behavior/sequential.v b/analysis/facts/behavior/sequential.v
similarity index 95%
rename from restructuring/analysis/facts/behavior/sequential.v
rename to analysis/facts/behavior/sequential.v
index 75efd68ab..7c115ca56 100644
--- a/restructuring/analysis/facts/behavior/sequential.v
+++ b/analysis/facts/behavior/sequential.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.sequentiality.
+Require Export rt.model.task.sequentiality.
Section ExecutionOrder.
(** Consider any type of job associated with any type of tasks... *)
diff --git a/restructuring/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
similarity index 99%
rename from restructuring/analysis/facts/behavior/service.v
rename to analysis/facts/behavior/service.v
index 1d84947bc..c0852c0df 100644
--- a/restructuring/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -1,6 +1,6 @@
Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.processor.platform_properties.
+Require Export rt.behavior.all.
+Require Export rt.model.processor.platform_properties.
From mathcomp Require Import ssrnat ssrbool fintype.
diff --git a/restructuring/analysis/facts/behavior/service_of_jobs.v b/analysis/facts/behavior/service_of_jobs.v
similarity index 97%
rename from restructuring/analysis/facts/behavior/service_of_jobs.v
rename to analysis/facts/behavior/service_of_jobs.v
index 5e3bfb7ab..627a27770 100644
--- a/restructuring/analysis/facts/behavior/service_of_jobs.v
+++ b/analysis/facts/behavior/service_of_jobs.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.aggregate.service_of_jobs.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Import rt.restructuring.model.processor.ideal.
+Require Export rt.model.aggregate.workload.
+Require Export rt.model.aggregate.service_of_jobs.
+Require Export rt.analysis.facts.behavior.completion.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Import rt.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/behavior/task_arrivals.v b/analysis/facts/behavior/task_arrivals.v
similarity index 94%
rename from restructuring/analysis/facts/behavior/task_arrivals.v
rename to analysis/facts/behavior/task_arrivals.v
index 539c0c4de..96e695dc0 100644
--- a/restructuring/analysis/facts/behavior/task_arrivals.v
+++ b/analysis/facts/behavior/task_arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.arrivals.
+Require Export rt.model.task.arrivals.
(** In this file we provide basic properties related to tasks on arrival sequences. *)
Section TaskArrivals.
diff --git a/restructuring/analysis/facts/behavior/workload.v b/analysis/facts/behavior/workload.v
similarity index 90%
rename from restructuring/analysis/facts/behavior/workload.v
rename to analysis/facts/behavior/workload.v
index f8286ab2b..c7a352543 100644
--- a/restructuring/analysis/facts/behavior/workload.v
+++ b/analysis/facts/behavior/workload.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.model.aggregate.workload.
+Require Export rt.analysis.facts.behavior.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/busy_interval.v b/analysis/facts/busy_interval.v
similarity index 98%
rename from restructuring/analysis/facts/busy_interval.v
rename to analysis/facts/busy_interval.v
index 9275bab69..aeb1e61c5 100644
--- a/restructuring/analysis/facts/busy_interval.v
+++ b/analysis/facts/busy_interval.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.concepts.priority_inversion.
-Require Export rt.restructuring.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.work_conserving.
+Require Export rt.analysis.concepts.priority_inversion.
+Require Export rt.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
diff --git a/restructuring/analysis/facts/carry_in.v b/analysis/facts/carry_in.v
similarity index 98%
rename from restructuring/analysis/facts/carry_in.v
rename to analysis/facts/carry_in.v
index 35b0cb56c..e4832432f 100644
--- a/restructuring/analysis/facts/carry_in.v
+++ b/analysis/facts/carry_in.v
@@ -1,12 +1,12 @@
-Require Export rt.restructuring.analysis.definitions.carry_in.
-Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Export rt.analysis.definitions.carry_in.
+Require Export rt.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * Existence of No Carry-In Instant *)
diff --git a/restructuring/analysis/facts/edf.v b/analysis/facts/edf.v
similarity index 89%
rename from restructuring/analysis/facts/edf.v
rename to analysis/facts/edf.v
index 10cd3dc4c..f85bd1a19 100644
--- a/restructuring/analysis/facts/edf.v
+++ b/analysis/facts/edf.v
@@ -1,5 +1,5 @@
-Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.task.absolute_deadline.
+Require Import rt.model.priority.edf.
+Require Import rt.model.task.absolute_deadline.
(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.
diff --git a/restructuring/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
similarity index 97%
rename from restructuring/analysis/facts/preemption/job/limited.v
rename to analysis/facts/preemption/job/limited.v
index 4241860f0..76cb3846a 100644
--- a/restructuring/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.limited_preemptive.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.limited_preemptive.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
similarity index 95%
rename from restructuring/analysis/facts/preemption/job/nonpreemptive.v
rename to analysis/facts/preemption/job/nonpreemptive.v
index 029b0a24d..2154889ff 100644
--- a/restructuring/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.schedule.nonpreemptive.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.model.schedule.nonpreemptive.
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
similarity index 93%
rename from restructuring/analysis/facts/preemption/job/preemptive.v
rename to analysis/facts/preemption/job/preemptive.v
index f2af28e1f..3d06928e6 100644
--- a/restructuring/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.fully_preemptive.
+Require Export rt.model.task.preemption.parameters.
+Require Import rt.model.preemption.fully_preemptive.
(** * Preemptions in Fully Preemptive Model *)
(** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
similarity index 81%
rename from restructuring/analysis/facts/preemption/rtc_threshold/floating.v
rename to analysis/facts/preemption/rtc_threshold/floating.v
index e5be78e16..e376c23e1 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
+Require Export rt.analysis.facts.preemption.task.floating.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
similarity index 98%
rename from restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
rename to analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 03dd0428b..9a4f1c349 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.facts.behavior.all.
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.facts.behavior.all.
+Require Export rt.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
(** In this section, we provide a few basic properties
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
similarity index 95%
rename from restructuring/analysis/facts/preemption/rtc_threshold/limited.v
rename to analysis/facts/preemption/rtc_threshold/limited.v
index 781948940..bab0d88aa 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.analysis.facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.analysis.facts.preemption.task.limited.
+Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
similarity index 92%
rename from restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
rename to analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index f1dcc2704..70aa48a16 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
+Require Export rt.analysis.facts.preemption.job.nonpreemptive.
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
similarity index 85%
rename from restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
rename to analysis/facts/preemption/rtc_threshold/preemptive.v
index e2e9b6a0a..e92b55560 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -1,6 +1,6 @@
-Require Import rt.restructuring.model.preemption.fully_preemptive.
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-Require Import rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Import rt.model.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
+Require Import rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
similarity index 96%
rename from restructuring/analysis/facts/preemption/task/floating.v
rename to analysis/facts/preemption/task/floating.v
index e76c73048..28fa12479 100644
--- a/restructuring/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.limited.
+Require Export rt.analysis.facts.preemption.job.limited.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
similarity index 96%
rename from restructuring/analysis/facts/preemption/task/limited.v
rename to analysis/facts/preemption/task/limited.v
index 88ba4d0de..a62f17823 100644
--- a/restructuring/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.limited.
+Require Export rt.analysis.facts.preemption.job.limited.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
similarity index 94%
rename from restructuring/analysis/facts/preemption/task/nonpreemptive.v
rename to analysis/facts/preemption/task/nonpreemptive.v
index 62786996d..8e3d584c4 100644
--- a/restructuring/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
+Require Export rt.analysis.facts.preemption.job.nonpreemptive.
-Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
similarity index 91%
rename from restructuring/analysis/facts/preemption/task/preemptive.v
rename to analysis/facts/preemption/task/preemptive.v
index 8b17d3c66..4c95a45a7 100644
--- a/restructuring/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.facts.preemption.job.preemptive.
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
(** * Platform for Fully Preemptive Model *)
(** In this section, we prove that instantiation of functions
diff --git a/restructuring/analysis/facts/priority_inversion.v b/analysis/facts/priority_inversion.v
similarity index 98%
rename from restructuring/analysis/facts/priority_inversion.v
rename to analysis/facts/priority_inversion.v
index 1e1eb9c93..ca247335f 100644
--- a/restructuring/analysis/facts/priority_inversion.v
+++ b/analysis/facts/priority_inversion.v
@@ -1,19 +1,19 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.concepts.busy_interval.
-Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Export rt.model.task.preemption.parameters.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.behavior.ideal_schedule.
+Require Export rt.model.schedule.work_conserving.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.concepts.busy_interval.
+Require Export rt.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout the file we assume for the classic Liu & Layland model
of readiness without jitter and no self-suspensions, where
pending jobs are always ready. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** In preparation of the derivation of the priority inversion bound, we
establish two basic facts on preemption times. *)
diff --git a/restructuring/analysis/facts/rbf.v b/analysis/facts/rbf.v
similarity index 98%
rename from restructuring/analysis/facts/rbf.v
rename to analysis/facts/rbf.v
index 5cdc4ffbc..af0888348 100644
--- a/restructuring/analysis/facts/rbf.v
+++ b/analysis/facts/rbf.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.facts.behavior.workload.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.concepts.request_bound_function.
+Require Export rt.analysis.facts.behavior.workload.
+Require Export rt.analysis.definitions.job_properties.
+Require Export rt.analysis.concepts.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
similarity index 90%
rename from restructuring/analysis/facts/readiness/basic.v
rename to analysis/facts/readiness/basic.v
index a58055a18..df77d613d 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -1,7 +1,7 @@
-Require Import rt.restructuring.analysis.facts.behavior.completion.
+Require Import rt.analysis.facts.behavior.completion.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
Section LiuAndLaylandReadiness.
(** Consider any kind of jobs... *)
diff --git a/restructuring/analysis/facts/tdma.v b/analysis/facts/tdma.v
similarity index 99%
rename from restructuring/analysis/facts/tdma.v
rename to analysis/facts/tdma.v
index c95193301..830e1258e 100644
--- a/restructuring/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.tdma.
+Require Export rt.model.schedule.tdma.
Require Import rt.util.all.
From mathcomp Require Import div.
diff --git a/restructuring/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
similarity index 98%
rename from restructuring/analysis/facts/transform/edf_opt.v
rename to analysis/facts/transform/edf_opt.v
index 993ac7789..11f798498 100644
--- a/restructuring/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,9 +1,9 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.model.schedule.edf.
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.transform.edf_trans.
-Require Export rt.restructuring.analysis.facts.transform.swaps.
-Require Export rt.restructuring.analysis.facts.readiness.basic.
+Require Export rt.model.schedule.edf.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.transform.edf_trans.
+Require Export rt.analysis.facts.transform.swaps.
+Require Export rt.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
@@ -12,9 +12,9 @@ Require Export rt.restructuring.analysis.facts.readiness.basic.
the obtained EDF schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
diff --git a/restructuring/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
similarity index 96%
rename from restructuring/analysis/facts/transform/replace_at.v
rename to analysis/facts/transform/replace_at.v
index 29a4d8805..a1cc634a6 100644
--- a/restructuring/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.transform.swap.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.analysis.transform.swap.
+Require Export rt.analysis.facts.behavior.completion.
(** In this file, we make a few simple observations about schedules with
replacements. *)
diff --git a/restructuring/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
similarity index 99%
rename from restructuring/analysis/facts/transform/swaps.v
rename to analysis/facts/transform/swaps.v
index 1b27adf6b..8ed2b4160 100644
--- a/restructuring/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.facts.transform.replace_at.
-Require Export rt.restructuring.analysis.facts.behavior.deadlines.
+Require Export rt.analysis.facts.transform.replace_at.
+Require Export rt.analysis.facts.behavior.deadlines.
(** In this file, we establish invariants about schedules in which two
allocations have been swapped, as for instance it is done in the
diff --git a/restructuring/analysis/transform/edf_trans.v b/analysis/transform/edf_trans.v
similarity index 96%
rename from restructuring/analysis/transform/edf_trans.v
rename to analysis/transform/edf_trans.v
index 1fd663234..cf96a6506 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/analysis/transform/edf_trans.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.transform.prefix.
-Require Export rt.restructuring.analysis.transform.swap.
+Require Export rt.analysis.transform.prefix.
+Require Export rt.analysis.transform.swap.
(** In this file we define the EDF transformation of a schedule, which turns a
(finite prefix of a) schedule into an EDF schedule. This operation is at
diff --git a/restructuring/analysis/transform/prefix.v b/analysis/transform/prefix.v
similarity index 98%
rename from restructuring/analysis/transform/prefix.v
rename to analysis/transform/prefix.v
index 90e5ee75d..feb160289 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.facts.behavior.all.
+Require Export rt.analysis.facts.behavior.all.
(** This file provides an operation that transforms a finite prefix of
a given schedule by applying a point-wise transformation to each
diff --git a/restructuring/analysis/transform/swap.v b/analysis/transform/swap.v
similarity index 97%
rename from restructuring/analysis/transform/swap.v
rename to analysis/transform/swap.v
index 443aa3987..eec37bca1 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof. *)
diff --git a/restructuring/behavior/README.md b/behavior/README.md
similarity index 100%
rename from restructuring/behavior/README.md
rename to behavior/README.md
diff --git a/behavior/all.v b/behavior/all.v
new file mode 100644
index 000000000..a2c66f74b
--- /dev/null
+++ b/behavior/all.v
@@ -0,0 +1,6 @@
+Require Export rt.behavior.time.
+Require Export rt.behavior.job.
+Require Export rt.behavior.arrival_sequence.
+Require Export rt.behavior.schedule.
+Require Export rt.behavior.service.
+Require Export rt.behavior.ready.
diff --git a/restructuring/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
similarity index 98%
rename from restructuring/behavior/arrival_sequence.v
rename to behavior/arrival_sequence.v
index 564c6f4e1..bcc8dfa50 100644
--- a/restructuring/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
-Require Export rt.restructuring.behavior.job.
+Require Export rt.behavior.job.
Require Export rt.util.notation.
(** This module contains basic definitions and properties of job arrival
diff --git a/restructuring/behavior/job.v b/behavior/job.v
similarity index 94%
rename from restructuring/behavior/job.v
rename to behavior/job.v
index df1d07851..6d10d08d9 100644
--- a/restructuring/behavior/job.v
+++ b/behavior/job.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.time.
+Require Export rt.behavior.time.
From mathcomp Require Export eqtype ssrnat.
(** * Notion of a Job Type *)
diff --git a/restructuring/behavior/ready.v b/behavior/ready.v
similarity index 98%
rename from restructuring/behavior/ready.v
rename to behavior/ready.v
index 90361a662..fac5542f6 100644
--- a/restructuring/behavior/ready.v
+++ b/behavior/ready.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.service.
+Require Export rt.behavior.service.
(** * Readiness of a Job *)
diff --git a/restructuring/behavior/schedule.v b/behavior/schedule.v
similarity index 98%
rename from restructuring/behavior/schedule.v
rename to behavior/schedule.v
index cba3f33eb..25009b418 100644
--- a/restructuring/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.arrival_sequence.
+Require Export rt.behavior.arrival_sequence.
(** * Generic Processor State *)
diff --git a/restructuring/behavior/service.v b/behavior/service.v
similarity index 98%
rename from restructuring/behavior/service.v
rename to behavior/service.v
index 6223722de..0cbb438a5 100644
--- a/restructuring/behavior/service.v
+++ b/behavior/service.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.schedule.
+Require Export rt.behavior.schedule.
Section Service.
diff --git a/restructuring/behavior/time.v b/behavior/time.v
similarity index 100%
rename from restructuring/behavior/time.v
rename to behavior/time.v
diff --git a/create_makefile.sh b/create_makefile.sh
index 8a7176c66..973076b38 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -10,7 +10,7 @@ do
FIND_OPTS+=( ! -path './classic/*' )
;;
--only-classic)
- FIND_OPTS+=( ! -path './restructuring/*' )
+ FIND_OPTS+=( ! -path './analysis/*' ! -path './behavior/*' ! -path './model/*' ! -path './results/*')
;;
*)
echo "Unrecognized option: $1"
diff --git a/restructuring/model/README.md b/model/README.md
similarity index 100%
rename from restructuring/model/README.md
rename to model/README.md
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/model/aggregate/service_of_jobs.v
similarity index 98%
rename from restructuring/model/aggregate/service_of_jobs.v
rename to model/aggregate/service_of_jobs.v
index e6ed0146f..908d2de04 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/model/aggregate/service_of_jobs.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * Service Received by Sets of Jobs *)
diff --git a/restructuring/model/aggregate/workload.v b/model/aggregate/workload.v
similarity index 97%
rename from restructuring/model/aggregate/workload.v
rename to model/aggregate/workload.v
index 8394feac8..8054e7911 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * Cumulative Workload of Sets of Jobs *)
diff --git a/restructuring/model/preemption/fully_nonpreemptive.v b/model/preemption/fully_nonpreemptive.v
similarity index 91%
rename from restructuring/model/preemption/fully_nonpreemptive.v
rename to model/preemption/fully_nonpreemptive.v
index 6915071ab..d70545dcb 100644
--- a/restructuring/model/preemption/fully_nonpreemptive.v
+++ b/model/preemption/fully_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
(** * Preemption Model: Fully Non-Preemptive Jobs *)
(** In this section, we instantiate [job_preemptable] for the fully
diff --git a/restructuring/model/preemption/fully_preemptive.v b/model/preemption/fully_preemptive.v
similarity index 90%
rename from restructuring/model/preemption/fully_preemptive.v
rename to model/preemption/fully_preemptive.v
index d982b2dfa..a02d2ae24 100644
--- a/restructuring/model/preemption/fully_preemptive.v
+++ b/model/preemption/fully_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
(** * Preemption Model: Fully Preemptive Jobs *)
(** In this section, we instantiate [job_preemptable] for the fully preemptive
diff --git a/restructuring/model/preemption/limited_preemptive.v b/model/preemption/limited_preemptive.v
similarity index 97%
rename from restructuring/model/preemption/limited_preemptive.v
rename to model/preemption/limited_preemptive.v
index 98fdca850..105401d19 100644
--- a/restructuring/model/preemption/limited_preemptive.v
+++ b/model/preemption/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
(** * Job Model Parameter for Preemption Points *)
diff --git a/restructuring/model/preemption/parameter.v b/model/preemption/parameter.v
similarity index 99%
rename from restructuring/model/preemption/parameter.v
rename to model/preemption/parameter.v
index 970d59dd0..ce601d511 100644
--- a/restructuring/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -1,5 +1,5 @@
Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Job-Level Preemption Model *)
(** There are many equivalent ways to represent at which points in time a job
diff --git a/restructuring/model/priority/classes.v b/model/priority/classes.v
similarity index 99%
rename from restructuring/model/priority/classes.v
rename to model/priority/classes.v
index ca8a406a3..06fe6efad 100644
--- a/restructuring/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
Require Export rt.util.rel.
Require Export rt.util.list.
diff --git a/restructuring/model/priority/deadline_monotonic.v b/model/priority/deadline_monotonic.v
similarity index 95%
rename from restructuring/model/priority/deadline_monotonic.v
rename to model/priority/deadline_monotonic.v
index 6236df717..0a25f5699 100644
--- a/restructuring/model/priority/deadline_monotonic.v
+++ b/model/priority/deadline_monotonic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * Deadline-Monotonic Fixed-Priority Policy *)
diff --git a/restructuring/model/priority/edf.v b/model/priority/edf.v
similarity index 95%
rename from restructuring/model/priority/edf.v
rename to model/priority/edf.v
index 6aaa625cd..e0bfe8f3c 100644
--- a/restructuring/model/priority/edf.v
+++ b/model/priority/edf.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * EDF Priority Policy *)
diff --git a/restructuring/model/priority/fifo.v b/model/priority/fifo.v
similarity index 95%
rename from restructuring/model/priority/fifo.v
rename to model/priority/fifo.v
index 67dfb099c..1c0a36568 100644
--- a/restructuring/model/priority/fifo.v
+++ b/model/priority/fifo.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * FIFO Priority Policy *)
diff --git a/restructuring/model/priority/numeric_fixed_priority.v b/model/priority/numeric_fixed_priority.v
similarity index 97%
rename from restructuring/model/priority/numeric_fixed_priority.v
rename to model/priority/numeric_fixed_priority.v
index c86717b6f..bc5a698b3 100644
--- a/restructuring/model/priority/numeric_fixed_priority.v
+++ b/model/priority/numeric_fixed_priority.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.priority.classes.
+Require Export rt.model.priority.classes.
(** * Numeric Fixed Task Priorities *)
diff --git a/restructuring/model/priority/rate_monotonic.v b/model/priority/rate_monotonic.v
similarity index 92%
rename from restructuring/model/priority/rate_monotonic.v
rename to model/priority/rate_monotonic.v
index 7d17f266f..bc3833046 100644
--- a/restructuring/model/priority/rate_monotonic.v
+++ b/model/priority/rate_monotonic.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.task.arrival.sporadic.
+Require Export rt.model.priority.classes.
+Require Export rt.model.task.arrival.sporadic.
(** * Rate-Monotonic Fixed-Priority Policy *)
diff --git a/restructuring/model/processor/ideal.v b/model/processor/ideal.v
similarity index 98%
rename from restructuring/model/processor/ideal.v
rename to model/processor/ideal.v
index 70ceea83c..5f5b83bc5 100644
--- a/restructuring/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -1,5 +1,5 @@
From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * The Ideal Uniprocessor Model *)
diff --git a/restructuring/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
similarity index 98%
rename from restructuring/model/processor/multiprocessor.v
rename to model/processor/multiprocessor.v
index 9c13ebcaf..ca02b538d 100644
--- a/restructuring/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -1,5 +1,5 @@
From mathcomp Require Export fintype.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Multiprocessor State *)
diff --git a/restructuring/model/processor/platform_properties.v b/model/processor/platform_properties.v
similarity index 96%
rename from restructuring/model/processor/platform_properties.v
rename to model/processor/platform_properties.v
index bf5e4825c..cd2ad2273 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/model/processor/platform_properties.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** To reason about classes of schedule types / processor models, we define the
following properties that group processor models into classes of similar
diff --git a/restructuring/model/processor/spin.v b/model/processor/spin.v
similarity index 97%
rename from restructuring/model/processor/spin.v
rename to model/processor/spin.v
index 42d23623a..5c1b708ed 100644
--- a/restructuring/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -1,5 +1,5 @@
From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** In the following, we define a processor state that includes the possibility
of spinning, where spinning jobs do not progress (= don't get any service).
diff --git a/restructuring/model/processor/varspeed.v b/model/processor/varspeed.v
similarity index 97%
rename from restructuring/model/processor/varspeed.v
rename to model/processor/varspeed.v
index 4e9967b82..e452f69f7 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -1,5 +1,5 @@
From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** In the following, we define a model of processors with variable execution
speeds.
diff --git a/restructuring/model/readiness/basic.v b/model/readiness/basic.v
similarity index 94%
rename from restructuring/model/readiness/basic.v
rename to model/readiness/basic.v
index 5c94fd67f..271e6499c 100644
--- a/restructuring/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Liu & Layland Readiness Model *)
diff --git a/restructuring/model/readiness/jitter.v b/model/readiness/jitter.v
similarity index 97%
rename from restructuring/model/readiness/jitter.v
rename to model/readiness/jitter.v
index d7579df1e..ab0b8b3b2 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
Require Import rt.util.nat.
diff --git a/restructuring/model/readiness/suspension.v b/model/readiness/suspension.v
similarity index 96%
rename from restructuring/model/readiness/suspension.v
rename to model/readiness/suspension.v
index b6c2e5214..5c9c5f2bc 100644
--- a/restructuring/model/readiness/suspension.v
+++ b/model/readiness/suspension.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.definitions.progress.
+Require Export rt.behavior.all.
+Require Export rt.analysis.definitions.progress.
Require Export rt.util.nat.
(** * Job Model Parameter for Jobs Exhibiting Self-Suspensions *)
diff --git a/restructuring/model/schedule/edf.v b/model/schedule/edf.v
similarity index 98%
rename from restructuring/model/schedule/edf.v
rename to model/schedule/edf.v
index 4d05ba0b2..cfe08f007 100644
--- a/restructuring/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Fully-Preemptive EDF Schedules *)
diff --git a/restructuring/model/schedule/limited_preemptive.v b/model/schedule/limited_preemptive.v
similarity index 94%
rename from restructuring/model/schedule/limited_preemptive.v
rename to model/schedule/limited_preemptive.v
index 3bf94581f..a9849974a 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/model/schedule/limited_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
(** * Preemption Model Compliance *)
diff --git a/restructuring/model/schedule/nonpreemptive.v b/model/schedule/nonpreemptive.v
similarity index 95%
rename from restructuring/model/schedule/nonpreemptive.v
rename to model/schedule/nonpreemptive.v
index 05e1852f3..6bff4dd09 100644
--- a/restructuring/model/schedule/nonpreemptive.v
+++ b/model/schedule/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Nonpreemptive Schedules *)
diff --git a/restructuring/model/schedule/preemption_time.v b/model/schedule/preemption_time.v
similarity index 93%
rename from restructuring/model/schedule/preemption_time.v
rename to model/schedule/preemption_time.v
index 8fb17776e..97508bc08 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/model/schedule/preemption_time.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.parameter.
+Require Export rt.model.preemption.parameter.
(** * Preemption Times *)
@@ -14,7 +14,7 @@ Require Export rt.restructuring.model.preemption.parameter.
ideal uniprocessor schedules. Lifting this assumption is future work. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
Section PreemptionTime.
diff --git a/restructuring/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
similarity index 91%
rename from restructuring/model/schedule/priority_driven.v
rename to model/schedule/priority_driven.v
index 49845a653..b66607e4c 100644
--- a/restructuring/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.schedule.preemption_time.
+Require Export rt.model.priority.classes.
+Require Export rt.model.schedule.preemption_time.
(** * Priority-Driven Schedules *)
@@ -13,7 +13,7 @@ Require Export rt.restructuring.model.schedule.preemption_time.
uniprocessor schedules. Removal of this limitation is future work. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
Section Priority.
diff --git a/restructuring/model/schedule/tdma.v b/model/schedule/tdma.v
similarity index 98%
rename from restructuring/model/schedule/tdma.v
rename to model/schedule/tdma.v
index 24ee5d529..c86e0425d 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,10 +1,10 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
Require Export rt.util.seqset.
Require Export rt.util.rel.
From mathcomp Require Import div.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
(** * TDMA Scheduling *)
diff --git a/restructuring/model/schedule/work_conserving.v b/model/schedule/work_conserving.v
similarity index 97%
rename from restructuring/model/schedule/work_conserving.v
rename to model/schedule/work_conserving.v
index 6d72faff1..335dff614 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/model/schedule/work_conserving.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Definition of Work Conservation *)
diff --git a/restructuring/model/task/absolute_deadline.v b/model/task/absolute_deadline.v
similarity index 89%
rename from restructuring/model/task/absolute_deadline.v
rename to model/task/absolute_deadline.v
index 86cc56f10..f9be6873c 100644
--- a/restructuring/model/task/absolute_deadline.v
+++ b/model/task/absolute_deadline.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
(** Given relative task deadlines and a mapping from jobs to tasks, we provide
the canonical definition of each job's absolute deadline, i.e.,
diff --git a/restructuring/model/task/arrival/curves.v b/model/task/arrival/curves.v
similarity index 99%
rename from restructuring/model/task/arrival/curves.v
rename to model/task/arrival/curves.v
index 649d3a62a..20f196236 100644
--- a/restructuring/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -1,5 +1,5 @@
Require Export rt.util.rel.
-Require Export rt.restructuring.model.task.arrivals.
+Require Export rt.model.task.arrivals.
(** * The Arbitrary Arrival Curves Model *)
diff --git a/restructuring/model/task/arrival/sporadic.v b/model/task/arrival/sporadic.v
similarity index 98%
rename from restructuring/model/task/arrival/sporadic.v
rename to model/task/arrival/sporadic.v
index f2e7f53bc..b154736e2 100644
--- a/restructuring/model/task/arrival/sporadic.v
+++ b/model/task/arrival/sporadic.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
(** * The Sporadic Task Model *)
diff --git a/restructuring/model/task/arrivals.v b/model/task/arrivals.v
similarity index 95%
rename from restructuring/model/task/arrivals.v
rename to model/task/arrivals.v
index 540571a58..5ba7bc383 100644
--- a/restructuring/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
(** In this module, we provide basic definitions concerning the job
arrivals of a given task. *)
diff --git a/restructuring/model/task/concept.v b/model/task/concept.v
similarity index 98%
rename from restructuring/model/task/concept.v
rename to model/task/concept.v
index db9044e79..c9cf36960 100644
--- a/restructuring/model/task/concept.v
+++ b/model/task/concept.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssrbool.
-Require Export rt.restructuring.behavior.all.
+Require Export rt.behavior.all.
(** * Task Type *)
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/floating_nonpreemptive.v
rename to model/task/preemption/floating_nonpreemptive.v
index bd65347ee..62d93a0d3 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Import rt.model.preemption.limited_preemptive.
+Require Export rt.model.task.preemption.parameters.
(** * Task Model with Floating Non-Preemptive Regions *)
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/model/task/preemption/fully_nonpreemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/fully_nonpreemptive.v
rename to model/task/preemption/fully_nonpreemptive.v
index 707c2e990..9da4626eb 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/model/task/preemption/fully_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.model.task.preemption.parameters.
(** * Fully Non-Preemptive Task Model *)
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v
similarity index 95%
rename from restructuring/model/task/preemption/fully_preemptive.v
rename to model/task/preemption/fully_preemptive.v
index 6a4faa33a..7cff6fbba 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/model/task/preemption/fully_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
+Require Export rt.model.task.preemption.parameters.
(** * Fully Preemptive Task Model *)
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
similarity index 97%
rename from restructuring/model/task/preemption/limited_preemptive.v
rename to model/task/preemption/limited_preemptive.v
index c91d4f216..685d09357 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.limited_preemptive.
+Require Export rt.model.task.preemption.parameters.
+Require Import rt.model.preemption.limited_preemptive.
(** * Limited-Preemptive Task Model *)
diff --git a/restructuring/model/task/preemption/parameters.v b/model/task/preemption/parameters.v
similarity index 98%
rename from restructuring/model/task/preemption/parameters.v
rename to model/task/preemption/parameters.v
index 151a83873..e5092055f 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/model/task/preemption/parameters.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.preemption.parameter.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.preemption.parameter.
+Require Export rt.model.task.concept.
(** * Task Preemption Model *)
diff --git a/restructuring/model/task/sequentiality.v b/model/task/sequentiality.v
similarity index 95%
rename from restructuring/model/task/sequentiality.v
rename to model/task/sequentiality.v
index 8afbffb46..b6819e434 100644
--- a/restructuring/model/task/sequentiality.v
+++ b/model/task/sequentiality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.task.concept.
(** In this module, we give a precise definition of the common notion of
"sequential tasks", which is commonly understood to mean that the jobs of a
diff --git a/restructuring/model/task/suspension/dynamic.v b/model/task/suspension/dynamic.v
similarity index 91%
rename from restructuring/model/task/suspension/dynamic.v
rename to model/task/suspension/dynamic.v
index 44d6c5a58..31e1dbfda 100644
--- a/restructuring/model/task/suspension/dynamic.v
+++ b/model/task/suspension/dynamic.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.readiness.suspension.
-Require Export rt.restructuring.model.task.concept.
+Require Export rt.model.readiness.suspension.
+Require Export rt.model.task.concept.
(** * Task Parameter for the Dynamic Self-Suspension Model *)
diff --git a/restructuring/README.md b/restructuring/README.md
deleted file mode 100644
index 0d89a0d0f..000000000
--- a/restructuring/README.md
+++ /dev/null
@@ -1,17 +0,0 @@
-# Restructed Prosa
-
-This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa are changed to comply with the “new styleâ€, they are placed here.
-
-The following discussion is going to move to the top-level README file when the `restructuring` prefix is dropped.
-
-## Structure
-
-There are four main parts of Prosa.
-
-The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
-
-The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module may contain multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.) and higher-level results can pick-and-choose whatever definitions are appropriate.
-
-The `analysis` namespace collects all definitions and proofs of **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Most importantly, all high-level analysis results and virtually all proofs are located here.
-
-In future work, there will also (again) be an `implementation` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
diff --git a/restructuring/analysis/facts/behavior/all.v b/restructuring/analysis/facts/behavior/all.v
deleted file mode 100644
index dbd7016f9..000000000
--- a/restructuring/analysis/facts/behavior/all.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Export rt.restructuring.analysis.facts.behavior.service.
-Require Export rt.restructuring.analysis.facts.behavior.service_of_jobs.
-Require Export rt.restructuring.analysis.facts.behavior.completion.
-Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
-Require Export rt.restructuring.analysis.facts.behavior.sequential.
-Require Export rt.restructuring.analysis.facts.behavior.arrivals.
-Require Export rt.restructuring.analysis.facts.behavior.deadlines.
-Require Export rt.restructuring.analysis.facts.behavior.workload.
diff --git a/restructuring/behavior/all.v b/restructuring/behavior/all.v
deleted file mode 100644
index f12642cbe..000000000
--- a/restructuring/behavior/all.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Export rt.restructuring.behavior.time.
-Require Export rt.restructuring.behavior.job.
-Require Export rt.restructuring.behavior.arrival_sequence.
-Require Export rt.restructuring.behavior.schedule.
-Require Export rt.restructuring.behavior.service.
-Require Export rt.restructuring.behavior.ready.
diff --git a/restructuring/results/edf/optimality.v b/results/edf/optimality.v
similarity index 95%
rename from restructuring/results/edf/optimality.v
rename to results/edf/optimality.v
index 44e7f6836..8158da072 100644
--- a/restructuring/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.facts.transform.edf_opt.
+Require Export rt.analysis.facts.transform.edf_opt.
(** This file contains the theorem that states the famous EDF
optimality result: if there is any way to meet all deadlines
@@ -6,10 +6,10 @@ Require Export rt.restructuring.analysis.facts.transform.edf_opt.
schedule in which all deadlines are met. *)
(** The following results assume ideal uniprocessor schedules... *)
-Require rt.restructuring.model.processor.ideal.
+Require rt.model.processor.ideal.
(** ... and the basic (i.e., Liu & Layland) readiness model under which any
pending job is ready. *)
-Require rt.restructuring.model.readiness.basic.
+Require rt.model.readiness.basic.
Section Optimality.
(** For any given type of jobs... *)
diff --git a/restructuring/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
similarity index 97%
rename from restructuring/results/edf/rta/bounded_nps.v
rename to results/edf/rta/bounded_nps.v
index 96e0dd951..85cf2103e 100644
--- a/restructuring/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.facts.priority_inversion.
-Require Export rt.restructuring.results.edf.rta.bounded_pi.
-Require Export rt.restructuring.analysis.facts.rbf.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.analysis.facts.priority_inversion.
+Require Export rt.results.edf.rta.bounded_pi.
+Require Export rt.analysis.facts.rbf.
+Require Import rt.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * RTA for EDF-schedulers with Bounded Non-Preemptive Segments *)
diff --git a/restructuring/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
similarity index 98%
rename from restructuring/results/edf/rta/bounded_pi.v
rename to results/edf/rta/bounded_pi.v
index f8cbcdcae..dc900393d 100644
--- a/restructuring/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,18 +1,18 @@
-Require Export rt.restructuring.analysis.facts.edf.
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.priority_inversion.
-Require Export rt.restructuring.analysis.facts.carry_in.
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.task.absolute_deadline.
-Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
+Require Export rt.analysis.facts.edf.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.priority_inversion.
+Require Export rt.analysis.facts.carry_in.
+Require Export rt.analysis.concepts.schedulability.
+Require Import rt.model.priority.edf.
+Require Import rt.model.task.absolute_deadline.
+Require Import rt.analysis.abstract.ideal_jlfp_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
diff --git a/restructuring/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/floating_nonpreemptive.v
rename to results/edf/rta/floating_nonpreemptive.v
index a7f1ebd94..51949915c 100644
--- a/restructuring/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.floating.
+Require Import rt.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
(** * RTA for Model with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
diff --git a/restructuring/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/fully_nonpreemptive.v
rename to results/edf/rta/fully_nonpreemptive.v
index bd170fec0..4d8311764 100644
--- a/restructuring/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+Require Import rt.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the fully non-preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
(** * RTA for Fully Non-Preemptive FP Model *)
(** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
diff --git a/restructuring/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
similarity index 93%
rename from restructuring/results/edf/rta/fully_preemptive.v
rename to results/edf/rta/fully_preemptive.v
index ad7f4121a..2a875b431 100644
--- a/restructuring/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,17 +1,17 @@
-Require Import rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
-Require Import rt.restructuring.model.priority.edf.
+Require Import rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.preemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.preemptive.
+Require Import rt.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the fully preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
(** * RTA for Fully Preemptive EDF Model *)
(** In this section we prove the RTA theorem for the fully preemptive EDF model *)
diff --git a/restructuring/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
similarity index 94%
rename from restructuring/results/edf/rta/limited_preemptive.v
rename to results/edf/rta/limited_preemptive.v
index 133b828e2..eccb3e98c 100644
--- a/restructuring/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,17 +1,17 @@
-Require Export rt.restructuring.results.edf.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
-Require Import rt.restructuring.model.priority.edf.
+Require Export rt.results.edf.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.limited.
+Require Import rt.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the task model with fixed preemption points. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
(** * RTA for EDF-schedulers with Fixed Preemption Points *)
(** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
diff --git a/restructuring/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
similarity index 96%
rename from restructuring/results/fixed_priority/rta/bounded_nps.v
rename to results/fixed_priority/rta/bounded_nps.v
index 58e4da3ee..418d5f35c 100644
--- a/restructuring/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,14 +1,14 @@
-Require Export rt.restructuring.analysis.concepts.schedulability.
-Require Export rt.restructuring.analysis.concepts.request_bound_function.
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_pi.
-Require Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.analysis.concepts.schedulability.
+Require Export rt.analysis.concepts.request_bound_function.
+Require Export rt.results.fixed_priority.rta.bounded_pi.
+Require Export rt.analysis.facts.priority_inversion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
diff --git a/restructuring/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
similarity index 98%
rename from restructuring/results/fixed_priority/rta/bounded_pi.v
rename to results/fixed_priority/rta/bounded_pi.v
index 184a79486..5546a98a6 100644
--- a/restructuring/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -1,13 +1,13 @@
-Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.busy_interval.
-Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
+Require Export rt.model.schedule.priority_driven.
+Require Export rt.analysis.facts.busy_interval.
+Require Import rt.analysis.abstract.ideal_jlfp_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
(** In this module we instantiate the Abstract Response-Time analysis
diff --git a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
similarity index 93%
rename from restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
rename to results/fixed_priority/rta/floating_nonpreemptive.v
index 4bb73c0f0..1094dbe78 100644
--- a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.floating.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.floating_nonpreemptive.
(** * RTA for Model with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating
diff --git a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
similarity index 93%
rename from restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
rename to results/fixed_priority/rta/fully_nonpreemptive.v
index 0cf5969b4..e1eb3fcd3 100644
--- a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the fully non-preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+Require Import rt.model.task.preemption.fully_nonpreemptive.
(** * RTA for Fully Non-Preemptive FP Model *)
(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
diff --git a/restructuring/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
similarity index 92%
rename from restructuring/results/fixed_priority/rta/fully_preemptive.v
rename to results/fixed_priority/rta/fully_preemptive.v
index 9195c46ee..c216f3d56 100644
--- a/restructuring/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.task.preemptive.
+Require Export rt.analysis.facts.preemption.rtc_threshold.preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the fully preemptive task model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+Require Import rt.model.task.preemption.fully_preemptive.
(** * RTA for Fully Preemptive FP Model *)
(** In this module we prove the RTA theorem for fully preemptive FP model. *)
diff --git a/restructuring/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
similarity index 94%
rename from restructuring/results/fixed_priority/rta/limited_preemptive.v
rename to results/fixed_priority/rta/limited_preemptive.v
index 19fa54b29..360c097b5 100644
--- a/restructuring/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,16 +1,16 @@
-Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
-Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
+Require Export rt.results.fixed_priority.rta.bounded_nps.
+Require Export rt.analysis.facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
+Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.model.readiness.basic.
(** Throughout this file, we assume the task model with fixed preemption points. *)
-Require Import rt.restructuring.model.preemption.limited_preemptive.
-Require Import rt.restructuring.model.task.preemption.limited_preemptive.
+Require Import rt.model.preemption.limited_preemptive.
+Require Import rt.model.task.preemption.limited_preemptive.
(** * RTA for FP-schedulers with Fixed Preemption Points *)
--
GitLab