Library prosa.analysis.facts.model.task_schedule
Require Export prosa.model.task.concept.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.scheduled.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.scheduled.
In this file we provide basic properties related to schedule of a task.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any valid arrival sequence of such jobs ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... and let sched be any corresponding uni-processor schedule.
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_uniproc : uniprocessor_model PState.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Let tsk be any task.
Lemma job_of_task_scheduled_implies_task_scheduled :
∀ j t,
job_of_task tsk j →
scheduled_at sched j t →
task_scheduled_at arr_seq sched tsk t.
Proof.
move⇒ j t TSK.
rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
by move: TSK; rewrite /job_of_task.
Qed.
∀ j t,
job_of_task tsk j →
scheduled_at sched j t →
task_scheduled_at arr_seq sched tsk t.
Proof.
move⇒ j t TSK.
rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
by move: TSK; rewrite /job_of_task.
Qed.
And vice versa, if no job of task tsk is scheduled at time
t, then task tsk is not scheduled at time t.
Lemma job_of_task_scheduled_implies_task_scheduled':
∀ j t,
~~ job_of_task tsk j →
scheduled_at sched j t →
~~ task_scheduled_at arr_seq sched tsk t.
Proof.
move ⇒ j t TSK SCHED; apply: contra; last exact: TSK.
move: SCHED; rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
by rewrite /job_of_task.
Qed.
End TaskSchedule.
∀ j t,
~~ job_of_task tsk j →
scheduled_at sched j t →
~~ task_scheduled_at arr_seq sched tsk t.
Proof.
move ⇒ j t TSK SCHED; apply: contra; last exact: TSK.
move: SCHED; rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
by rewrite /job_of_task.
Qed.
End TaskSchedule.