Library prosa.classic.model.schedule.uni.limited.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Import Job Service UniprocessorSchedule.
Section Definitions.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable job_lock_in_service: Job → time.
Definition job_lock_in_service_positive :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
0 < job_lock_in_service j.
Definition job_lock_in_service_le_job_cost :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
job_lock_in_service j ≤ job_cost j.
Definition job_nonpreemptive_after_lock_in_service :=
∀ j t t',
arrives_in arr_seq j →
t ≤ t' →
job_lock_in_service j ≤ service sched j t →
~~ completed_by job_cost sched j t' →
scheduled_at sched j t'.
Definition proper_job_lock_in_service :=
job_lock_in_service_positive ∧
job_lock_in_service_le_job_cost ∧
job_nonpreemptive_after_lock_in_service.
Variable task_lock_in_service: Task → time.
Definition task_lock_in_service_le_task_cost tsk :=
task_lock_in_service tsk ≤ task_cost tsk.
Definition task_lock_in_service_bounds_job_lock_in_service tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_lock_in_service j ≤ task_lock_in_service tsk.
Definition proper_task_lock_in_service tsk :=
task_lock_in_service_le_task_cost tsk ∧
task_lock_in_service_bounds_job_lock_in_service tsk.
End Definitions.
Section Examples.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Section FullyPreemptiveModel.
Let job_lock_in_service (j: Job) := job_cost j.
Lemma job_nonpreemptive_after_lock_in_service_trivial:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
End FullyPreemptiveModel.
Section FullyNonPreemptiveModel.
Let job_lock_in_service (j: Job) := ε.
Hypothesis H_is_nonpreemptive_schedule:
NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
Lemma property_last_segment_is_nonpreemptive_holds:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
End FullyNonPreemptiveModel.
End Examples.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Import Job Service UniprocessorSchedule.
Section Definitions.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable job_lock_in_service: Job → time.
Definition job_lock_in_service_positive :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
0 < job_lock_in_service j.
Definition job_lock_in_service_le_job_cost :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
job_lock_in_service j ≤ job_cost j.
Definition job_nonpreemptive_after_lock_in_service :=
∀ j t t',
arrives_in arr_seq j →
t ≤ t' →
job_lock_in_service j ≤ service sched j t →
~~ completed_by job_cost sched j t' →
scheduled_at sched j t'.
Definition proper_job_lock_in_service :=
job_lock_in_service_positive ∧
job_lock_in_service_le_job_cost ∧
job_nonpreemptive_after_lock_in_service.
Variable task_lock_in_service: Task → time.
Definition task_lock_in_service_le_task_cost tsk :=
task_lock_in_service tsk ≤ task_cost tsk.
Definition task_lock_in_service_bounds_job_lock_in_service tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_lock_in_service j ≤ task_lock_in_service tsk.
Definition proper_task_lock_in_service tsk :=
task_lock_in_service_le_task_cost tsk ∧
task_lock_in_service_bounds_job_lock_in_service tsk.
End Definitions.
Section Examples.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Section FullyPreemptiveModel.
Let job_lock_in_service (j: Job) := job_cost j.
Lemma job_nonpreemptive_after_lock_in_service_trivial:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
End FullyPreemptiveModel.
Section FullyNonPreemptiveModel.
Let job_lock_in_service (j: Job) := ε.
Hypothesis H_is_nonpreemptive_schedule:
NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
Lemma property_last_segment_is_nonpreemptive_holds:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
End FullyNonPreemptiveModel.
End Examples.