Library prosa.model.task.sequentiality

Require Export prosa.model.task.concept.
Require Export prosa.model.task.arrivals.

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 ...
  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 model.
  Context {PState : ProcessorState Job}.

Consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule of this arrival sequence.
  Variable sched : schedule PState.

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),
      arrives_in arr_seq j1
      arrives_in arr_seq j2
      same_task j1 j2
      job_arrival j1 < job_arrival j2
      scheduled_at sched j2 t
      completed_by sched j1 t.

Given a job j and a time instant t, we say that all prior jobs are completed if any job j_tsk of task job_task j that arrives before time job_arrival j is completed by time t.
  Definition prior_jobs_complete (j : Job) (t : instant) :=
    all
      (fun j_tskcompleted_by sched j_tsk t)
      (task_arrivals_before arr_seq (job_task j) (job_arrival j)).

End PropertyOfSequentiality.