Library prosa.model.task.offset
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.
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.
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.