From d72908b6cf35f00d22f9e917d04fe6ad292559fd Mon Sep 17 00:00:00 2001 From: Maxime Lesourd Date: Fri, 24 May 2019 15:16:36 +0200 Subject: [PATCH] Renaming in schedule.v --- behavior/schedule/schedule.v | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/behavior/schedule/schedule.v b/behavior/schedule/schedule.v index e4fd37c..a82aafb 100644 --- a/behavior/schedule/schedule.v +++ b/behavior/schedule/schedule.v @@ -26,7 +26,7 @@ Definition schedule (PState : Type) := instant -> PState. Class JobCost (J : JobType) := job_cost : J -> nat. -Section Service. +Section Schedule. Context {Job : eqType} {PState : Type}. Context `{ProcessorState Job PState}. @@ -71,10 +71,8 @@ Section Service. Definition remaining_cost j t := job_cost j - service j t. - (* In this section, we define properties of valid schedules. *) - Section ValidSchedules. - - Variable (arr_seq : arrival_sequence Job). + (* In this section, we define valid schedules. *) + Section ValidSchedule. (* We define whether jobs come from some arrival sequence... *) Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) := @@ -88,5 +86,13 @@ Section Service. Definition completed_jobs_dont_execute := forall j t, service j t <= job_cost j. - End ValidSchedules. -End Service. + (* We say that the schedule is valid iff + - jobs come from some arrival sequence + - a job can only be scheduled if it has arrived and is not completed yet *) + Definition schedule_is_valid (arr_seq : arrival_sequence Job) := + jobs_come_from_arrival_sequence arr_seq /\ + jobs_must_arrive_to_execute /\ + completed_jobs_dont_execute. + + End ValidSchedule. +End Schedule. -- GitLab