Library rt.restructuring.model.preemption.job.instance.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model.preemption Require Import job.parameters.
Platform for Fully Non-Preemptive Model
In this section, we instantiate [job_preemptable] for the fully non-preemptive model.
Consider any type of jobs.
We say that the model is fully non-preemptive iff no job
can be preempted until its completion.
Global Instance fully_nonpreemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0) || (ρ == job_cost j)
}.
End FullyNonPreemptiveModel.
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0) || (ρ == job_cost j)
}.
End FullyNonPreemptiveModel.