Library prosa.classic.model.schedule.uni.susp.valid_schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.susp.schedule
               prosa.classic.model.schedule.uni.susp.platform.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ValidSuspensionAwareSchedule.

  Import ScheduleWithSuspensions Suspension Priority PlatformWithSuspensions.

  Section DefiningValidSchedule.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.

    Variable higher_eq_priority: JLDP_policy Job.

    Variable job_suspension_duration: job_suspension Job.

    Variable job_cost: Job → time.

    Variable sched_susp: schedule Job.


    Let H1_jobs_come_from_arrival_sequence := jobs_come_from_arrival_sequence sched_susp arr_seq.

    Let H2_jobs_must_arrive_to_execute := jobs_must_arrive_to_execute job_arrival sched_susp.

    Let H3_completed_jobs_dont_execute := completed_jobs_dont_execute job_cost sched_susp.

    Let H4_work_conserving :=
      work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.

    Let H5_respects_priority :=
      respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
                           sched_susp higher_eq_priority.

    Let H6_respects_self_suspensions :=
      respects_self_suspensions job_arrival job_cost job_suspension_duration sched_susp.

    Definition valid_suspension_aware_schedule :=
      H1_jobs_come_from_arrival_sequence ∧
      H2_jobs_must_arrive_to_execute ∧
      H3_completed_jobs_dont_execute ∧
      H4_work_conserving ∧
      H5_respects_priority ∧
      H6_respects_self_suspensions.

  End DefiningValidSchedule.

End ValidSuspensionAwareSchedule.