Library rt.restructuring.model.schedule.sequential
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task.
Section PropertyOfSequentiality.
Consider any type of job associated with any type of tasks...
... with arrival times and costs ...
... and any kind of processor state model.
Given a schedule ...
...we say that tasks are sequential if each task's jobs
are executed in the order they arrived.
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.