Project Page Index Table of Contents

# 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.