Library prosa.classic.model.schedule.uni.end_time

Require Import Arith Nat.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
               prosa.classic.model.arrival.basic.job
               prosa.classic.model.schedule.uni.schedule
               prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.


Module end_time.
  Import UniprocessorSchedule Job ResponseTime.

  Section Task.
    Context {task: eqType}.
    Variable task_cost: task → time.
    Variable task_period: task → time.
    Variable task_deadline: task → time.

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

    Inductive diagnosis_option : Set :=
      | OK : instant → diagnosis_option
      | Failure : instant → diagnosis_option.

    Section Job_end_time_Def.

      Variable sched: schedule Job.

      Variable job:Job.

      Let job_scheduled_at t:= scheduled_at sched job t = true.

      Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
        match c with
        | 0 ⇒ OK t
        | S c'⇒ match wf with
              | 0 ⇒ Failure t
              | S wf'⇒ if scheduled_at sched job t then end_time_option (S t) c' wf'
                            else end_time_option (S t) c wf'
              end
        end.

      Inductive end_time_predicate : instant→ duration→instant→Prop:=
        |C0_: ∀ t, end_time_predicate t 0 t

        |S_C_not_sched: ∀ t c e,
          ¬job_scheduled_at t→
          end_time_predicate (S t) (S c) e→
          end_time_predicate t (S c) e

        |S_C_sched: ∀ t c e,
          job_scheduled_at t→
          end_time_predicate (S t) c e→
          end_time_predicate t (S c) e.

      Definition completes_at (t:instant):=
        end_time_predicate (job_arrival job) (job_cost job) t.

    End Job_end_time_Def.

    Section Lemmas.

      Variable job:Job.

      Variable sched: schedule Job.

      Hypothesis H_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute job_arrival sched.
      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.

      Hypothesis H_valid_job:
      valid_realtime_job job_cost job_deadline job.

      Let job_end_time_function:= end_time_option sched job.

      Let job_end_time_p:= end_time_predicate sched job.

      Let job_completes_at := completes_at sched job.

      Let job_scheduled_at t:= scheduled_at sched job t = true.

      Theorem end_time_function_predicat_equivalence:
        ∀ e wf t c,
          job_end_time_function t c wf = OK e →
          job_end_time_p t c e.

      Theorem end_time_predicat_function_equivalence:
        ∀ t c e ,
          job_end_time_p t c e →
          ∃ wf, job_end_time_function t c wf = OK e.

      Lemma end_time_predicate_not_sched:
        ∀ t c e,
          ~(job_scheduled_at t) →
          end_time_predicate sched job t c.+1 e →
          end_time_predicate sched job t.+1 c.+1 e.

      Lemma end_time_predicate_sched:
        ∀ t c e,
          job_scheduled_at t →
          end_time_predicate sched job t c.+1 e →
          end_time_predicate sched job t.+1 c e.

      Variable job_end: instant.

      Let job_completed_by:=
        completed_by job_cost sched.

      Let job_service_during:=
        service_during sched job.

      Lemma arrival_le_end:
         ∀ t c e, job_end_time_p t c e → t ≤ e.

      Lemma arrival_add_cost_le_end:
        ∀ t c e,
          job_end_time_p t c e →
          t+c≤e.

      Lemma service_eq_cost_at_end_time:
        job_completes_at job_end →
        job_service_during (job_arrival job) job_end = job_cost job.

      Lemma completed_by_end_time:
        job_completes_at job_end →
        job_completed_by job job_end.

      Corollary end_time_positive:
        job_completes_at job_end → job_end > 0.

      Lemma job_uncompletes_at_end_time_sub_1:
        job_completes_at job_end →
        job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.

      Lemma job_uncompleted_before_end_time:
        job_completes_at job_end →
        ∀ t', job_arrival job ≤ t' ∧ t'≤ job_end.-1 →
           job_service_during (job_arrival job) t' < job_cost job.

    End Lemmas.

  End Task.

End end_time.