structure Scheduler.State.SchedulerDatum : Type

• operator_id : OperatorId
• shift_start : PosixTime

def Scheduler.State.SchedulerDatum.init : SchedulerDatum

Equations

• Scheduler.State.SchedulerDatum.init = { operator_id := 0, shift_start := 0 }

def Scheduler.State.SchedulerDatum.shift_end (s : SchedulerDatum) (dur : PosixTime) : PosixTime

Equations

• s.shift_end dur = s.shift_start + dur

def Scheduler.State.SchedulerDatum.shift_interval (s : SchedulerDatum) (dur : PosixTime) : DefinedTimeInterval

Equations

• s.shift_interval dur = { lower := s.shift_start, upper := s.shift_end dur }

inductive Scheduler.State.Sch_Actions : Type

• Advance (next_active : Tokens.Elem.TId) : Sch_Actions
• Rewind (last_reg last_active root_active : Tokens.Elem.TId) : Sch_Actions