# Library prosa.implementation.definitions.arrival_bound

# Implementation of a Task's Arrival Bound

Inductive task_arrivals_bound :=

| Periodic : nat → task_arrivals_bound

| Sporadic : nat → task_arrivals_bound

| ArrivalPrefix : ArrivalCurvePrefix → 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.

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

Canonical task_arrivals_bound_eqMixin := EqMixin eqn_task_arrivals_bound.

Canonical task_arrivals_bound_eqType := Eval hnf in EqType task_arrivals_bound task_arrivals_bound_eqMixin.

Canonical task_arrivals_bound_eqType := Eval hnf in EqType task_arrivals_bound task_arrivals_bound_eqMixin.