Library prosa.classic.model.schedule.uni.limited.rbf

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task_arrival
               prosa.classic.model.priority
               prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.curves.bounds.
Require Import prosa.classic.analysis.uni.arrival_curves.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Module RBF.

  Import Job Time ArrivalSequence ArrivalCurves TaskArrival Priority MaxArrivalsWorkloadBound.

  Section RBFProperties.

    Context {Task: eqType}.
    Variable task_cost: Task → time.

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

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    Variable higher_eq_priority: FP_policy Task.
    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.

    Variable tsk: Task.

    Variable max_arrivals: Task → time → nat.
    Hypothesis H_proper_arrival_curve:
      proper_arrival_curve job_task arr_seq max_arrivals tsk.

    Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.

    Lemma task_rbf_0_zero:
      task_rbf 0 = 0.

    Lemma task_rbf_monotone:
      monotone task_rbf leq.

    Variable j: Job.
    Hypothesis H_j_arrives: arrives_in arr_seq j.
    Hypothesis H_job_of_tsk: job_task j = tsk.

    Lemma task_rbf_1_ge_task_cost:
      task_rbf 1 ≥ task_cost tsk.

  End RBFProperties.

End RBF.