Project Page Index Table of Contents

# 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.