Library prosa.classic.model.schedule.uni.susp.last_execution
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module LastExecution.
Export Job UniprocessorSchedule.
Section TimeAfterLastExecution.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section Defs.
Variable j: Job.
Variable t: time.
Let scheduled_before :=
[∃ t0: 'I_t, job_scheduled_at j t0].
Let last_time_scheduled :=
\max_(t_last < t | job_scheduled_at j t_last) t_last.
Definition time_after_last_execution :=
if scheduled_before then
last_time_scheduled + 1
else job_arrival j.
End Defs.
Section Lemmas.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Section JobHasArrived.
Lemma last_execution_after_arrival:
∀ t,
has_arrived job_arrival j (time_after_last_execution j t).
End JobHasArrived.
Section Monotonicity.
Variable t1: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t1.
Lemma last_execution_monotonic:
∀ t2,
t1 ≤ t2 →
time_after_last_execution j t1 ≤ time_after_last_execution j t2.
End Monotonicity.
Section Idempotence.
Lemma last_execution_idempotent:
∀ t,
time_after_last_execution j (time_after_last_execution j t)
= time_after_last_execution j t.
End Idempotence.
Section BoundedByIdentity.
Variable t: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t.
Lemma last_execution_bounded_by_identity:
time_after_last_execution j t ≤ t.
End BoundedByIdentity.
Section SameLastExecution.
Variable t t': time.
Hypothesis H_same_service: service sched j t = service sched j t'.
Lemma same_service_implies_same_last_execution:
time_after_last_execution j t = time_after_last_execution j t'.
End SameLastExecution.
Section SameService.
Lemma same_service_since_last_execution:
∀ t,
service sched j (time_after_last_execution j t) = service sched j t.
End SameService.
Section ExistsIntermediateExecution.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Variable s: time.
Hypothesis H_less_than_cost: s < job_cost j.
Lemma exists_last_execution_with_smaller_service:
∃ t0,
service sched j (time_after_last_execution j t0) = s.
End ExistsIntermediateExecution.
Section LessServiceBeforeLastExecution.
Variable t: time.
Variable t0: time.
Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.
Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.
Lemma less_service_before_start_of_suspension:
service sched j t0 < service sched j t.
End LessServiceBeforeLastExecution.
End Lemmas.
End TimeAfterLastExecution.
End LastExecution.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module LastExecution.
Export Job UniprocessorSchedule.
Section TimeAfterLastExecution.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section Defs.
Variable j: Job.
Variable t: time.
Let scheduled_before :=
[∃ t0: 'I_t, job_scheduled_at j t0].
Let last_time_scheduled :=
\max_(t_last < t | job_scheduled_at j t_last) t_last.
Definition time_after_last_execution :=
if scheduled_before then
last_time_scheduled + 1
else job_arrival j.
End Defs.
Section Lemmas.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Section JobHasArrived.
Lemma last_execution_after_arrival:
∀ t,
has_arrived job_arrival j (time_after_last_execution j t).
End JobHasArrived.
Section Monotonicity.
Variable t1: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t1.
Lemma last_execution_monotonic:
∀ t2,
t1 ≤ t2 →
time_after_last_execution j t1 ≤ time_after_last_execution j t2.
End Monotonicity.
Section Idempotence.
Lemma last_execution_idempotent:
∀ t,
time_after_last_execution j (time_after_last_execution j t)
= time_after_last_execution j t.
End Idempotence.
Section BoundedByIdentity.
Variable t: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t.
Lemma last_execution_bounded_by_identity:
time_after_last_execution j t ≤ t.
End BoundedByIdentity.
Section SameLastExecution.
Variable t t': time.
Hypothesis H_same_service: service sched j t = service sched j t'.
Lemma same_service_implies_same_last_execution:
time_after_last_execution j t = time_after_last_execution j t'.
End SameLastExecution.
Section SameService.
Lemma same_service_since_last_execution:
∀ t,
service sched j (time_after_last_execution j t) = service sched j t.
End SameService.
Section ExistsIntermediateExecution.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Variable s: time.
Hypothesis H_less_than_cost: s < job_cost j.
Lemma exists_last_execution_with_smaller_service:
∃ t0,
service sched j (time_after_last_execution j t0) = s.
End ExistsIntermediateExecution.
Section LessServiceBeforeLastExecution.
Variable t: time.
Variable t0: time.
Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.
Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.
Lemma less_service_before_start_of_suspension:
service sched j t0 < service sched j t.
End LessServiceBeforeLastExecution.
End Lemmas.
End TimeAfterLastExecution.
End LastExecution.