Skip to content
Snippets Groups Projects

Max arrivals to rbf

Merged Max arrivals to rbf
(removed):max_arrivals_to_rbf into master
1 unresolved thread
Merged Ghost User requested to merge (removed):max_arrivals_to_rbf into master
1 unresolved thread
Compare
and
6 files
+ 221
− 6
Compare changes
  • Side-by-side
  • Inline
Files
6
analysis/facts/model/rbf.v
+ 1
− 1
@@ -252,7 +252,7 @@ Section RequestBoundFunctions.
[max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
that equals 0 for the empty interval delta = 0. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Let's define some local names for clarity. *)