Library probsa.rt.model.events
(* --------------------------------- Prosa ---------------------------------- *)
From prosa Require Export util.all.
From prosa Require Export behavior.all.
(* -------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export boolp.
From probsa.probability Require Export partition.
From probsa.rt.behavior Require Export job arrival_sequence.
(* -------------------------------- SSReflect ------------------------------- *)
From mathcomp Require Import finfun.
(* ------------------------------ Definitions ------------------------------- *)
From prosa Require Export util.all.
From prosa Require Export behavior.all.
(* -------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export boolp.
From probsa.probability Require Export partition.
From probsa.rt.behavior Require Export job arrival_sequence.
(* -------------------------------- SSReflect ------------------------------- *)
From mathcomp Require Import finfun.
(* ------------------------------ Definitions ------------------------------- *)
Fixed Arrival Sequence
Given a probability space (Ω,μ) and a job type Job, function ξ_fix returns an event E ⊆ Ω in which the arrival-sequence random variable ξ_pr is equal to some fixed (deterministic) arrival sequence ξ.
Definition ξ_fix {Ω} {μ : measure Ω} {Job : JobType}
(ξ_pr : pr_arrival_sequence μ Job) (ξ : arrival_sequence Job) : pred Ω :=
fun ω : Ω ⇒ ξ_pr ω == ξ.
(ξ_pr : pr_arrival_sequence μ Job) (ξ : arrival_sequence Job) : pred Ω :=
fun ω : Ω ⇒ ξ_pr ω == ξ.
Fixed Job Costs
Given a probability space (Ω, μ), an assignment of costs 𝗖 to jobs, and a set of jobs jobs, the term 𝓒_fix 𝗖 jobs denotes an event E ⊆ Ω where the costs of jobs in jobs agree with the assignment of 𝗖.
Definition 𝓒_fix {Ω} {μ : measure Ω} {Job : JobType} {job_cost : JobCostRV Job Ω μ}
(𝗖 : Job → option work) (jobs : seq Job) : pred Ω :=
fun ω : Ω ⇒ all (fun j : Job ⇒ compute_costs ω j == 𝗖 j) jobs.
(𝗖 : Job → option work) (jobs : seq Job) : pred Ω :=
fun ω : Ω ⇒ all (fun j : Job ⇒ compute_costs ω j == 𝗖 j) jobs.
Partitions
In addition to the aforementioned straightforward events, one can construct partitions over arrival sequences and sequences of job costs of a fixed set of jobs.Partition on Arrival Sequences
In this section, we define a construction for a partition S of a sample space on arrival sequences. Each event S◁{ξ} of the partition is an event with a fixed arrival sequence ξ.
Section ArrivalsPartition.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Program Definition partition_on_ξ : @Ω_partition Ω μ :=
{|
I := [countType of imgT arr_seq];
p := fun ξ ω ⇒ arr_seq ω == sval ξ
|}.
End ArrivalsPartition.
{|
I := [countType of imgT arr_seq];
p := fun ξ ω ⇒ arr_seq ω == sval ξ
|}.
End ArrivalsPartition.
Partition on Job Costs
In this section, we define a construction for a partition {S_i} of a sample space on (1) costs of a single job and (2) costs of a finite set of jobs.
Section CostPartition.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}.
Consider a job j. First, we define a partition S of Ω into
events where the job cost of j is fixed. We define index of
the partition as all job costs None, Some 0, Some 1, .... In
other words, an event S◁{Some 2} contains ωs such that
job_cost j ω = Some 2.
Program Definition partition_on_𝓒 (j : Job) : @Ω_partition Ω μ :=
{|
I := [countType of option nat];
p := fun (c : option work) (ω : Ω) ⇒ job_cost j ω == c
|}.
{|
I := [countType of option nat];
p := fun (c : option work) (ω : Ω) ⇒ job_cost j ω == c
|}.