Library prosa.behavior.service
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.schedule.
Section Service.
Consider any schedule.
First, we define whether a job [j] is scheduled at time [t], ...
... and the instantaneous service received by job j at time t.
Based on the notion of instantaneous service, we define the cumulative
service received by job j during any interval from [t1] until (but not
including) [t2].
Using the previous definition, we define the cumulative service received
by job [j] up to (but not including) time [t].
Job Completion and Response Time
We say that job [j] has completed by time [t] if it received all required
service in the interval from [0] until (but not including) [t].
We say that job [j] completes at time [t] if it has completed by time [t] but
not by time [t - 1].
We say that a constant [R] is a response time bound of a job [j] if [j]
has completed by [R] units after its arrival.
We say that a job meets its deadline if it completes by its absolute deadline.
Pending or Incomplete Jobs
Job [j] is pending earlier and at time [t] iff it has arrived before time [t]
and has not been completed yet.
Definition pending_earlier_and_at (j : Job) (t : instant) :=
arrived_before j t && ~~ completed_by j t.
arrived_before j t && ~~ completed_by j t.
Let's define the remaining cost of job [j] as the amount of service that
has yet to be received for it to complete.