Concrete arrival sequence

Added definitions and facts about the concrete arrival sequence, used in Poet to generate assumption-less certificates

implementation/definitions/maximal_arrival_sequence.v

+Require Import prosa.model.processor.ideal.
+Require Import prosa.model.task.concept.
+Require Import prosa.model.task.arrival.curves.
+Require Export prosa.analysis.facts.model.task_arrivals.
+Require Export prosa.util.all.
+
+(** 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 [MaxArrivals] 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 time 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 the 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.