From 4efbd031ac88f1fa2b59d59a20a5db19d4026983 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 17 Sep 2019 15:22:32 +0200
Subject: [PATCH] Polishing base files
---
restructuring/model/job.v | 4 ++--
restructuring/model/processor/platform_properties.v | 6 +++---
restructuring/model/task.v | 9 +++++----
3 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index ba5d58e50..0e017838e 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -9,9 +9,9 @@ Section PropertesOfJob.
Context `{JobCost Job}.
(* Consider an arbitrary job. *)
- Variable j: Job.
+ Variable j : Job.
(* The job cost must be positive. *)
Definition job_cost_positive := job_cost j > 0.
-End PropertesOfJob.
\ No newline at end of file
+End PropertesOfJob.
\ No newline at end of file
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index 1c9a4552c..dedc5544e 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -4,14 +4,14 @@ From rt.restructuring.behavior Require Export schedule.
following properties that a processor model might possess. *)
Section ProcessorModels.
(* Consider any job type and any processor state. *)
- Context {Job: JobType}.
- Context {PState: Type}.
+ Context {Job : JobType}.
+ Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* We say that a processor model provides unit service if no
job ever receives more than one unit of service at any time. *)
Definition unit_service_proc_model :=
- forall j s, service_in j s <= 1.
+ forall (j : Job) (s : PState), service_in j s <= 1.
(* We say that a processor model offers ideal progress if a scheduled job
always receives non-zero service. *)
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index ef934520d..b325e42d6 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,6 +1,5 @@
From mathcomp Require Export ssrbool.
From rt.restructuring.behavior Require Export job.
-
From rt.restructuring.behavior Require Export arrival_sequence.
(* Throughout the library we assume that tasks have decidable equality *)
@@ -32,9 +31,11 @@ Section SameTask.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
- (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1
- is equal to job_task j2. *)
- Definition same_task j1 j2 := job_task j1 == job_task j2.
+ (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1 is equal to job_task j2, ... *)
+ Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.
+
+ (* ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
+ Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
End SameTask.
--
GitLab