Library prosa.model.readiness.sequential
Sequential Readiness Model
Consider any type of job associated with any type of tasks...
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
... and any kind of processor state.
Consider any job arrival sequence ...
Variable arr_seq : arrival_sequence Job.
(* A job j is ready at a time instant t iff all jobs from task
job_task j that arrived earlier than job j are already
completed by time t. *)
Global Program Instance sequential_ready_instance : JobReady Job PState :=
{
job_ready sched j t :=
pending sched j t &&
prior_jobs_complete arr_seq sched j t
}.
Next Obligation.
by move: H3 ⇒ /andP [T _].
Defined.
End SequentialTasksReadiness.
(* A job j is ready at a time instant t iff all jobs from task
job_task j that arrived earlier than job j are already
completed by time t. *)
Global Program Instance sequential_ready_instance : JobReady Job PState :=
{
job_ready sched j t :=
pending sched j t &&
prior_jobs_complete arr_seq sched j t
}.
Next Obligation.
by move: H3 ⇒ /andP [T _].
Defined.
End SequentialTasksReadiness.