# Library prosa.implementation.definitions.arrival_bound

From HB Require Import structures.
Require Export prosa.implementation.definitions.extrapolated_arrival_curve.

# Implementation of a Task's Arrival Bound

In this file, we define a reference implementation of the notion of a task's arrival bound.
Note that its use is entirely optional: clients of Prosa may choose to use this type or implement their own notion of arrival bounds.
A task's arrival bound is an inductive type comprised of three types of arrival patterns: (a) periodic, characterized by a period between consequent activation of a task, (b) sporadic, characterized by a minimum inter-arrival time, or (c) arrival-curve prefix, characterized by a finite prefix of an arrival curve.
Inductive task_arrivals_bound :=
| Periodic : nat → task_arrivals_bound
| Sporadic : nat → task_arrivals_bound
| ArrivalPrefix : ArrivalCurvePrefix → task_arrivals_bound.
To make it compatible with ssreflect, we define a decidable equality for arrival bounds.
Definition task_arrivals_bound_eqdef (tb1 tb2 : task_arrivals_bound) :=
match tb1, tb2 with
| Periodic p1, Periodic p2 ⇒ p1 == p2
| Sporadic s1, Sporadic s2 ⇒ s1 == s2
| ArrivalPrefix s1, ArrivalPrefix s2 ⇒ s1 == s2
| _, _ ⇒ false
end.
Next, we prove that task_eqdef is indeed an equality, ...
Lemma eqn_task_arrivals_bound : Equality.axiom task_arrivals_bound_eqdef.
Proof.
intros x y.
destruct (task_arrivals_bound_eqdef x y) eqn:EQ.
{ apply ReflectT; destruct x, y.
all: try by move: EQ ⇒ /eqP EQ; subst.
}
{ apply ReflectF; destruct x, y.
all: try by move: EQ ⇒ /eqP EQ.
all: by move: EQ ⇒ /neqP; intros NEQ1 NEQ2; apply NEQ1; inversion NEQ2.
}
Qed.
..., which allows instantiating the canonical structure for task_arrivals_bound : eqType.
HB.instance Definition _ := hasDecEq.Build task_arrivals_bound eqn_task_arrivals_bound.