Library prosa.analysis.definitions.job_response_time
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.