Library rt.restructuring.model.schedule.sequential

From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.model Require Export task.

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 jobs (or, rather, tasks) are sequential if each task's jobs
     are executed in the order they arrived. *)
  Definition sequential_jobs :=
    ∀ (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.