Library prosa.model.task.offset
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
Require Export prosa.behavior.all.
Require Export prosa.model.task.arrivals.
Require Export prosa.util.all.
Require Export prosa.analysis.facts.behavior.all.
Task Offset
In the following section, we define two important properties
that an offset of any task should satisfy.
Consider any type of tasks with offsets, ...
... any type of jobs associated with these tasks, ...
... and any arrival sequence.
No jobs of a task [tsk] arrive before [task_offset tsk].
Definition no_jobs_before_offset (tsk : Task) :=
∀ j,
job_task j = tsk →
job_arrival j ≥ task_offset tsk.
∀ j,
job_task j = tsk →
job_arrival j ≥ task_offset tsk.
Furthermore for a task [tsk], there exists a job that
arrives exactly at the offset.
Definition job_released_at_offset (tsk : Task) :=
∃ j',
arrives_in arr_seq j' ∧
job_task j' = tsk ∧
job_arrival j' = task_offset tsk.
∃ j',
arrives_in arr_seq j' ∧
job_task j' = tsk ∧
job_arrival j' = task_offset tsk.
An offset is valid iff it satisfies both of the above conditions.
In the context of a set of tasks [ts], ...
... all tasks in the set must have valid offsets.
In this section we define the notion of a maximum task offset.
Consider any type of tasks with offsets, ...
... and any task set.
We define the sequence of task offsets of all tasks in [ts], ...
... and the maximum among all the task offsets.