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

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

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

Module ValidJitterAwareSchedule.

  Import UniprocessorScheduleWithJitter Priority Platform.

  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_cost: Job → time.
    Variable job_jitter: Job → time.

    Variable sched: schedule Job.


    Let H1_jobs_come_from_arrival_sequence := jobs_come_from_arrival_sequence sched arr_seq.

    Let H2_jobs_execute_after_jitter := jobs_execute_after_jitter job_arrival job_jitter sched.

    Let H3_completed_jobs_dont_execute := completed_jobs_dont_execute job_cost sched.

    Let H4_work_conserving := work_conserving job_arrival job_cost job_jitter arr_seq sched.

    Let H5_respects_priority :=
      respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.

    Definition valid_jitter_aware_schedule :=
      H1_jobs_come_from_arrival_sequence ∧
      H2_jobs_execute_after_jitter ∧
      H3_completed_jobs_dont_execute ∧
      H4_work_conserving ∧
      H5_respects_priority.

  End DefiningValidSchedule.

End ValidJitterAwareSchedule.