Require Export prosa.model.task.arrival.curves.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.util.supremum.

(** * A Maximal Arrival Sequence *)

(** In this section, we propose a concrete instantiation of an arrival sequence.
    Given an arbitrary arrival curve, the defined arrival sequence tries to
    generate as many jobs as possible at any time instant by adopting a greedy
    strategy: at each time [t], the arrival sequence contains the maximum possible
    number of jobs that does not violate the given arrival curve's constraints. *)
Section MaximalArrivalSequence.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

  (** ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Let [max_arrivals] denote any function that takes a task and an interval length
      and returns the associated number of job arrivals of the task. *)
  Context `{MaxArrivals Task}.

  (** In this section, we define a procedure that computes the maximal number of
      jobs that can be released at a given instant without violating the
      corresponding arrival curve. *)
  Section NumberOfJobs.

    (** Let [tsk] be any task. *)
    Variable tsk : Task.

    (** First, we introduce a function that computes the sum of all elements in
        a given list's suffix of length [n]. *)
    Definition suffix_sum xs n := \sum_(size xs - n <= t < size xs) nth 0 xs t.

    (** Let the arrival prefix [arr_prefix] be a sequence of natural numbers,
        where [nth xs t] denotes the number of jobs that arrive at time [t].
        Then, given an arrival curve [max_arrivals] and an arrival prefix
        [arr_prefix], we define a function that computes the number of jobs that
        can be additionally released without violating the arrival curve.

        The high-level idea is as follows. Let us assume that the length of the
        arrival prefix is [Δ]. To preserve the sub-additive property, one needs
        to go through all suffixes of the arrival prefix and pick the
        minimum. *)
    Definition jobs_remaining (arr_prefix : seq nat) :=
      supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].

    (** Further, we define the function [next_max_arrival] to handle a special
        case: when the arrival prefix is empty, the function returns the value
        of the arrival curve with a window length of [1]. Otherwise, it returns
        the number the number of jobs that can additionally be generated.  *)
    Definition next_max_arrival (arr_prefix : seq nat) :=
      match jobs_remaining arr_prefix with
      | None => max_arrivals tsk 1
      | Some n => n
      end.

    (** Next, we define a function that extends by one a given arrival prefix... *)
    Definition extend_arrival_prefix (arr_prefix : seq nat) :=
      arr_prefix ++ [:: next_max_arrival arr_prefix ].

    (** ... and a function that generates a maximal arrival prefix
        of size [t], starting from an empty arrival prefix. *)
    Definition maximal_arrival_prefix (t : nat) :=
      iter t.+1 extend_arrival_prefix [::].

    (** Finally, we define a function that returns the maximal number
        of jobs that can be released at time [t]; this definition
        assumes that at each time instant prior to time [t] the maximal
        number of jobs were released. *)
    Definition max_arrivals_at t := nth 0 (maximal_arrival_prefix t) t.

  End NumberOfJobs.

  (** Consider a function that generates [n] concrete jobs of
      the given task at the given time instant. *)
  Variable generate_jobs_at : Task -> nat -> instant -> seq Job.

  (** The maximal arrival sequence of task set [ts] at time [t] is a
      concatenation of sequences of generated jobs for each task. *)
  Definition concrete_arrival_sequence (ts : seq Task) (t : instant) :=
    \cat_(tsk <- ts) generate_jobs_at tsk (max_arrivals_at tsk t) t.

End MaximalArrivalSequence.