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

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.suspension
               prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ScheduleWithSuspensions.

  Export UniprocessorSchedule SuspensionIntervals.

  Section Definitions.

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

    Variable next_suspension: job_suspension Job.

    Variable sched: schedule Job.

    Let job_pending_at := pending job_arrival job_cost sched.
    Let job_scheduled_at := scheduled_at sched.
    Let job_suspended_at := suspended_at job_arrival job_cost next_suspension sched.

    Section BackloggedJob.

      Variable j: Job.

      Definition backlogged (t: time) :=
        job_pending_at j t
        && ~~ job_scheduled_at j t
        && ~~ job_suspended_at j t.

    End BackloggedJob.

  End Definitions.

End ScheduleWithSuspensions.