# 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_consistent_arrivals: consistent_arrival_times arr_seq. Hypothesis

H_uniq_arr_seq: arrival_sequence_uniq arr_seq.

H_consistent_arrivals: consistent_arrival_times arr_seq. Hypothesis

H_uniq_arr_seq: arrival_sequence_uniq 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.