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)]).
The first component of arrival-curve prefix ac_prefix is called horizon.
The second component of ac_prefix is called steps.
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.
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).
In the following section, we define a few validity predicates.
Horizon should be positive.
Horizon should bound time steps.
We define an alternative, decidable version of large_horizon...
... 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.
    moveac.
    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).
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.
We define an alternative, decidable version of valid_arrival_curve_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.
    moveac.
    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.