Project Page Index Table of Contents

# Library prosa.model.processor.supply

Require Export prosa.behavior.schedule.

# Supply

In this section, we define some useful notions about supply.
Section Supply.
Consider any kind of jobs and any kind of processor state.
Context {Job : JobType} {PState : ProcessorState Job}.
Consider any schedule.
Variable sched : schedule PState.
We define a function that retrieves the amount of supply available at a particular instant in time.
Definition supply_at (t : instant) := supply_in (sched t).
Based on the notion of instantaneous supply, we define the cumulative supply produced during an interval from t1 until (but not including) t2.
Definition supply_during (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) supply_at t.
Next, we define a predicate that checks if there is any supply at a given time instant.
Definition has_supply (t : instant) := supply_at t > 0.
We say that there is a blackout at a time instant t if there is no supply at t.
Definition is_blackout (t : instant) := ~~ has_supply t.
Similarly to supply_during, we define the cumulative duration of blackout time instants during a time interval `[t1,t2)`.
Definition blackout_during (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) is_blackout t.
End Supply.