Library prosa.model.schedule.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.all.
Nonpreemptive Schedules
Consider any type of jobs with execution costs ...
... and any kind of processor model.
We say that a given schedule is _nonpreemptive_ if every job,
once it is scheduled, remains scheduled until completion.