Library prosa.analysis.facts.periodic.max_inter_arrival


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.analysis.facts.periodic.arrival_separation.

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).
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, ...
  Remark valid_period_is_valid_max_inter_arrival_time:
     tsk, valid_period tsk positive_task_max_inter_arrival_time tsk.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 41)
  
  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

----------------------------------------------------------------------------- *)


  Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

... and show that the periodic model respects the task max inter-arrival model.
  Remark periodic_model_respects_max_inter_arrival_model:
     tsk,
      valid_period tsk
      respects_periodic_task_model arr_seq tsk
      valid_task_max_inter_arrival_time arr_seq tsk.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  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

----------------------------------------------------------------------------- *)


    Proof.
      intros tsk VALID_PERIOD PERIODIC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  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

----------------------------------------------------------------------------- *)


      split; first by apply VALID_PERIOD ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  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

----------------------------------------------------------------------------- *)


      intros j ARR TSK IND.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  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

----------------------------------------------------------------------------- *)


      specialize (PERIODIC j); feed_n 3 PERIODIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  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

----------------------------------------------------------------------------- *)


      move : PERIODIC ⇒ [j' [ARR' [IND' [TSK' ARRJ']]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 159)
  
  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'0 : Job,
    j <> j'0 /\
    arrives_in arr_seq j'0 /\
    job_task j'0 = tsk /\
    job_arrival j'0 <= job_arrival j <=
    job_arrival j'0 + task_max_inter_arrival_time tsk

----------------------------------------------------------------------------- *)


       j'; repeat split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 163)
  
  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'

subgoal 2 (ID 319) is:
 job_arrival j' <= job_arrival j <=
 job_arrival j' + task_max_inter_arrival_time tsk

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 163)
  
  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'

----------------------------------------------------------------------------- *)


case: (boolP (j == j')) ⇒ [/eqP EQ|NEQ].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 388)
  
  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'

subgoal 2 (ID 387) is:
 j <> j'

----------------------------------------------------------------------------- *)


        - have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 421)
  
  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'

subgoal 2 (ID 387) is:
 j <> j'

----------------------------------------------------------------------------- *)


          now exfalso; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 387)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 319)

subgoal 1 (ID 319) is:
 job_arrival j' <= job_arrival j <=
 job_arrival j' + task_max_inter_arrival_time tsk

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 319)
  
  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

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 319)
  
  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

----------------------------------------------------------------------------- *)


have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 712)
  
  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

----------------------------------------------------------------------------- *)


        rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 720)
  
  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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

End PeriodicTasksRespectMaxInterArrivalModel.