# Library prosa.model.task.arrival.sporadic

# The Sporadic Task Model

## Task Parameter for the Sporadic Task Model

Consider any type of sporadic tasks.

A valid sporadic task should have a non-zero minimum inter-arrival
time.

Further, in the context of a set of such tasks, ...

... every task in the set should have a valid inter-arrival time.

Definition valid_taskset_inter_arrival_times :=

∀ tsk : Task,

tsk \in ts → valid_task_min_inter_arrival_time tsk.

∀ tsk : Task,

tsk \in ts → valid_task_min_inter_arrival_time tsk.

Next, consider any type of jobs stemming from these tasks ...

... and an arbitrary arrival sequence of such jobs.

We say that a task respects the sporadic task model if the arrivals of
its jobs in the arrival sequence are appropriately spaced in time.

Given two different jobs j and j' ...

...that belong to the arrival sequence...

... and that stem from the given task, ...

... if the arrival of j precedes the arrival of j' ...,

then the arrival of j and the arrival of j' are separated by at least
one period.

Based on the above definition, we define the sporadic task model as
follows.

Definition taskset_respects_sporadic_task_model :=

∀ tsk, tsk \in ts → respects_sporadic_task_model tsk.

End ValidSporadicTaskModel.

∀ tsk, tsk \in ts → respects_sporadic_task_model tsk.

End ValidSporadicTaskModel.