Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
(** ** Periodic Task Model respects the Task Max Inter-Arrival model. *) (** In this section, we show that the periodic task model respects the task max inter-arrival model (i.e. consecutive jobs of a task are separated at most by a certain duration specified by the [task_max_inter_arrival_time] parameter). *) Section PeriodicTasksRespectMaxInterArrivalModel. (** Consider any type of periodic tasks, ... *) Context {Task : TaskType} `{PeriodicModel Task}. (** ... any type of jobs associated with the tasks, ... *) Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}. (** ... and any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** By using each task's period as its maximum inter-arrival time, ... *) Global Instance max_inter_eq_period : TaskMaxInterArrival Task := { task_max_inter_arrival_time := task_period }. (** ... we observe that for any task [tsk], [task_max_inter_arrival_time tsk] is positive, ... *)
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job

forall tsk : Task, valid_period tsk -> positive_task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job

forall tsk : Task, valid_period tsk -> positive_task_max_inter_arrival_time tsk
trivial. Qed. (** ... and show that the periodic model respects the task max inter-arrival model. *)
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job

forall tsk : Task, valid_period tsk -> respects_periodic_task_model arr_seq tsk -> valid_task_max_inter_arrival_time arr_seq tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job

forall tsk : Task, valid_period tsk -> respects_periodic_task_model arr_seq tsk -> valid_task_max_inter_arrival_time arr_seq tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk

valid_task_max_inter_arrival_time arr_seq tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk

arr_sep_task_max_inter_arrival arr_seq tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j

exists j' : Job, j <> j' /\ arrives_in arr_seq j' /\ job_task j' = tsk /\ job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
PERIODIC: exists j' : Job, arrives_in arr_seq j' /\ job_index arr_seq j' = job_index arr_seq j - 1 /\ job_task j' = tsk /\ job_arrival j = job_arrival j' + task_period tsk
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j

exists j' : Job, j <> j' /\ arrives_in arr_seq j' /\ job_task j' = tsk /\ job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk

exists j' : Job, j <> j' /\ arrives_in arr_seq j' /\ job_task j' = tsk /\ job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
EQ: j = j'

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
EQ: j = j'

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
EQ: j = j'
EQ_IND: job_index arr_seq j' = job_index arr_seq j

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NEQ: j != j'

j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NEQ: j != j'

j <> j'
now apply /eqP.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk

job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk

job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD: 0 < task_period tsk

job_arrival j' <= job_arrival j <= job_arrival j' + task_max_inter_arrival_time tsk
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j = job_arrival j' + task_period tsk
NZ_PERIOD: 0 < task_period tsk

job_arrival j' <= job_arrival j' + task_period tsk <= job_arrival j' + task_period tsk
now lia. } Qed. End PeriodicTasksRespectMaxInterArrivalModel.