Library rt.restructuring.behavior.readiness.jitter

From mathcomp Require Export ssreflect ssrnat ssrbool.
From rt.restructuring.behavior Require Export ready.

(* WIP: define the readiness function for models with jitter (and no
   self-suspensions). *)

Section ReadinessOfJitteryJobs.
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

  Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.

  Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j ≤ t.

  (* A job that experiences jitter is ready only when the jitter-induced delay
     has passed after its arrival. *)
  Global Instance jitter_ready_instance : JobReady PState Job :=
    {
      job_ready sched j t := is_released j t && ~~ completed_by sched j t
    }.

End ReadinessOfJitteryJobs.