Library rt.restructuring.model.preemption.job.instance.preemptive
(* ----------------------------------[ 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 Premptive Model
In this section, we instantiate [job_preemptable] for the fully preemptive model.
Consider any type of jobs.
In the fully preemptive model any job can be preempted at any time.
Global Program Instance fully_preemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := true
}.
End FullyPreemptiveModel.
{
job_preemptable (j : Job) (ρ : work) := true
}.
End FullyPreemptiveModel.