Library rt.restructuring.behavior.readiness.basic

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

(* WIP: define the readiness function for the basic model without jitter and no
   self-suspensions. *)

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

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

  (* A job is ready iff it is pending. *)
  Global Instance basic_ready_instance : JobReady PState Job :=
    {
      job_ready sched j t := pending sched j t
    }.

End LiuAndLaylandReadiness.