Library probsa.rt.behavior.arrival_sequence
From prosa Require Export util.all.
From prosa Require Export behavior.all.
From prosa Require Export model.task.concept.
From probsa.util Require Export boolp.
From probsa.rt.behavior Require Export job.
From prosa Require Export behavior.all.
From prosa Require Export model.task.concept.
From probsa.util Require Export boolp.
From probsa.rt.behavior Require Export job.
Probabilistic Arrival Sequence
Arrival sequence is a function that maps a time instant to a sequence of jobs that arrive at this time instant. A probabilistic arrival sequence is a random variable with a codomain in arrival sequences.
Definition pr_arrival_sequence {Ω} (μ : measure Ω) (Job : JobType) : Type :=
rvar μ [eqType of {classic (arrival_sequence Job)}].
rvar μ [eqType of {classic (arrival_sequence Job)}].
job_arrival → pr_arrival_sequence for Job : Finite
If Job is a finType, one can derive a probabilistic arrival sequence from JobArrivalRV.
Section ArrSeqForFinTypeJobs.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
The set of jobs that arrive at a time instant t in a scenario
ω is simply j <- Job | job_arrival j ω = t. Note that since
the number of jobs is finite, we can just check every single job
if it arrives at time t in a scenario ω.
Due to the fact that arrival_sequence is an arrow type
(instant → seq Job), Coq cannot automatically derive the right
type. Therefore, we need to steer Coq's coercion and type
systems towards the right type via annotation B :=
Equality.clone _ _. This technicality does not change the
intuitive meaning; therefore, we do not explain it here. An
interested reader can inspect the resulting term using commands
Set Printing All and Print arr_seq.
Definition arr_seq : pr_arrival_sequence μ Job :=
mkRvar _ (B := Equality.clone _ _)
(fun ω t ⇒
[seq j <- index_enum Job |
if job_arrival j ω is Some ta
then t == ta
else false
]
).
End ArrSeqForFinTypeJobs.
Section PrArrivalsBetween.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Definition pr_arrivals_between (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ arrivals_between (ξ ω) t1 t2).
Definition pr_arrivals_task_between (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ [seq j <- pr_arrivals_between t1 t2 ω | job_of_task tsk j]).
End PrArrivalsBetween.
Section ConsistentDef.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Definition arr_seq_job_arrival_consistent :=
∀ (j : Job) (ω : Ω) (t : instant),
job_arrival j ω = Some t ↔ j \in arr_seq ω t.
End ConsistentDef.
Section ArrSeqAndJobArrivalAgree.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Local Remark cons_elim :
∀ {T} (x y : T) (xs ys : seq T),
x::xs = y::ys → x = y ∧ xs = ys.
Local Remark filter_eq_cons_sat :
∀ {T} (x : T) (xs ys : seq T) (P : pred T),
x :: xs = [seq e <- ys | P e] → P x.
Local Remark filter_cons_eq :
∀ {T} (x : T) (xs : seq T) (P1 P2 : T → bool),
[seq e <- x::xs | P1 e ] = [seq e <- x::xs | P2 e ] →
(P1 x = P2 x) ∧ [seq e <- xs | P1 e ] = [seq e <- xs | P2 e ].
Lemma eq_arr_seq_impl_eq_job_arrival :
∀ (j : Job) (ω ω' : Ω),
(∀ t, arr_seq ω t = arr_seq ω' t) →
job_arrival j ω = job_arrival j ω'.
End ArrSeqAndJobArrivalAgree.
Section ArrSeqUniq.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Lemma arr_seq_uniq :
∀ t ω, uniq (ξ t ω).
End ArrSeqUniq.
Section Consistent.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Lemma arr_seq_consistent :
arr_seq_job_arrival_consistent.
Lemma pr_consistent_arrival_times :
∀ (ω : Ω),
@consistent_arrival_times
Job
(fun j ⇒ odflt0 (job_arrival j) ω)
(arr_seq ω).
End Consistent.
Global Opaque arr_seq arrival_sequence.
mkRvar _ (B := Equality.clone _ _)
(fun ω t ⇒
[seq j <- index_enum Job |
if job_arrival j ω is Some ta
then t == ta
else false
]
).
End ArrSeqForFinTypeJobs.
Section PrArrivalsBetween.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Definition pr_arrivals_between (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ arrivals_between (ξ ω) t1 t2).
Definition pr_arrivals_task_between (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ [seq j <- pr_arrivals_between t1 t2 ω | job_of_task tsk j]).
End PrArrivalsBetween.
Section ConsistentDef.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Definition arr_seq_job_arrival_consistent :=
∀ (j : Job) (ω : Ω) (t : instant),
job_arrival j ω = Some t ↔ j \in arr_seq ω t.
End ConsistentDef.
Section ArrSeqAndJobArrivalAgree.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Local Remark cons_elim :
∀ {T} (x y : T) (xs ys : seq T),
x::xs = y::ys → x = y ∧ xs = ys.
Local Remark filter_eq_cons_sat :
∀ {T} (x : T) (xs ys : seq T) (P : pred T),
x :: xs = [seq e <- ys | P e] → P x.
Local Remark filter_cons_eq :
∀ {T} (x : T) (xs : seq T) (P1 P2 : T → bool),
[seq e <- x::xs | P1 e ] = [seq e <- x::xs | P2 e ] →
(P1 x = P2 x) ∧ [seq e <- xs | P1 e ] = [seq e <- xs | P2 e ].
Lemma eq_arr_seq_impl_eq_job_arrival :
∀ (j : Job) (ω ω' : Ω),
(∀ t, arr_seq ω t = arr_seq ω' t) →
job_arrival j ω = job_arrival j ω'.
End ArrSeqAndJobArrivalAgree.
Section ArrSeqUniq.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Lemma arr_seq_uniq :
∀ t ω, uniq (ξ t ω).
End ArrSeqUniq.
Section Consistent.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Lemma arr_seq_consistent :
arr_seq_job_arrival_consistent.
Lemma pr_consistent_arrival_times :
∀ (ω : Ω),
@consistent_arrival_times
Job
(fun j ⇒ odflt0 (job_arrival j) ω)
(arr_seq ω).
End Consistent.
Global Opaque arr_seq arrival_sequence.