Commit 4efbd031 authored by Sergey Bozhko's avatar Sergey Bozhko

Polishing base files

parent 8cfea2c7
......@@ -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
......@@ -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. *)
......
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment