Library prosa.classic.model.suspension

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

Module Suspension.

  Import ArrivalSequence.

  Section SuspensionTimes.

    Variable Job: eqType.

    Definition job_suspension := Job →
                                 time →
                                 duration.
  End SuspensionTimes.

  Section TotalSuspensionTime.

    Context {Job: eqType}.
    Variable job_cost: Job → time.

    Variable next_suspension: job_suspension Job.

    Variable j: Job.

    Definition total_suspension :=
      \sum_(0 ≤ t < job_cost j) (next_suspension j t).

  End TotalSuspensionTime.

  Section DynamicSuspensions.

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

    Variable next_suspension: job_suspension Job.

    Let total_job_suspension := total_suspension job_cost next_suspension.

    Variable suspension_bound: Task → duration.

    Definition dynamic_suspension_model :=
      ∀ j, total_job_suspension j ≤ suspension_bound (job_task j).

  End DynamicSuspensions.

End Suspension.