Library prosa.model.task.sequentiality
In this module, we give a precise definition of the common notion of
"sequential tasks", which is commonly understood to mean that the jobs of a
sequential task execute in sequence and in a non-overlapping fashion.
Consider any type of jobs stemming from any type of tasks ...
... with arrival times and costs ...
... and any kind of processor model.
Given a schedule of such jobs ...
... we say that the tasks execute sequentially if each task's jobs are
executed in arrival order and in a non-overlapping fashion.
Definition sequential_tasks :=
∀ (j1 j2: Job) (t: instant),
same_task j1 j2 →
job_arrival j1 < job_arrival j2 →
scheduled_at sched j2 t →
completed_by sched j1 t.
End PropertyOfSequentiality.
∀ (j1 j2: Job) (t: instant),
same_task j1 j2 →
job_arrival j1 < job_arrival j2 →
scheduled_at sched j2 t →
completed_by sched j1 t.
End PropertyOfSequentiality.