Library prosa.analysis.definitions.infinite_jobs

(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

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.