Library prosa.implementation.definitions.extrapolated_arrival_curve
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.
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.
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).
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).
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.
Horizon should bound time steps.
Definition large_horizon (ac_prefix : ArrivalCurvePrefix) :=
∀ s, s \in time_steps_of ac_prefix → s ≤ horizon_of ac_prefix.
∀ 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).
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).
∀ (ac_prefix : ArrivalCurvePrefix),
reflect (large_horizon ac_prefix) (large_horizon_dec 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).
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.
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).
(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).
∀ (ac_prefix : ArrivalCurvePrefix),
reflect (valid_arrival_curve_prefix ac_prefix) (valid_arrival_curve_prefix_dec ac_prefix).
We also define a predicate for non-decreasing order that is
more convenient for proving some of the claims.