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.

(* In this file, we take any predicate that defines whether a job
   is suspended at time t and build a table of suspension durations
   that is valid up to time t. *)
Module SuspensionTableConstruction.

  Import ScheduleWithSuspensions Suspension.

  Section BuildingSuspensionTable.

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

    (* Consider any job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.

    (* ...and any schedule of this arrival sequence... *)
    Variable sched: schedule Job.

    (* ...in which jobs must arrive to execute. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    (* Recall the instant following the last execution of a job, which
       indicates the start of the latest suspension interval. *)
    Let start_of_latest_suspension :=
      time_after_last_execution job_arrival sched.

    (* For simplicity, let's also define some local names. *)
    Let job_completed_by := completed_by job_cost sched.

    (* We are going to construct a suspension table that is valid up to time t_max. *)
    Variable t_max: time.

    (* First, consider any predicate that indicates whether a job is suspended at time t. *)
    Variable job_suspended_at: Job → time → bool.

    (* Assume that this predicate only holds for jobs that have arrived... *)
    Hypothesis H_arrived:
      ∀ j t,
        t < t_max →
        job_suspended_at j t →
        has_arrived job_arrival j t.

    (* ...and that have not yet completed. *)
    Hypothesis H_not_completed:
      ∀ j t,
        t < t_max →
        job_suspended_at j t →
        ~~ job_completed_by j t.

    (* Assume that this predicate divides the timeline into continuous
       suspension intervals, for any given amount of received service. *)
    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.

    (* Then, we can construct a suspension table for the given suspension
       predicate as follows. *)
    Definition build_suspension_duration (j: Job) (s: time) :=
        \sum_(0 ≤ t < t_max | service sched j t == s) job_suspended_at j t.

    (* In order to prove that the suspension table matches the given predicate,
       let's first prove some helper lemmas. *)
    Section HelperLemmas.

      (* First, we show that for any job j suspended at time t, the cumulative suspension
         time before the beginning of the suspension is zero. *)
      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.

      (* Next, we prove that after time t_max, no job suspends according to the table. *)
      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.

    (* Using the lemmas above, we prove that up to time t_max, the constructed suspension
       table matches the given suspension predicate. *)
    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.