From fcf52c78c50dd93994652b18729f430f2adc61bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 6 Nov 2019 18:08:08 +0100
Subject: [PATCH] update explanation of new Prosa's structure

---
 restructuring/README.md | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/restructuring/README.md b/restructuring/README.md
index 53d871b6d..0d89a0d0f 100644
--- a/restructuring/README.md
+++ b/restructuring/README.md
@@ -1,11 +1,17 @@
-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.
+# Restructed Prosa
 
-The behavior directory collects all definitions and basic properties of system behavior (i.e., trace-based semantics). Changes here are sensitive since this is the part of the library that everyone is going to use, so changes here should be discussed early.
+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 model directory collects all definitions and basic properties of system models (e.g., sporadic tasks, arrival curves, scheduling policies etc.). One should port and validate a new system model before the corresponding analysis.
+The following discussion is going to move to the top-level README file when the `restructuring` prefix is dropped.
 
-The analysis directory collects all definitions of system properties (e.g., schedulability, response time etc.), analysis results and proofs. The stucture of this directory is not clear yet.
+## Structure 
 
-# Remarks
+There are four main parts of Prosa. 
 
-We have chosen and applied some renaming rules for sections and definitions, cf. arrival_sequence.v and sporadic.v. Basically, we try to consistenly use `Valid*` , `*Properties` for section names about a concept `*` and `respects_*`, `valid_*` for definitions about a system model `*`.
+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.
-- 
GitLab