Library prosa.implementation.refinements.arrival_curve_prefix

Require Export prosa.implementation.refinements.arrival_curve.

In this section, we prove some properties that every valid arrival curve prefix entails.

Section ValidArrivalCurvePrefixFacts.

Consider a task set with valid arrivals ts, ...

Variable ts : seq Task.
Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.

... and a task tsk belonging to ts with positive cost and non-zero arrival bound.

  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.
  Hypothesis H_tsk_in_ts : tsk \in ts.
  Hypothesis H_positive_step : fst (head (0,0) (steps_of (get_arrival_curve_prefix tsk))) > 0.

First, we show that the arrival curve prefix of tsk is valid.

Lemma has_valid_arrival_curve_prefix_tsk :
has_valid_arrival_curve_prefix tsk.

Next, we show that each time step of the arrival curve prefix must be positive.

  Lemma steps_are_positive_if_first_step_is_positive :
    ∀ st,
      st \in get_time_steps_of_task tsk → st > 0.

Next, we show that even shifting the time steps by a positive offset, they remain positive.

  Lemma nonshifted_offsets_are_positive :
    ∀ A offs,
      A \in repeat_steps_with_offset tsk offs → A > 0.

Finally, we show that the time steps are strictly increasing.

Lemma time_steps_sorted :
sorted ltn (get_time_steps_of_task tsk).

End ValidArrivalCurvePrefixFacts.