sequential.v

Require Export rt.restructuring.model.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 tasks are sequential if each task's jobs
     are executed in the order they arrived. *)
  Definition sequential_tasks :=
    forall (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.