From 46e8bd905c02a4ca185f403e27238af02884b8b8 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 15 Oct 2019 13:36:08 +0200
Subject: [PATCH] Restructuring the model folder

---
 restructuring/analysis/arrival/rbf.v                       | 3 ++-
 restructuring/analysis/arrival/workload_bound.v            | 5 +++--
 restructuring/analysis/basic_facts/task_arrivals.v         | 2 +-
 restructuring/model/{ => aggregate}/service_of_jobs.v      | 0
 restructuring/model/{arrival => aggregate}/task_arrivals.v | 0
 restructuring/model/{ => aggregate}/workload.v             | 0
 restructuring/model/job.v                                  | 4 ++--
 7 files changed, 8 insertions(+), 6 deletions(-)
 rename restructuring/model/{ => aggregate}/service_of_jobs.v (100%)
 rename restructuring/model/{arrival => aggregate}/task_arrivals.v (100%)
 rename restructuring/model/{ => aggregate}/workload.v (100%)

diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index 1bf9b7c51..cb9b77140 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,7 +1,8 @@
 From rt.util Require Import all.
 From rt.restructuring.behavior Require Import schedule.
 From rt.restructuring.model Require Import job task.
-From rt.restructuring.model.arrival Require Import task_arrivals arrival_curves.
+From rt.restructuring.model.aggregate Require Import task_arrivals.
+From rt.restructuring.model.arrival Require Import arrival_curves.
 From rt.restructuring.analysis Require Import arrival.workload_bound.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index f37679204..91688c0b4 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,7 +1,8 @@
 From rt.util Require Import sum.
 From rt.restructuring.behavior Require Import schedule.
-From rt.restructuring.model Require Import task schedule.priority_based.priorities arrival.arrival_curves.
-From rt.restructuring.model.arrival Require Import task_arrivals arrival_curves.
+From rt.restructuring.model Require Import task schedule.priority_based.priorities.
+From rt.restructuring.model.aggregate Require Import task_arrivals.
+From rt.restructuring.model.arrival Require Import arrival_curves.
 From rt.restructuring.analysis Require Import
      workload ideal_schedule basic_facts.arrivals.
 
diff --git a/restructuring/analysis/basic_facts/task_arrivals.v b/restructuring/analysis/basic_facts/task_arrivals.v
index ac264c7d6..381fc6aa0 100644
--- a/restructuring/analysis/basic_facts/task_arrivals.v
+++ b/restructuring/analysis/basic_facts/task_arrivals.v
@@ -1,4 +1,4 @@
-From rt.restructuring.model Require Export arrival.task_arrivals.
+From rt.restructuring.model.aggregate Require Export task_arrivals.
 
 (* In this file we provide basic properties related to tasks on arrival sequences. *)
 Section TaskArrivals.
diff --git a/restructuring/model/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
similarity index 100%
rename from restructuring/model/service_of_jobs.v
rename to restructuring/model/aggregate/service_of_jobs.v
diff --git a/restructuring/model/arrival/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
similarity index 100%
rename from restructuring/model/arrival/task_arrivals.v
rename to restructuring/model/aggregate/task_arrivals.v
diff --git a/restructuring/model/workload.v b/restructuring/model/aggregate/workload.v
similarity index 100%
rename from restructuring/model/workload.v
rename to restructuring/model/aggregate/workload.v
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index 0e017838e..40ddc1a91 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -2,7 +2,7 @@ From rt.restructuring.behavior Require Export time job.
 From mathcomp Require Export eqtype ssrnat.
 
 (* In this section, we introduce properties of a job. *)
-Section PropertesOfJob.
+Section PropertiesOfJob.
 
   (* Assume that job costs are known. *)
   Context {Job : JobType}.
@@ -14,4 +14,4 @@ Section PropertesOfJob.
   (* The job cost must be positive. *)
   Definition job_cost_positive := job_cost j > 0.
 
-End PropertesOfJob. 
\ No newline at end of file
+End PropertiesOfJob. 
\ No newline at end of file
-- 
GitLab