Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.

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

Module AbstractRTADefinitions.

  Import Job UniprocessorSchedule.

  Section Definitions.

    Context {Task: eqType}.

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

    Variable arr_seq: arrival_sequence Job.

    Variable sched: schedule Job.

    Variable tsk: Task.

    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.

    Let job_pending_earlier_and_at := pending_earlier_and_at job_arrival job_cost sched.

    Variable interference: Job → time → bool.

    Variable interfering_workload: Job → time → time.

    Definition cumul_interference j t1 t2 := \sum_(t1 ≤ t < t2) interference j t.
    Definition cumul_interfering_workload j t1 t2 := \sum_(t1 ≤ t < t2) interfering_workload j t.

    Section BusyInterval.

      Definition quiet_time (j: Job) (t: time) :=
        cumul_interference j 0 t = cumul_interfering_workload j 0 t ∧
        ~~ job_pending_earlier_and_at j t.

      Definition busy_interval_prefix (j: Job) (t1 t2: time) :=
        t1 ≤ job_arrival j < t2 ∧
        quiet_time j t1 ∧
        (∀ t, t1 < t < t2 → ¬ quiet_time j t).

      Definition busy_interval (j: Job) (t1 t2: time) :=
        busy_interval_prefix j t1 t2 ∧
        quiet_time j t2.

      Lemma busy_interval_is_unique:
        ∀ j t1 t2 t1' t2',
          busy_interval j t1 t2 →
          busy_interval j t1' t2' →
          t1 = t1' ∧ t2 = t2'.

    End BusyInterval.

    Section BusyIntervalProperties.

      Definition work_conserving :=
        ∀ j t1 t2 t,
          arrives_in arr_seq j →
          job_task j = tsk →
          job_cost j > 0 →
          busy_interval j t1 t2 →
          t1 ≤ t < t2 →
          ¬ interference j t ↔ job_scheduled_at j t.

      Definition busy_intervals_are_bounded_by L :=
        ∀ j,
          arrives_in arr_seq j →
          job_task j = tsk →
          job_cost j > 0 →
          ∃ t1 t2,
            t1 ≤ job_arrival j < t2 ∧
            t2 ≤ t1 + L ∧
            busy_interval j t1 t2.

      Definition job_interference_is_bounded_by (interference_bound_function: Task → time → time → time) :=
        ∀ t1 t2 delta j,
          busy_interval j t1 t2 →
          t1 + delta < t2 →
          arrives_in arr_seq j →
          job_task j = tsk →
          ~~ job_completed_by j (t1 + delta) →
          let offset := job_arrival j - t1 in
          cumul_interference j t1 (t1 + delta) ≤ interference_bound_function tsk offset delta .

    End BusyIntervalProperties.

  End Definitions.

End AbstractRTADefinitions.