Library rt.restructuring.model.task.sequentiality

Require Export rt.restructuring.model.task.concept.
Section PropertyOfSequentiality.

Consider any type of job associated with any type of tasks...
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.

... with arrival times and costs ...
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... and any kind of processor state model.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

Given a schedule ...
  Variable sched: schedule PState.

...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.