Library prosa.model.task.arrival.example

Arrival Model Conversion

This file demonstrates the automatic conversion of arrival models. In particular, we show how a set of periodic tasks can be interpreted also as (1) sporadic tasks with minimum inter-arrival times, (2) sporadic tasks with arrival curves, and (3) request-bound functions.
Consider periodic tasks ...
  Context {Task : TaskType} `{PeriodicModel Task}.

... and their corresponding jobs.
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.

Given a set of such periodic tasks ...
  Variable ts : TaskSet Task.

... and a valid arrival sequence, ...
... if the tasks are valid periodic tasks, ...
... then we can automatically interpret them also as satisfying other arrival models, as we demonstrate in the following.

Periodic Tasks as Sporadic Tasks

The tasks satisfy the sporadic validity constraint...
... and arrival sequence is legal under the sporadic task model.

Periodic Tasks as Arrival Curves

The tasks satisfy the arrival-curve validity constraint...
... and the arrival sequence is legal under the arrival-curve model.

Periodic Tasks as RBFs

Assuming that each task has a WCET...
  Context `{TaskCost Task}.

... and that jobs are compliant with the WCET, ...
  Context `{JobCost Job}.
  Hypothesis H_valid_costs : jobs_have_valid_job_costs.

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