Library prosa.classic.model.arrival.jitter.arrival_sequence
Require Import prosa.classic.util.all prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* In this file we provide extra definitions for job arrival sequences with jitter. *)
Module ArrivalSequenceWithJitter.
Export ArrivalSequence.
(* First, we identify the actual arrival time of a job. *)
Section ActualArrival.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
(* Let j be any job. *)
Variable j: Job.
(* We define the actual arrival of job j as the time when the jitter ends. *)
Definition actual_arrival := job_arrival j + job_jitter j.
(* Next, we state whether the actual arrival of job j occurs in some interval 0, t, ... *)
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
(* ...along with the variants for interval 0, t), ... *)
Definition actual_arrival_before (t: time) := actual_arrival < t.
(* ...and interval t1, t2). *)
Definition actual_arrival_between (t1 t2: time) :=
t1 ≤ actual_arrival < t2.
End ActualArrival.
(* In this section, we show how to compute the list of arriving jobs. *)
Section ArrivingJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Let actual_job_arrival_before := actual_arrival_before job_arrival job_jitter.
Let arrivals_before := jobs_arrived_before arr_seq.
(* First, we define the actual job arrivals in the interval t1, t2). *)
Definition actual_arrivals_between (t1 t2: time) :=
[seq j <- arrivals_before t2 | t1 ≤ actual_job_arrival j < t2].
(* Similarly, we define the actual job arrivals up to time t... *)
Definition actual_arrivals_up_to (t: time) := actual_arrivals_between 0 t.+1.
(* ...and the actual job arrivals strictly before time t. *)
Definition actual_arrivals_before (t: time) := actual_arrivals_between 0 t.
(* In this section, we prove some lemmas about the arrival sequence prefixes. *)
Section Lemmas.
(* Assume that job arrival times are consistent. *)
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
(* We begin with basic lemmas for manipulating the sequences. *)
Section Basic.
(* First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma actual_arrivals_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in actual_arrivals_between t1 t2 =
(j \in actual_arrivals_between t1 t ++ actual_arrivals_between t t2).
Lemma actual_arrivals_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in actual_arrivals_between t1 t2 →
j \in actual_arrivals_between t1' t2'.
End Basic.
(* Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
(* First, we prove that if a job belongs to the prefix (actual_arrivals_before t),
then it arrives in the arrival sequence. *)
Lemma in_actual_arrivals_between_implies_arrived:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
arrives_in arr_seq j.
Lemma in_actual_arrivals_before_implies_arrived:
∀ j t,
j \in actual_arrivals_before t →
arrives_in arr_seq j.
(* Next, we prove that if a job belongs to the prefix (actual_arrivals_before t),
then its actual job arrival occured before t. *)
Lemma in_actual_arrivals_implies_arrived_before:
∀ j t,
j \in actual_arrivals_before t →
actual_job_arrival_before j t.
(* We also prove that if a job belongs to the prefix (actual_arrivals_between t1 t2),
then its actual job arrival occured between t1 and t2. *)
Lemma in_actual_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
actual_job_arrival_between j t1 t2.
(* Similarly, we prove that if a job from the arrival sequence has actual arrival
before time t, then it belongs to the sequence (actual_arrivals_before t). *)
Lemma arrived_between_implies_in_actual_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
actual_job_arrival_between j t1 t2 →
j \in actual_arrivals_between t1 t2.
(* Next, we prove that if the arrival sequence doesn't contain duplicate jobs,
the same applies for any of its prefixes. *)
Lemma actual_arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (actual_arrivals_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivingJobs.
End ArrivalSequenceWithJitter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* In this file we provide extra definitions for job arrival sequences with jitter. *)
Module ArrivalSequenceWithJitter.
Export ArrivalSequence.
(* First, we identify the actual arrival time of a job. *)
Section ActualArrival.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
(* Let j be any job. *)
Variable j: Job.
(* We define the actual arrival of job j as the time when the jitter ends. *)
Definition actual_arrival := job_arrival j + job_jitter j.
(* Next, we state whether the actual arrival of job j occurs in some interval 0, t, ... *)
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
(* ...along with the variants for interval 0, t), ... *)
Definition actual_arrival_before (t: time) := actual_arrival < t.
(* ...and interval t1, t2). *)
Definition actual_arrival_between (t1 t2: time) :=
t1 ≤ actual_arrival < t2.
End ActualArrival.
(* In this section, we show how to compute the list of arriving jobs. *)
Section ArrivingJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Let actual_job_arrival_before := actual_arrival_before job_arrival job_jitter.
Let arrivals_before := jobs_arrived_before arr_seq.
(* First, we define the actual job arrivals in the interval t1, t2). *)
Definition actual_arrivals_between (t1 t2: time) :=
[seq j <- arrivals_before t2 | t1 ≤ actual_job_arrival j < t2].
(* Similarly, we define the actual job arrivals up to time t... *)
Definition actual_arrivals_up_to (t: time) := actual_arrivals_between 0 t.+1.
(* ...and the actual job arrivals strictly before time t. *)
Definition actual_arrivals_before (t: time) := actual_arrivals_between 0 t.
(* In this section, we prove some lemmas about the arrival sequence prefixes. *)
Section Lemmas.
(* Assume that job arrival times are consistent. *)
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
(* We begin with basic lemmas for manipulating the sequences. *)
Section Basic.
(* First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma actual_arrivals_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in actual_arrivals_between t1 t2 =
(j \in actual_arrivals_between t1 t ++ actual_arrivals_between t t2).
Lemma actual_arrivals_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in actual_arrivals_between t1 t2 →
j \in actual_arrivals_between t1' t2'.
End Basic.
(* Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
(* First, we prove that if a job belongs to the prefix (actual_arrivals_before t),
then it arrives in the arrival sequence. *)
Lemma in_actual_arrivals_between_implies_arrived:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
arrives_in arr_seq j.
Lemma in_actual_arrivals_before_implies_arrived:
∀ j t,
j \in actual_arrivals_before t →
arrives_in arr_seq j.
(* Next, we prove that if a job belongs to the prefix (actual_arrivals_before t),
then its actual job arrival occured before t. *)
Lemma in_actual_arrivals_implies_arrived_before:
∀ j t,
j \in actual_arrivals_before t →
actual_job_arrival_before j t.
(* We also prove that if a job belongs to the prefix (actual_arrivals_between t1 t2),
then its actual job arrival occured between t1 and t2. *)
Lemma in_actual_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
actual_job_arrival_between j t1 t2.
(* Similarly, we prove that if a job from the arrival sequence has actual arrival
before time t, then it belongs to the sequence (actual_arrivals_before t). *)
Lemma arrived_between_implies_in_actual_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
actual_job_arrival_between j t1 t2 →
j \in actual_arrivals_between t1 t2.
(* Next, we prove that if the arrival sequence doesn't contain duplicate jobs,
the same applies for any of its prefixes. *)
Lemma actual_arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (actual_arrivals_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivingJobs.
End ArrivalSequenceWithJitter.