Library prosa.model.schedule.preemption_time
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.preemption.parameter.
Preemption Times
Consider any type of jobs, ...
... any preemption model, ...
... and any ideal uniprocessor schedule of such jobs.
We say that a time [t] is a preemption time iff the job that is currently
scheduled at [t], if any, can be preempted according to the predicate
[job_preemptable] (which encodes the preemption model). An idle instant
is always a preemption time.
Definition preemption_time (t : instant) :=
if sched t is Some j then
job_preemptable j (service sched j t)
else true.
End PreemptionTime.
if sched t is Some j then
job_preemptable j (service sched j t)
else true.
End PreemptionTime.