Library prosa.analysis.definitions.sbf.sbf

Require Export prosa.behavior.job.

Supply Bound Functions (SBF)

In this module, we define the notion of Supply Bound Functions (SBF), which can be used to reason about the minimum amount of supply provided in a given time interval.
Class SupplyBoundFunction :=
  { supply_bound_function : duration → work }.
Coercion supply_bound_function : SupplyBoundFunction >-> Funclass.