GitLab

• File abstract_rta.v now contains generalized aRTA. The old abstract_rta.v will be renamed into ideal_abstract_rta.v
• Added a notion of a parameter in definition job_interference_is_bounded_by in file definitions.v
• Temporally removed lemma from run_to_completion_threshold, since it relies on assumptions about ideal processor

    Lemma job_completes_after_reaching_run_to_completion_threshold:
      forall t,
        job_run_to_completion_threshold j <= service sched j t ->
        completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).

• Renamed file run_to_completion_threshold.v into lower_bound_on_service.v