arrival_bound.v

From HB Require Import structures.

[Loading ML file ring_plugin.cmxs (using legacy method) ... done]

[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]

[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]

Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.

[Loading ML file coq-elpi.elpi ... done]

Require Export prosa.implementation.definitions.extrapolated_arrival_curve.

[Loading ML file zify_plugin.cmxs (using legacy method) ... done]

[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]

[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]

[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]

Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]

(** * 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 [task_arrivals_bound : eqType]. *) HB.instance Definition _ := hasDecEq.Build task_arrivals_bound eqn_task_arrivals_bound.