Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_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]

Require Export prosa.model.task.arrival.curves.
Require Export prosa.analysis.facts.sporadic.arrival_bound.

(** Arrival Curve for Sporadic Tasks *)

(** Any analysis that supports arbitrary arrival curves can also be
    used to analyze sporadic tasks. We establish this link below. *)
Section SporadicArrivalCurve.
  (** Consider any type of sporadic tasks. *)
  Context {Task : TaskType} `{SporadicModel Task}.

  (** The bound on the maximum number of arrivals in a given interval
      [max_sporadic_arrivals] is in fact a valid arrival curve, which
      we note with the following arrival-curve declaration. *)
  Global Program Instance MaxArrivalsSporadic : MaxArrivals Task := max_sporadic_arrivals.

  (** It remains to be shown that [max_sporadic_arrivals] satisfies
      all expectations placed on arrival curves. First, we observe
      that the bound is structurally sound. *)
  
Task: TaskType
H: SporadicModel Task
forall tsk : Task,
valid_arrival_curve (max_sporadic_arrivals tsk)

  
Task: TaskType
H: SporadicModel Task
forall tsk : Task,
valid_arrival_curve (max_sporadic_arrivals tsk)

    
Task: TaskType
H: SporadicModel Task
tsk: Task
monotone leq (max_sporadic_arrivals tsk)

    
Task: TaskType
H: SporadicModel Task
tsk: Task
delta1, delta2: nat
LEQ: delta1 <= delta2
max_sporadic_arrivals tsk delta1 <=
max_sporadic_arrivals tsk delta2

    exact: div_ceil_monotone1.
  Qed.

  (** For convenience, we lift the preceding observation to the level
      of entire task sets. *)
  
Task: TaskType
H: SporadicModel Task
forall ts : TaskSet Task,
valid_taskset_arrival_curve ts max_arrivals

  
Task: TaskType
H: SporadicModel Task
forall ts : TaskSet Task,
valid_taskset_arrival_curve ts max_arrivals
 move=> ? ? ?; exact: sporadic_arrival_curve_valid. Qed.

   (** Next, we note that it is indeed an arrival bound. To this end,
       consider any type of jobs stemming from these tasks ... *)
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

  (** ... and any well-formed arrival sequence of such jobs. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** We establish the validity of the defined curve. *)
  Section Validity.

    (** Let [tsk] denote any valid sporadic task to be analyzed. *)
    Variable tsk : Task.
    Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
    Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.

    (** We observe that [max_sporadic_arrivals] is indeed an upper bound
        on the maximum number of arrivals. *)
    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model
  arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time
  tsk
respects_max_arrivals arr_seq tsk
  (max_sporadic_arrivals tsk)

    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
tsk: Task
H_sporadic_model: respects_sporadic_task_model
  arr_seq tsk
H_valid_inter_min_arrival: valid_task_min_inter_arrival_time
  tsk
respects_max_arrivals arr_seq tsk
  (max_sporadic_arrivals tsk)
 by move=> t1 t2 LEQ; apply: sporadic_task_arrivals_bound. Qed.

  End Validity.

  (** For convenience, we lift the preceding observation to the level
      of entire task sets. *)
  
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
forall ts : TaskSet Task,
valid_taskset_inter_arrival_times ts ->
taskset_respects_sporadic_task_model ts arr_seq ->
taskset_respects_max_arrivals arr_seq ts

  
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
forall ts : TaskSet Task,
valid_taskset_inter_arrival_times ts ->
taskset_respects_sporadic_task_model ts arr_seq ->
taskset_respects_max_arrivals arr_seq ts

    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: TaskSet Task
VAL: valid_taskset_inter_arrival_times ts
SPO: taskset_respects_sporadic_task_model ts arr_seq
tsk: Task
IN: tsk \in ts
respects_max_arrivals arr_seq tsk (max_arrivals tsk)

    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: TaskSet Task
VAL: valid_taskset_inter_arrival_times ts
SPO: taskset_respects_sporadic_task_model ts arr_seq
tsk: Task
IN: tsk \in ts
respects_sporadic_task_model arr_seq tsk
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: TaskSet Task
VAL: valid_taskset_inter_arrival_times ts
SPO: taskset_respects_sporadic_task_model ts arr_seq
tsk: Task
IN: tsk \in ts
valid_task_min_inter_arrival_time tsk

    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: TaskSet Task
VAL: valid_taskset_inter_arrival_times ts
SPO: taskset_respects_sporadic_task_model ts arr_seq
tsk: Task
IN: tsk \in ts
respects_sporadic_task_model arr_seq tsk
 exact: SPO.
    
Task: TaskType
H: SporadicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
ts: TaskSet Task
VAL: valid_taskset_inter_arrival_times ts
SPO: taskset_respects_sporadic_task_model ts arr_seq
tsk: Task
IN: tsk \in ts
valid_task_min_inter_arrival_time tsk
 exact: VAL.
  Qed.

End SporadicArrivalCurve.

(** We add the lemmas into the "Hint Database" basic_rt_facts so that
    they become available for proof automation. *)
Global Hint Resolve
  sporadic_arrival_curve_valid
  sporadic_task_sets_arrival_curve_valid
  sporadic_arrival_curve_respects_max_arrivals
  sporadic_task_sets_respects_max_arrivals
  : basic_rt_facts.