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

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

Module SuspensionTableConstruction.

  Import ScheduleWithSuspensions Suspension.

  Section BuildingSuspensionTable.

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

    Variable arr_seq: arrival_sequence Job.

    Variable sched: schedule Job.

    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    Let start_of_latest_suspension :=
      time_after_last_execution job_arrival sched.

    Let job_completed_by := completed_by job_cost sched.

    Variable t_max: time.

    Variable job_suspended_at: Job → time → bool.

    Hypothesis H_arrived:
      ∀ j t,
        t < t_max →
        job_suspended_at j t →
        has_arrived job_arrival j t.

    Hypothesis H_not_completed:
      ∀ j t,
        t < t_max →
        job_suspended_at j t →
        ~~ job_completed_by j t.

    Hypothesis H_continuous_suspension:
      ∀ j t t_susp,
        t < t_max →
        job_suspended_at j t →
        start_of_latest_suspension j t ≤ t_susp < t →
        job_suspended_at j t_susp.

    Definition build_suspension_duration (j: Job) (s: time) :=
        \sum_(0 ≤ t < t_max | service sched j t == s) job_suspended_at j t.

    Section HelperLemmas.

      Lemma not_suspended_before_suspension_start:
        ∀ j t,
          t < t_max →
          job_suspended_at j t →
          let susp_start := start_of_latest_suspension j t in
          let S := service sched j in
            \sum_(0 ≤ i < susp_start | S i == S susp_start) job_suspended_at j i = 0.

      Lemma suspension_duration_no_suspension_after_t_max:
        ∀ j t,
          has_arrived job_arrival j t →
          t_max ≤ t →
          ~~ suspended_at job_arrival job_cost build_suspension_duration sched j t.

    End HelperLemmas.

    Open Scope fun_scope.

    Lemma suspension_duration_matches_predicate_up_to_t_max:
      ∀ j t,
        t < t_max →
        job_suspended_at j t =
        suspended_at job_arrival job_cost build_suspension_duration sched j t.

  End BuildingSuspensionTable.

End SuspensionTableConstruction.