From 80bd79d56a5af9462481b8b38d763039925be15d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 30 Aug 2019 15:54:46 +0200
Subject: [PATCH] move basic facts out of behavior/ folder

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.
---
 restructuring/analysis/basic_facts/all.v                    | 6 ++++++
 .../{behavior/facts => analysis/basic_facts}/arrivals.v     | 0
 .../{behavior/facts => analysis/basic_facts}/completion.v   | 2 +-
 .../{behavior/facts => analysis/basic_facts}/deadlines.v    | 5 +++--
 .../facts => analysis/basic_facts}/ideal_schedule.v         | 0
 .../{behavior/facts => analysis/basic_facts}/sequential.v   | 0
 .../{behavior/facts => analysis/basic_facts}/service.v      | 0
 restructuring/analysis/schedulability.v                     | 3 ++-
 restructuring/analysis/transform/facts/edf_opt.v            | 2 +-
 restructuring/analysis/transform/facts/replace_at.v         | 2 +-
 restructuring/analysis/transform/facts/swaps.v              | 2 +-
 restructuring/analysis/transform/prefix.v                   | 3 ++-
 restructuring/analysis/transform/swap.v                     | 2 +-
 restructuring/behavior/facts/all.v                          | 6 ------
 restructuring/model/readiness/basic.v                       | 2 +-
 restructuring/model/schedule/task_schedule.v                | 5 +++--
 16 files changed, 22 insertions(+), 18 deletions(-)
 create mode 100644 restructuring/analysis/basic_facts/all.v
 rename restructuring/{behavior/facts => analysis/basic_facts}/arrivals.v (100%)
 rename restructuring/{behavior/facts => analysis/basic_facts}/completion.v (99%)
 rename restructuring/{behavior/facts => analysis/basic_facts}/deadlines.v (94%)
 rename restructuring/{behavior/facts => analysis/basic_facts}/ideal_schedule.v (100%)
 rename restructuring/{behavior/facts => analysis/basic_facts}/sequential.v (100%)
 rename restructuring/{behavior/facts => analysis/basic_facts}/service.v (100%)
 delete mode 100644 restructuring/behavior/facts/all.v

diff --git a/restructuring/analysis/basic_facts/all.v b/restructuring/analysis/basic_facts/all.v
new file mode 100644
index 000000000..96e03e871
--- /dev/null
+++ b/restructuring/analysis/basic_facts/all.v
@@ -0,0 +1,6 @@
+Require Export rt.restructuring.analysis.basic_facts.service.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.basic_facts.sequential.
+Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.deadlines.
diff --git a/restructuring/behavior/facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
similarity index 100%
rename from restructuring/behavior/facts/arrivals.v
rename to restructuring/analysis/basic_facts/arrivals.v
diff --git a/restructuring/behavior/facts/completion.v b/restructuring/analysis/basic_facts/completion.v
similarity index 99%
rename from restructuring/behavior/facts/completion.v
rename to restructuring/analysis/basic_facts/completion.v
index 7743faeb4..582c4d829 100644
--- a/restructuring/behavior/facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule.
-From rt.restructuring.behavior.facts Require Export service.
+From rt.restructuring.analysis.basic_facts Require Export service.
 
 From rt.util Require Import nat.
 
diff --git a/restructuring/behavior/facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
similarity index 94%
rename from restructuring/behavior/facts/deadlines.v
rename to restructuring/analysis/basic_facts/deadlines.v
index 703f5529c..1196bd3e3 100644
--- a/restructuring/behavior/facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,4 +1,5 @@
-From rt.restructuring.behavior Require Export schedule facts.service facts.completion.
+From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.analysis.basic_facts Require Export service completion.
 
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
@@ -69,4 +70,4 @@ Section DeadlineFacts.
 
   End EqualProgress.
 
-End DeadlineFacts.
\ No newline at end of file
+End DeadlineFacts.
diff --git a/restructuring/behavior/facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
similarity index 100%
rename from restructuring/behavior/facts/ideal_schedule.v
rename to restructuring/analysis/basic_facts/ideal_schedule.v
diff --git a/restructuring/behavior/facts/sequential.v b/restructuring/analysis/basic_facts/sequential.v
similarity index 100%
rename from restructuring/behavior/facts/sequential.v
rename to restructuring/analysis/basic_facts/sequential.v
diff --git a/restructuring/behavior/facts/service.v b/restructuring/analysis/basic_facts/service.v
similarity index 100%
rename from restructuring/behavior/facts/service.v
rename to restructuring/analysis/basic_facts/service.v
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 5bb6e8b72..7226af674 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,5 +1,6 @@
-From rt.restructuring.behavior Require Export schedule facts.completion.
+From rt.restructuring.behavior Require Export schedule.
 From rt.restructuring.model Require Export task.
+From rt.restructuring.analysis.basic_facts Require Export completion.
 From rt.util Require Export seqset.
 
 Section Task.
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index 28cc99010..c298caee9 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export facts.all.
+From rt.restructuring.analysis Require Export basic_facts.all.
 From rt.restructuring.model Require Export schedule.edf.
 From rt.restructuring.analysis Require Export schedulability transform.edf_trans transform.facts.swaps.
 
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/transform/facts/replace_at.v
index 4c16fe2fa..62c52ec27 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/transform/facts/replace_at.v
@@ -1,5 +1,5 @@
 From rt.restructuring.analysis.transform Require Export swap.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
 From rt.util Require Import nat.
 
 (** In this file, we make a few simple observations about schedules with
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index 1535a6a9a..5395156ae 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -1,5 +1,5 @@
 From rt.restructuring.analysis.transform Require Export swap facts.replace_at.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
 From rt.util Require Import nat.
 
 (** In this file, we establish invariants about schedules in which two
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index e67da6b8f..2187ebe2a 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Import schedule facts.all.
+From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.analysis Require Import basic_facts.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/restructuring/analysis/transform/swap.v
index 1cd62f9e1..6f32fc7d3 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule job.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import 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/facts/all.v b/restructuring/behavior/facts/all.v
deleted file mode 100644
index ef6afe004..000000000
--- a/restructuring/behavior/facts/all.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Export rt.restructuring.behavior.facts.service.
-Require Export rt.restructuring.behavior.facts.completion.
-Require Export rt.restructuring.behavior.facts.ideal_schedule.
-Require Export rt.restructuring.behavior.facts.sequential.
-Require Export rt.restructuring.behavior.facts.arrivals.
-Require Export rt.restructuring.behavior.facts.deadlines.
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index d9fd6d860..2852f526a 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule.
-From rt.restructuring.behavior.facts Require Import completion.
+From rt.restructuring.analysis.basic_facts Require Import completion.
 
 (* We define the readiness indicator function for the classic Liu & Layland
    model without jitter and no self-suspensions, where jobs are always
diff --git a/restructuring/model/schedule/task_schedule.v b/restructuring/model/schedule/task_schedule.v
index 97c6a111e..0a5ef66ec 100644
--- a/restructuring/model/schedule/task_schedule.v
+++ b/restructuring/model/schedule/task_schedule.v
@@ -1,5 +1,6 @@
 From rt.restructuring.model Require Import task.
-From rt.restructuring.behavior Require Import schedule ideal_schedule.
+From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -49,4 +50,4 @@ Section ScheduleOfTask.
 
   End TaskProperties.
 
-End ScheduleOfTask. 
\ No newline at end of file
+End ScheduleOfTask. 
-- 
GitLab