Library prosa.model.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.all.
Liu & Layland Readiness Model
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time and a cost.
In the basic Liu & Layland model, a job is ready iff it is pending.
Global Program Instance basic_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t
}.
End LiuAndLaylandReadiness.
{
job_ready sched j t := pending sched j t
}.
End LiuAndLaylandReadiness.