# Library prosa.analysis.facts.shifted_job_costs

Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.model.task.concept.
Require Export prosa.analysis.facts.hyperperiod.
In this file we define a new function for job costs in an observation interval and prove its validity.
Section ValidJobCostsShifted.
Consider any type of periodic tasks ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{PeriodicModel Task}.
Context `{TaskCost Task}.
... and any type of jobs.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Consider a consistent arrival sequence with non-duplicate arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Furthermore, assume that arrivals have valid job costs.
Hypothesis H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq.
Consider a periodic task set ts such that all tasks in ts have valid periods and offsets.
Variable ts : TaskSet Task.
Hypothesis H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts.
Hypothesis H_valid_periods_in_taskset : valid_periods ts.
Hypothesis H_valid_offsets_in_taskset : valid_offsets arr_seq ts.
Consider a job j that stems from the arrival sequence.
Variable j : Job.
Hypothesis H_j_from_arrival_sequence : arrives_in arr_seq j.
Let O_max denote the maximum task offset of all tasks in ts ...
Let O_max := max_task_offset ts.
... and let HP denote the hyperperiod of all tasks in ts.
Let HP := hyperperiod ts.
We now define a new function for job costs in the observation interval.
Given that job j arrives after O_max, the cost of a job j' that arrives in the interval `[O_max + HP, O_max + 2HP)` is defined to be the same as the job cost of its corresponding job in j's hyperperiod.
Definition job_costs_shifted (j' : Job) :=
if (job_arrival j ≥ O_max) && (O_max + HP ≤ job_arrival j' < O_max + 2 × HP) then
job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
else job_cost j'.
Assume that we have an infinite sequence of jobs.
Hypothesis H_infinite_jobs : infinite_jobs arr_seq.
Assume all jobs in the arrival sequence arr_seq belong to some task in ts.
Hypothesis H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
We assign the job costs as defined by the job_costs_shifted function.
Instance job_costs_in_oi : JobCost Job :=
{
job_cost := job_costs_shifted
}.
We show that the job_costs_shifted function is valid.
Lemma job_costs_shifted_valid : arrivals_have_valid_job_costs arr_seq.
Proof.
rewrite /arrivals_have_valid_job_costs /valid_job_cost.
intros j' ARR.
unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.
destruct (leqP O_max (job_arrival j)) as [A | B];
last by apply H_arrivals_have_valid_job_costs ⇒ //.
destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ];
last by apply H_arrivals_have_valid_job_costs ⇒ //.
destruct (leqP (O_max + 2 × HP) (job_arrival j')) as [LT | LT];
first by apply H_arrivals_have_valid_job_costs ⇒ //.
specialize (corresponding_jobs_have_same_task arr_seq ts j' j) ⇒ TSK.
rewrite -[in X in _ ≤ task_cost X]TSK.
have IN : job_task j' \in ts by apply H_jobs_from_taskset.
by apply H_arrivals_have_valid_job_costs, corresponding_job_arrives ⇒ //; lia.
Qed.
End ValidJobCostsShifted.