Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(** * 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.
Equality.axiom (T:=task_arrivals_bound)
  task_arrivals_bound_eqdef
Proof.
Equality.axiom (T:=task_arrivals_bound)
  task_arrivals_bound_eqdef
  intros x y.
x, y: task_arrivals_bound
reflect (x = y) (task_arrivals_bound_eqdef x y)
  destruct (task_arrivals_bound_eqdef x y) eqn:EQ.
x, y: task_arrivals_bound
EQ: task_arrivals_bound_eqdef x y = true
reflect (x = y) true
x, y: task_arrivals_bound
EQ: task_arrivals_bound_eqdef x y = false
reflect (x = y) false
  {
x, y: task_arrivals_bound
EQ: task_arrivals_bound_eqdef x y = true
reflect (x = y) true apply ReflectT; destruct x, y.
n, n0: nat
EQ: task_arrivals_bound_eqdef (Periodic n)
  (Periodic n0) = true
Periodic n = Periodic n0
n, n0: nat
EQ: task_arrivals_bound_eqdef (Periodic n)
  (Sporadic n0) = true
Periodic n = Sporadic n0
n: nat
a: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (Periodic n)
  (ArrivalPrefix a) = true
Periodic n = ArrivalPrefix a
n, n0: nat
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (Periodic n0) = true
Sporadic n = Periodic n0
n, n0: nat
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (Sporadic n0) = true
Sporadic n = Sporadic n0
n: nat
a: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (ArrivalPrefix a) = true
Sporadic n = ArrivalPrefix a
a: ArrivalCurvePrefix
n: nat
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (Periodic n) = true
ArrivalPrefix a = Periodic n
a: ArrivalCurvePrefix
n: nat
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (Sporadic n) = true
ArrivalPrefix a = Sporadic n
a, a0: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (ArrivalPrefix a0) = true
ArrivalPrefix a = ArrivalPrefix a0
    all: try by move: EQ => /eqP EQ; subst.
  }
x, y: task_arrivals_bound
EQ: task_arrivals_bound_eqdef x y = false
reflect (x = y) false
  {
x, y: task_arrivals_bound
EQ: task_arrivals_bound_eqdef x y = false
reflect (x = y) false apply ReflectF; destruct x, y.
n, n0: nat
EQ: task_arrivals_bound_eqdef (Periodic n)
  (Periodic n0) = false
Periodic n <> Periodic n0
n, n0: nat
EQ: task_arrivals_bound_eqdef (Periodic n)
  (Sporadic n0) = false
Periodic n <> Sporadic n0
n: nat
a: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (Periodic n)
  (ArrivalPrefix a) = false
Periodic n <> ArrivalPrefix a
n, n0: nat
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (Periodic n0) = false
Sporadic n <> Periodic n0
n, n0: nat
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (Sporadic n0) = false
Sporadic n <> Sporadic n0
n: nat
a: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (ArrivalPrefix a) = false
Sporadic n <> ArrivalPrefix a
a: ArrivalCurvePrefix
n: nat
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (Periodic n) = false
ArrivalPrefix a <> Periodic n
a: ArrivalCurvePrefix
n: nat
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (Sporadic n) = false
ArrivalPrefix a <> Sporadic n
a, a0: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (ArrivalPrefix a0) = false
ArrivalPrefix a <> ArrivalPrefix a0
    all: try by move: EQ => /eqP EQ.
n, n0: nat
EQ: task_arrivals_bound_eqdef (Periodic n)
  (Periodic n0) = false
Periodic n <> Periodic n0
n, n0: nat
EQ: task_arrivals_bound_eqdef (Sporadic n)
  (Sporadic n0) = false
Sporadic n <> Sporadic n0
a, a0: ArrivalCurvePrefix
EQ: task_arrivals_bound_eqdef (ArrivalPrefix a)
  (ArrivalPrefix a0) = false
ArrivalPrefix a <> ArrivalPrefix a0
    all: by move: EQ => /neqP; intros NEQ1 NEQ2; apply NEQ1; inversion NEQ2.
  }
Qed.

(** ..., which allows instantiating the canonical structure for [[eqType of task_arrivals_bound]]. *)
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.