Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
720 commits behind the upstream repository.

Björn Brandenburg
authored
Given an interval [a, b), a function f: nat -> T, a predicate P, and a total, reflexive, transitive relation R, [search_arg f P R a b] will find the x in [a, b) that is an extremum w.r.t. R among all elements x in [a, b) for which (f x) satisfies P. For example, this can be used to search in a schedule for a scheduled job released before some reference time with the earliest deadline.