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.

The function step_at returns the last step (duration × value) such that duration ≤ t.

The function value_at returns the value of the last step (duration × value) such that duration ≤ 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.

There should be no infinite arrivals; that is, value_at 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.

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.

We also define a predicate for non-decreasing order that is more convenient for proving some of the claims.