From 3b9b6f20bebcc7c95f624d6b5d227e64f8570c67 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 20 Dec 2019 20:31:52 +0100
Subject: [PATCH] Add facts.busy_interval

---
 analysis/facts/{ => busy_interval}/busy_interval.v      | 0
 analysis/facts/{ => busy_interval}/carry_in.v           | 3 +--
 analysis/facts/{ => busy_interval}/priority_inversion.v | 2 +-
 results/edf/rta/bounded_nps.v                           | 2 --
 results/edf/rta/bounded_pi.v                            | 4 ++--
 results/fixed_priority/rta/bounded_nps.v                | 2 +-
 results/fixed_priority/rta/bounded_pi.v                 | 3 +--
 7 files changed, 6 insertions(+), 10 deletions(-)
 rename analysis/facts/{ => busy_interval}/busy_interval.v (100%)
 rename analysis/facts/{ => busy_interval}/carry_in.v (99%)
 rename analysis/facts/{ => busy_interval}/priority_inversion.v (99%)

diff --git a/analysis/facts/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
similarity index 100%
rename from analysis/facts/busy_interval.v
rename to analysis/facts/busy_interval/busy_interval.v
diff --git a/analysis/facts/carry_in.v b/analysis/facts/busy_interval/carry_in.v
similarity index 99%
rename from analysis/facts/carry_in.v
rename to analysis/facts/busy_interval/carry_in.v
index 0a4132d84..2f981a04a 100644
--- a/analysis/facts/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -1,7 +1,6 @@
 Require Export prosa.analysis.facts.workload.
 Require Export prosa.analysis.definitions.carry_in.
-Require Export prosa.analysis.facts.busy_interval.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/analysis/facts/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
similarity index 99%
rename from analysis/facts/priority_inversion.v
rename to analysis/facts/busy_interval/priority_inversion.v
index 767c3d178..1e57c0fa7 100644
--- a/analysis/facts/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -4,7 +4,7 @@ Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.busy_interval.
 Require Export prosa.analysis.facts.model.ideal_schedule.
-Require Export prosa.analysis.facts.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index dbe22f2fc..b0f270970 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -1,9 +1,7 @@
 Require Import prosa.model.priority.edf.
 Require Export prosa.analysis.facts.rbf.
 Require Export prosa.analysis.facts.sequential.
-Require Export prosa.analysis.facts.priority_inversion.
 Require Export prosa.results.edf.rta.bounded_pi.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 55a3ae8db..b50dec910 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,7 +1,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.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.busy_interval.carry_in.
 Require Export prosa.analysis.definitions.schedulability.
 Require Import prosa.model.priority.edf.
 Require Import prosa.model.task.absolute_deadline.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 4b4dccf2d..3c07f6e7f 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -1,7 +1,7 @@
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.definitions.request_bound_function.
 Require Export prosa.analysis.facts.sequential.
-Require Export prosa.analysis.facts.priority_inversion.
+Require Export prosa.analysis.facts.busy_interval.priority_inversion.
 Require Export prosa.results.fixed_priority.rta.bounded_pi.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index a8beb06bc..5f9f41962 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -1,7 +1,6 @@
 Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 Require Import prosa.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 prosa.model.processor.ideal.
-- 
GitLab