Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
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_costs_shifted. (** We show that the [job_costs_shifted] function is valid. *)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts

arrivals_have_valid_job_costs arr_seq
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts

arrivals_have_valid_job_costs arr_seq
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts

forall j : Job, arrives_in arr_seq j -> job_cost j <= task_cost (job_task j)
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'

job_cost j' <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'

(if [&& O_max <= job_arrival j, O_max + HP <= job_arrival j' & 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') <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j

(if [&& true, O_max + HP <= job_arrival j' & 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') <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'

(if [&& true, true & 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') <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP

(if [&& true, true & true] 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') <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')) = job_task j'

(if [&& true, true & true] 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') <= task_cost (job_task j')
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')) = job_task j'

job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')) <= task_cost (job_task (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')))
Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')) = job_task j'
IN: job_task j' \in ts

job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')) <= task_cost (job_task (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j')))
by apply H_arrivals_have_valid_job_costs, corresponding_job_arrives => //; lia. Qed. End ValidJobCostsShifted.