# Library prosa.model.task.arrival.example

Require Import prosa.model.task.arrival.periodic.

Require Import prosa.model.task.arrival.periodic_as_sporadic.

Require Import prosa.model.task.arrival.sporadic_as_curve.

Require Import prosa.model.task.arrival.curve_as_rbf.

Require Import prosa.model.task.arrival.periodic_as_sporadic.

Require Import prosa.model.task.arrival.sporadic_as_curve.

Require Import prosa.model.task.arrival.curve_as_rbf.

# Arrival Model Conversion

Consider periodic tasks ...

... and their corresponding jobs.

Given a set of such periodic tasks ...

... and a valid arrival sequence, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... if the tasks are valid periodic tasks, ...

Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.

Hypothesis H_valid_periods : valid_periods ts.

Hypothesis H_valid_periods : valid_periods ts.

... then we can automatically interpret them also as satisfying
other arrival models, as we demonstrate in the following.
The tasks satisfy the sporadic validity constraint...

## Periodic Tasks as Sporadic Tasks

... and arrival sequence is legal under the sporadic task
model.

... and the arrival sequence is legal under the arrival-curve
model.

... and that jobs are compliant with the WCET, ...

... the tasks satisfy the RBF validity constraint...

... and the arrival sequence is legal under the RBF model.

Thanks to type-class resolution, all conversions from more
restrictive to less restrictive task model happen transparently
and the and necessary proofs are found automatically.
Of course, it is possible to start from sporadic tasks or tasks
with arrival curves, too.