Library rt.restructuring.analysis.task_schedule
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.model Require Import task.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Due to historical reasons this file defines the notion of a schedule of
a task for the ideal uniprocessor model. This is not a fundamental limitation
and the notion can be further generalized to an arbitrary model.
Schedule of task
In this section we define properties of schedule of a task
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 uniprocessor 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).
Definition task_service (t2 : instant) := task_service_during 0 t2.
End TaskProperties.
End ScheduleOfTask.
End TaskProperties.
End ScheduleOfTask.