Library prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Reduction of the serach space for Abstract RTA

In this module, we prove that in order to calculate the worst-case response time it is sufficient to consider only values of A that lie in the search space defined below.

Module AbstractRTAReduction.

  Import UniprocessorSchedule.

  Section SearchSpace.

    Context {Task: eqType}.

    Section EquivalentFunctions.

      Context {T: eqType}.

      Variables f1 f2: nat → T.

      Variable B: nat.

      Definition are_equivalent_at_values_less_than :=
        ∀ x, x < B → f1 x = f2 x.

      Definition are_not_equivalent_at_values_less_than :=
        ∃ x, x < B ∧ f1 x ≠ f2 x.

    End EquivalentFunctions.

    Variable tsk: Task.

    Variable B: time.

    Variable interference_bound_function: Task → time → time → time.

    Definition is_in_search_space A :=
      A = 0 ∨
      0 < A < B ∧ are_not_equivalent_at_values_less_than
                     (interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.

    Section ExistenceOfRepresentative.

      Variable A: time.
      Hypothesis H_A_less_than_B: A < B.

      Lemma representative_exists:
        ∃ A_sp,
          A_sp ≤ A ∧
          are_equivalent_at_values_less_than (interference_bound_function tsk A)
                                             (interference_bound_function tsk A_sp) B ∧
          is_in_search_space A_sp.

    End ExistenceOfRepresentative.

    Section FixpointSolutionForAnotherA.

      Variables A_sp F_sp: time.
      Hypothesis H_less_than: A_sp + F_sp < B.
      Hypothesis H_fixpoint: A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).

      Variable A: time.
      Hypothesis H_bounds_for_A: A_sp ≤ A ≤ A_sp + F_sp.
      Hypothesis H_equivalent:
        are_equivalent_at_values_less_than
          (interference_bound_function tsk A)
          (interference_bound_function tsk A_sp) B.

      Lemma solution_for_A_exists:
        ∃ F,
          A_sp + F_sp = A + F ∧
          F ≤ F_sp ∧
          A + F = interference_bound_function tsk A (A + F).

    End FixpointSolutionForAnotherA.

  End SearchSpace.

End AbstractRTAReduction.