Renaming in schedule.v

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.