Library probsa.rt.model.min_inter_arrival

(* --------------------------------- Prosa ---------------------------------- *)
Require Export prosa.model.task.concept.
Require Export prosa.model.task.arrival.sporadic.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.rt.behavior Require Export job arrival_sequence.

(* ---------------------------------- Main ---------------------------------- *)

Minimum Inter-Arrival Time

Section MinimumInterArrival.

Consider a probability space (Ω, μ), ...

Context {Ω} {μ : measure Ω}.

... any type of tasks with minimum inter-arrival time defined by a function task_min_inter_arrival_time from a type-class SporadicModel, ...

Context {Task : TaskType} `{SporadicModel Task}.

... and any fin-type of jobs associated with these tasks. Assume that the jobs have probabilistic arrival times defined by job_arrival.

  Context {Job : finType}.
  Context {job_arrival : JobCostRV Job Ω μ}
          {job_task : JobTask Job Task}.

For convenience, we denote the probabilistic arrival sequence as ξ_pr.

Let ξ_pr := arr_seq (job_arrival := job_arrival).

We say that task_min_inter_arrival_time (defined by SporadicModel) is a valid minimum inter-arrival time iff

for any evolution ω ∈ Ω, any time instants t1 and t2 such that t1 ≤ t2, and any two distinct jobs j and j' of the same task task (job_task j = job_task j'), the fact that j arrives at t1 and j' arrives at t2 implies that the difference between time instances t1 and t2 is at least task_min_inter_arrival_time (job_task j).

  Definition valid_min_inter_arrival :=
    ∀ ω, ∀ t1 t2, ∀ j j',
      job_task j = job_task j' →
      (t1 ≤ t2)%nat ∧ (j \in ξ_pr ω t1 ) ∧ (j' \in ξ_pr ω t2 ) ∧ (j != j') →
      (t2 - t1 ≥ task_min_inter_arrival_time (job_task j))%nat.

End MinimumInterArrival.