# Library prosa.analysis.definitions.task_schedule

Require Export prosa.model.task.concept.
Require Export prosa.analysis.definitions.service.
Require Export prosa.model.schedule.scheduled.

# Schedule and Service of task

In this section we define properties of the schedule and service of a task.
Section ScheduleAndServiceOfTask.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence of such jobs.
Variable arr_seq : arrival_sequence Job.
Let sched be any kind of schedule
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Let tsk be any task.
Variable tsk : Task.
We define a set of jobs of task tsk that are scheduled at time t.
Definition scheduled_jobs_of_task_at (t : instant) :=
[seq j <- scheduled_jobs_at arr_seq sched t | job_of_task tsk j].
Next we define whether task tsk is scheduled at time t.
Definition task_scheduled_at (t : instant) :=
scheduled_jobs_of_task_at t != [::].
We define the instantaneous service of tsk as the total instantaneous service of all jobs of this task scheduled at time t.
Definition task_service_at (t : instant) :=
\sum_(j <- scheduled_jobs_of_task_at t) service_at sched j t.
Based on the notion of instantaneous service, we define the cumulative service received by tsk during any interval `[t1, t2)` ...
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) task_service_at t.
...and the cumulative service received by tsk up to time t2, i.e., in the interval `[0, t2)`.
Definition task_service (t2 : instant) := task_service_during 0 t2.
Similarly, we define a set of jobs of task tsk receiving service at time t.
Definition served_jobs_of_task_at (t : instant) :=
[seq j <- scheduled_jobs_of_task_at t | receives_service_at sched j t].
Next, we define whether tsk is served at time t.
Definition task_served_at (t : instant) :=
served_jobs_of_task_at t != [::].
End ScheduleAndServiceOfTask.