Library prosa.analysis.definitions.task_schedule
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
Due to historical reasons this file defines the notion of a
schedule of a task for the ideal uni-processor model. This is not
a fundamental limitation and the notion can be further generalized
to an arbitrary model.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Let [sched] be any ideal uni-processor schedule.
Let [tsk] be any task.
Next we define whether a task is scheduled at time [t], ...
Definition task_scheduled_at (t : instant) :=
if sched t is Some j then
job_task j == tsk
else false.
if sched t is Some j then
job_task j == tsk
else false.
...which also corresponds to the instantaneous service it receives.
Based on the notion of instantaneous service, we define the
cumulative service received by [tsk] during any interval [t1, t2)...
...and the cumulative service received by [tsk] up to time t2,
i.e., in the interval [0, t2).