Library prosa.analysis.definitions.job_response_time
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.all.
In this section we define what it means for the response time
of a job to exceed some given duration.
Consider any kind of jobs ...
... and any kind of processor state.
Consider any schedule.
We say that a job [j] has a response time exceeding a number [x]
if [j] is pending [x] units of time after its arrival.
Definition job_response_time_exceeds (j : Job) (x : duration) :=
~~ completed_by sched j ((job_arrival j) + x).
End JobResponseTimeExceeds.
~~ completed_by sched j ((job_arrival j) + x).
End JobResponseTimeExceeds.