Library prosa.analysis.definitions.infinite_jobs

Require Export prosa.model.task.arrivals.

In this section we define the notion of an infinite release of jobs by a task.
Section InfiniteJobs.

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

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

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

We say that a task tsk releases an infinite number of jobs if for every integer n there exists a job j of task tsk such that job_index of j is equal to n.
  Definition infinite_jobs :=
     tsk n,
     j,
      arrives_in arr_seq j
      job_task j = tsk
      job_index arr_seq j = n.

End InfiniteJobs.