Library prosa.analysis.facts.model.task_schedule

Require Export prosa.model.task.concept.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.ideal.schedule.

In this file we provide basic properties related to schedule of a task.
Section TaskSchedule.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Let sched be any ideal uni-processor schedule.
  Variable sched : schedule (ideal.processor_state Job).

Let tsk be any task.
  Variable tsk : Task.

We show that if a job of task tsk is scheduled at time t, then task tsk is scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled :
    ∀ j t,
      job_of_task tsk j →
      scheduled_at sched j t →
      task_scheduled_at sched tsk t.

And vice versa, if no job of task tsk is scheduled at time t, then task tsk is not scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled':
    ∀ j t,
      ~~ job_of_task tsk j →
      scheduled_at sched j t →
      ~~ task_scheduled_at sched tsk t.

End TaskSchedule.