Project Page Index Table of Contents

# 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.
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).