# Library prosa.classic.model.suspension

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop.

Module Suspension.

Import ArrivalSequence.

(* First, we define the actual job suspension times. *)
Section SuspensionTimes.

(* Consider any type of job. *)
Variable Job: eqType.

(* We define job suspension as a function that takes a job in the arrival
sequence and its current service and returns how long the job must
suspend next. *)

Definition job_suspension := Job (* job *)
time (* current service *)
duration. (* duration of next suspension *)

End SuspensionTimes.

(* Next, we define the total suspension time incurred by a job. *)
Section TotalSuspensionTime.

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

(* Consider any job suspension function. *)
Variable next_suspension: job_suspension Job.

(* Let j be any job. *)
Variable j: Job.

(* We define the total suspension time incurred by job j as the cumulative
duration of each suspension point t in the interval 0, job_cost j). *)

Definition total_suspension :=
\sum_(0 t < job_cost j) (next_suspension j t).

End TotalSuspensionTime.

(* In this section, we define the dynamic self-suspension model as an
upper bound on the total suspension times. *)

Section DynamicSuspensions.

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

(* Consider any job arrival sequence subject to job suspensions. *)
Variable next_suspension: job_suspension Job.

(* Recall the definition of total suspension time. *)
Let total_job_suspension := total_suspension job_cost next_suspension.

(* Next, assume that for each task a suspension bound is known. *)