Library prosa.classic.model.arrival.curves.bounds

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence
        prosa.classic.model.arrival.basic.task_arrival.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div.

Module ArrivalCurves.

  Import ArrivalSequence TaskArrival.

  Section DefiningArrivalCurves.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.

    Let arrivals_of_tsk tsk := arrivals_of_task_between job_task arr_seq tsk.
    Let num_arrivals_of_tsk tsk := num_arrivals_of_task job_task arr_seq tsk.

    Section ArrivalBound.

      Variable max_arrivals: Task → time → nat.

      Definition is_arrival_bound (tsk: Task) :=
        ∀ (t1 t2: time),
          t1 ≤ t2 →
          num_arrivals_of_tsk tsk t1 t2 ≤ max_arrivals tsk (t2 - t1).

      Definition is_arrival_bound_for_taskset (ts: seq Task) :=
        ∀ (tsk: Task), tsk \in ts → is_arrival_bound tsk.

      Definition zero_arrival_curve (tsk: Task) :=
        max_arrivals tsk 0 = 0.

      Definition monotonic_arrival_curve (tsk: Task) :=
        monotone (max_arrivals tsk) leq.

      Definition proper_arrival_curve (tsk: Task) :=
        is_arrival_bound tsk ∧
        zero_arrival_curve tsk ∧
        monotonic_arrival_curve tsk.

      Definition family_of_proper_arrival_curves (ts: seq Task) :=
        ∀ (tsk: Task), tsk \in ts → proper_arrival_curve tsk.

    End ArrivalBound.

    Section SeparationBound.

      Variable min_length: Task → nat → time.

      Definition is_separation_bound tsk :=
        ∀ t1 t2,
          t1 ≤ t2 →
          min_length tsk (num_arrivals_of_tsk tsk t1 t2) ≤ t2 - t1.

    End SeparationBound.

  End DefiningArrivalCurves.

End ArrivalCurves.