Library prosa.model.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
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.