Library prosa.analysis.definitions.finish_time
Finish Time of a Job
Consider any type of jobs with arrival times and costs ...
... and any schedule of such jobs.
Consider an arbitrary job j.
In the following, we proceed under the assumption that j finishes
eventually (i.e., no later than R time units after its arrival, for any
finite R).
For technical reasons, we restate the response-time assumption explicitly
as an existentially quantified variable.
We are now ready for the main definition: job j's finish time is the
earliest time t such that completed_by sched j t holds. This time can
be computed with ssreflect's ex_minn utility function, which is
convenient because then we can reuse the corresponding lemmas.
In the following, we demonstrate the reuse of ex_minn properties by
establishing three natural properties of a job's finish time.
First, a job is indeed complete at its finish time.
Second, a job's finish time is the earliest time that it is complete.
Third, Prosa's notion of completes_at is satisfied at the finish time.
Finally, we can define a job's precise response time as usual as the time
from its arrival until its finish time.