From d1b319e6b779de251ae790510769cda5d08d9465 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 19 Dec 2019 16:12:25 +0100
Subject: [PATCH] merge analysis.concepts and analysis.definitions
In anticipation of future reorganization efforts by Sophie, there's no
point in keeping the two kinds of definitions separate.
---
analysis/abstract/abstract_rta.v | 2 +-
analysis/abstract/ideal_jlfp_rta.v | 2 +-
analysis/{concepts => definitions}/busy_interval.v | 0
analysis/{concepts => definitions}/priority_inversion.v | 2 +-
analysis/{concepts => definitions}/request_bound_function.v | 0
analysis/{concepts => definitions}/schedulability.v | 0
analysis/facts/busy_interval.v | 2 +-
analysis/facts/priority_inversion.v | 2 +-
analysis/facts/rbf.v | 2 +-
analysis/facts/transform/edf_opt.v | 2 +-
results/edf/rta/bounded_pi.v | 2 +-
results/fixed_priority/rta/bounded_nps.v | 4 ++--
12 files changed, 10 insertions(+), 10 deletions(-)
rename analysis/{concepts => definitions}/busy_interval.v (100%)
rename analysis/{concepts => definitions}/priority_inversion.v (98%)
rename analysis/{concepts => definitions}/request_bound_function.v (100%)
rename analysis/{concepts => definitions}/schedulability.v (100%)
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 8eeb79e92..06c0c2428 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.run_to_completion.
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 1a4959e1a..53b778c38 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.priority_inversion.
+Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.abstract.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/analysis/concepts/busy_interval.v b/analysis/definitions/busy_interval.v
similarity index 100%
rename from analysis/concepts/busy_interval.v
rename to analysis/definitions/busy_interval.v
diff --git a/analysis/concepts/priority_inversion.v b/analysis/definitions/priority_inversion.v
similarity index 98%
rename from analysis/concepts/priority_inversion.v
rename to analysis/definitions/priority_inversion.v
index d2397db20..21d933525 100644
--- a/analysis/concepts/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.concepts.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/analysis/concepts/request_bound_function.v b/analysis/definitions/request_bound_function.v
similarity index 100%
rename from analysis/concepts/request_bound_function.v
rename to analysis/definitions/request_bound_function.v
diff --git a/analysis/concepts/schedulability.v b/analysis/definitions/schedulability.v
similarity index 100%
rename from analysis/concepts/schedulability.v
rename to analysis/definitions/schedulability.v
diff --git a/analysis/facts/busy_interval.v b/analysis/facts/busy_interval.v
index 4dfb29e9a..ef2bbbd87 100644
--- a/analysis/facts/busy_interval.v
+++ b/analysis/facts/busy_interval.v
@@ -1,6 +1,6 @@
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.work_conserving.
-Require Export prosa.analysis.concepts.priority_inversion.
+Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/analysis/facts/priority_inversion.v b/analysis/facts/priority_inversion.v
index 84820dd42..fa62b565c 100644
--- a/analysis/facts/priority_inversion.v
+++ b/analysis/facts/priority_inversion.v
@@ -3,7 +3,7 @@ Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.job_properties.
-Require Export prosa.analysis.concepts.busy_interval.
+Require Export prosa.analysis.definitions.busy_interval.
Require Export prosa.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/analysis/facts/rbf.v b/analysis/facts/rbf.v
index 376dcf44b..27fa1e790 100644
--- a/analysis/facts/rbf.v
+++ b/analysis/facts/rbf.v
@@ -1,6 +1,6 @@
Require Export prosa.analysis.facts.behavior.workload.
Require Export prosa.analysis.definitions.job_properties.
-Require Export prosa.analysis.concepts.request_bound_function.
+Require Export prosa.analysis.definitions.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 0ce47a135..56d6e1247 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,6 +1,6 @@
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export prosa.model.schedule.edf.
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.transform.edf_trans.
Require Export prosa.analysis.facts.transform.swaps.
Require Export prosa.analysis.facts.readiness.basic.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index d7295099c..55a3ae8db 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -2,7 +2,7 @@ Require Export prosa.analysis.facts.edf.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.priority_inversion.
Require Export prosa.analysis.facts.carry_in.
-Require Export prosa.analysis.concepts.schedulability.
+Require Export prosa.analysis.definitions.schedulability.
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
Require Import prosa.analysis.abstract.ideal_jlfp_rta.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index bb195bafe..51b583a3a 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,5 +1,5 @@
-Require Export prosa.analysis.concepts.schedulability.
-Require Export prosa.analysis.concepts.request_bound_function.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
Require Export prosa.analysis.facts.priority_inversion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
--
GitLab