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
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.

    (* instant option, to be used in end_time_option *)
    Inductive diagnosis_option : Set :=
      | OK : instant diagnosis_option
      | Failure : instant diagnosis_option.

    Section Job_end_time_Def.

      (* Jobs will be scheduled on an uniprocessor *)
      Variable sched: schedule Job.

      (* Consider any job *)
      Variable job:Job.

      (* Recall the definition of scheduled_at for testing wether this job can 
        be scheduled at time t *)

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

      (* We define the function calculating the job's end time.
         It takes three arguments:
         t : job arrival instant
         c : job cost duration
         wf: an extra parameter that allows to realize a well-founded fixpoint
             with the type nat. It is supposed big enough to return the actual end time.
             Otherwise (i.e., it reaches 0), the function returns Failure t *)

      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'

      (* We define an end time predicate with three arguments:
         the job arrival instant, the job cost duration and 
         the job end time instant. Its three constructors 
         correspond to the cases:
         - cost = 0 and job has ended
         - cost > 0 and job cannot be scheduled at instant t
         - cost > 0 and job can be scheduled at instant t

      Inductive end_time_predicate : instant durationinstantProp:=
        |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.

      (* The predicate completes_at specifies the instant a job ends
          according to its arrival and cost *)

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

    End Job_end_time_Def.

    Section Lemmas.

      (* Consider any job *)
      Variable job:Job.

      (* ... and and uniprocessor schedule this job*)
      Variable sched: schedule Job.

      (* ... where jobs do not execute before their arrival times nor after completion *)
      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.

      (* Recall the function end_time_option*)
      Let job_end_time_function:= end_time_option sched job.

      (* Recall the end time predicate*)
      Let job_end_time_p:= end_time_predicate sched job.

      (* Recall the definition of completes_at*)
      Let job_completes_at := completes_at sched job.

      (* Recall the definition of scheduled_at for testing wether this job can 
        be scheduled at time t.*)

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

      (* Then, the job_end_time_function (if it terminates successfully) returns
         the same result as the job_end_time_p predicate *)

      (* function -> predicate *)
      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.

      (* The end time given by the predicate job_end_time_p  is the same as
         the result returned by the function job_end_time_function (provided
         wf is large enough) *)

      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.

      (* If we consider a time t where the job is not scheduled, then 
         the end_time_predicate returns the same end time starting from t or t+1 *)

      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.

      (* If we consider a time t where the job is scheduled, then the end_time_predicate 
         returns the same end time starting from t with a cost c+1 than from t+1 with a cost c*)

      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.

      (* Assume that the job end time is job_end *)
      Variable job_end: instant.

      (* Recall the definition of completed_by defined in
        model/schedule/uni/schedule.v *)

      Let job_completed_by:=
        completed_by job_cost sched.

      (* Recall the definition of service_during defined in
        model/schedule/uni/schedule.v *)

      Let job_service_during:=
        service_during sched job.

      (* then the job arrival is less than or equal to job end time *)
      Lemma arrival_le_end:
          t c e, job_end_time_p t c e t e.

      (* the sum of job arrival and job cost is less than or equal to 
        job end time*)

      Lemma arrival_add_cost_le_end:
         t c e,
          job_end_time_p t c e

      (* The servive received between the job arrival
         and the job end is equal to the job cost*)

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

      (* A job is completed by job end time*)
      Lemma completed_by_end_time:
        job_completes_at job_end
        job_completed_by job job_end.

      (* The job end time is positive *)
      Corollary end_time_positive:
        job_completes_at job_end job_end > 0.

      (* The service received between job arrival and the previous instant
         of job end time is exactly job cost-1*)

      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.

      (* At any instant from the job arrival and before the job end time,
         job cannot be finished; the service received is always less than job cost*)

      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.