# Library prosa.model.preemption.limited_preemptive

# Job Model Parameter for Preemption Points

# Preemption Model: Limited-Preemptive Jobs

Consider any type of jobs with arrival times and execution costs.

Given each job's preemption points, as determined by
job_preemptive_points, ...

...a job j is preemptable at a given point of progress ρ iff ρ is
one of the preemption points of j.

#[local] Instance limited_preemptive_job_model : JobPreemptable Job :=

{

job_preemptable (j : Job) (ρ : work) := ρ \in job_preemptive_points j

}.

{

job_preemptable (j : Job) (ρ : work) := ρ \in job_preemptive_points j

}.

## Model Validity

Consider any arrival sequence.

We require the sequence of preemption points to contain the beginning ...

Definition beginning_of_execution_in_preemption_points :=

∀ j, arrives_in arr_seq j → 0 \in job_preemptive_points j.

∀ j, arrives_in arr_seq j → 0 \in job_preemptive_points j.

Definition end_of_execution_in_preemption_points :=

∀ j, arrives_in arr_seq j → last0 (job_preemptive_points j) = job_cost j.

∀ j, arrives_in arr_seq j → last0 (job_preemptive_points j) = job_cost j.

We further require the sequence of preemption points to be a
non-decreasing sequence.

Definition preemption_points_is_nondecreasing_sequence :=

∀ j, arrives_in arr_seq j → nondecreasing_sequence (job_preemptive_points j).

∀ j, arrives_in arr_seq j → nondecreasing_sequence (job_preemptive_points j).

A job model is considered valid w.r.t. limited-preemptive preemption
model if it satisfies each of the preceding definitions.