Library prosa.classic.model.arrival.basic.job

Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssrnat ssrbool eqtype.

(* Properties of different types of job: *)
Module Job.

  Import Time ArrivalSequence.

  (* 1) Basic Job *)
  Section ValidJob.

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

    Variable j: Job.

    (* The job cost must be positive. *)
    Definition job_cost_positive := job_cost j > 0.

  End ValidJob.

  (* 2) Real-time job (with a deadline) *)
  Section ValidRealtimeJob.

    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.

    Variable j: Job.

    (* The job deadline must be positive and no less than its cost. *)
    Definition job_deadline_positive := job_deadline j > 0.
    Definition job_cost_le_deadline := job_cost j job_deadline j.

    Definition valid_realtime_job :=
      job_cost_positive job_cost j
      job_cost_le_deadline
      job_deadline_positive.

  End ValidRealtimeJob.

  (* 3) Job of sporadic task *)
  Section ValidSporadicTaskJob.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    Variable j: Job.

    (* The job cost cannot be larger than the task cost. *)
    Definition job_cost_le_task_cost :=
      job_cost j task_cost (job_task j).

    (* The job deadline must be equal to the task deadline. *)
    Definition job_deadline_eq_task_deadline :=
      job_deadline j = task_deadline (job_task j).

    Definition valid_sporadic_job :=
      valid_realtime_job job_cost job_deadline j
      job_cost_le_task_cost
      job_deadline_eq_task_deadline.

  End ValidSporadicTaskJob.

  (* 4) Job of task *)
  Section ValidTaskJob.

    Context {Task: eqType}.
    Variable task_cost: Task time.

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

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

    (* The job cost from the arrival sequence 
       cannot be larger than the task cost. *)

    Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
       j,
        arrives_in arr_seq j
        job_cost_le_task_cost task_cost job_cost job_task j.

  End ValidTaskJob.

End Job.