Library prosa.model.preemption.fully_preemptive
Preemption Model: Fully Preemptive Jobs
In this section, we instantiate job_preemptable for the fully preemptive model, wherein any job may be preempted at any time. This matches the classic Liu & Layland model.
Consider any type of jobs.
In the fully preemptive model, any job can be preempted at any time.
#[local] Instance fully_preemptive_job_model : JobPreemptable Job :=
{
job_preemptable (_ : Job) (_ : work) := true
}.
End FullyPreemptiveModel.
{
job_preemptable (_ : Job) (_ : work) := true
}.
End FullyPreemptiveModel.