Library prosa.implementation.definitions.extrapolated_arrival_curve

Require Export prosa.behavior.time.
Require Export prosa.util.all.

This file introduces an implementation of arrival curves via the periodic extension of finite arrival-curve prefix. An arrival-curve prefix is a pair comprising a horizon and a list of steps. The horizon defines the domain of the prefix, in which no extrapolation is necessary. The list of steps (duration × value) describes the value changes of the corresponding arrival curve within the domain.
For time instances outside of an arrival-curve prefix's domain, extrapolation is necessary. Therefore, past the domain, arrival-curve values are extrapolated assuming that the arrival-curve prefix is repeated with a period equal to the horizon.
Note that such a periodic extension does not necessarily give the tightest curve, and hence it is not optimal. The advantage is speed of calculation: periodic extension can be done in constant time, whereas the optimal extension takes roughly quadratic time in the number of steps.
An arrival-curve prefix is defined as a pair comprised of a horizon and a list of steps (duration × value) that describe the value changes of the described arrival curve.
For example, an arrival-curve prefix (5, [:: (1, 3)]) describes an arrival sequence with job bursts of size 3 happening every 5 time instances.
Definition ArrivalCurvePrefix : Type := duration × seq (duration × nat).

Given an inter-arrival time p (or period p), the corresponding arrival-curve prefix can be defined as (p, [:: (1, 1)]).
Definition inter_arrival_to_prefix (p : nat) : ArrivalCurvePrefix := (p, [:: (1, 1)]).

The first component of arrival-curve prefix ac_prefix is called horizon.
Definition horizon_of (ac_prefix : ArrivalCurvePrefix) := fst ac_prefix.

The second component of ac_prefix is called steps.
Definition steps_of (ac_prefix : ArrivalCurvePrefix) := snd ac_prefix.

The time steps of ac_prefix are the first components of the steps. That is, these are time instances before the horizon where the corresponding arrival curve makes a step.
Definition time_steps_of (ac_prefix : ArrivalCurvePrefix) :=
  map fst (steps_of ac_prefix).

The function step_at returns the last step (duration × value) such that duration ≤ t.
Definition step_at (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  last (0, 0) [ seq step <- steps_of ac_prefix | fst step ≤ t ].

(* The function value_at returns the _value_ of the last step
   (duration × value) such that duration ≤ t *)
Definition value_at (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  snd (step_at ac_prefix t).

Finally, we define a function extrapolated_arrival_curve that performs the periodic extension of the arrival-curve prefix (and hence, defines an arrival curve).
Value of extrapolated_arrival_curve t is defined as t %/ h × value_at horizon plus value_at (t mod horizon). The first summand corresponds to k full repetitions of the arrival-curve prefix inside interval [0,t). The second summand corresponds to the residual change inside interval [k*h, t).
Definition extrapolated_arrival_curve (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  let h := horizon_of ac_prefix in
  t %/ h × value_at ac_prefix h + value_at ac_prefix (t %% h).

In the following section, we define a few validity predicates.
Section ValidArrivalCurvePrefix.

Horizon should be positive.
  Definition positive_horizon (ac_prefix : ArrivalCurvePrefix) :=
    horizon_of ac_prefix > 0.

Horizon should bound time steps.
  Definition large_horizon (ac_prefix : ArrivalCurvePrefix) :=
    ∀ s, s \in time_steps_of ac_prefix → s ≤ horizon_of ac_prefix.

We define an alternative, decidable version of large_horizon...
  Definition large_horizon_dec (ac_prefix : ArrivalCurvePrefix) : bool :=
    all (fun s ⇒ s ≤ horizon_of ac_prefix) (time_steps_of ac_prefix).

... and prove that the two definitions are equivalent.
  Lemma large_horizon_P :
    ∀ (ac_prefix : ArrivalCurvePrefix),
      reflect (large_horizon ac_prefix) (large_horizon_dec ac_prefix).
  Proof.
    move⇒ ac.
    apply /introP; first by move⇒ /allP ?.
    apply ssr.ssrbool.contraNnot ⇒ ?.
    by apply /allP.
  Qed.

There should be no infinite arrivals; that is, value_at 0 = 0.
  Definition no_inf_arrivals (ac_prefix : ArrivalCurvePrefix) :=
    value_at ac_prefix 0 == 0.

Bursts must be specified; that is, steps_of should contain a pair (ε, b).
  Definition specified_bursts (ac_prefix : ArrivalCurvePrefix) :=
    ε \in time_steps_of ac_prefix.

Steps should be strictly increasing both in time steps and values.
  Definition ltn_steps a b := (fst a < fst b) && (snd a < snd b).
  Definition sorted_ltn_steps (ac_prefix : ArrivalCurvePrefix) :=
    sorted ltn_steps (steps_of ac_prefix).

The conjunction of the 5 afore-defined properties defines a valid arrival-curve prefix.
  Definition valid_arrival_curve_prefix (ac_prefix : ArrivalCurvePrefix) :=
    positive_horizon ac_prefix
    ∧ large_horizon ac_prefix
    ∧ no_inf_arrivals ac_prefix
    ∧ specified_bursts ac_prefix
    ∧ sorted_ltn_steps ac_prefix.

We define an alternative, decidable version of valid_arrival_curve_prefix...
  Definition valid_arrival_curve_prefix_dec (ac_prefix : ArrivalCurvePrefix) : bool :=
    (positive_horizon ac_prefix)
    && (large_horizon_dec ac_prefix)
    && (no_inf_arrivals ac_prefix)
    && (specified_bursts ac_prefix)
    && (sorted_ltn_steps ac_prefix).

... and prove that the two definitions are equivalent.
  Lemma valid_arrival_curve_prefix_P :
    ∀ (ac_prefix : ArrivalCurvePrefix),
      reflect (valid_arrival_curve_prefix ac_prefix) (valid_arrival_curve_prefix_dec ac_prefix).
  Proof.
    move⇒ ac.
    apply /introP.
    - by move ⇒ /andP[/andP[/andP[/andP[? /large_horizon_P ?] ?]?]?].
    - apply ssr.ssrbool.contraNnot.
      move⇒ [?[/large_horizon_P ?[?[??]]]].
      by repeat (apply /andP; split ⇒ //).
  Qed.

We also define a predicate for non-decreasing order that is more convenient for proving some of the claims.
  Definition leq_steps a b := (fst a ≤ fst b) && (snd a ≤ snd b).
  Definition sorted_leq_steps (ac_prefix : ArrivalCurvePrefix) :=
    sorted leq_steps (steps_of ac_prefix).

End ValidArrivalCurvePrefix.