structure Scheduler.Computational.Environment : Type

• parameters : MidgardParameters
• operatorsDir : OperatorDirectory.State.OperatorDirectory

def Scheduler.Computational.RelationFormat (e : Environment) (t : InfoActions State.Sch_Actions) (scheduler_in : State.SchedulerDatum) : State.SchedulerDatum → Prop

Equations

• Scheduler.Computational.RelationFormat e = Scheduler.Relation e.parameters e.operatorsDir

def Scheduler.Computational.computational : ComputationalRel StateMachine.Err RelationFormat

Equations

• One or more equations did not get rendered due to their size.

def Scheduler.Computational.SchedulerMachine : StepMachines.StepMachine Environment (InfoActions State.Sch_Actions) State.SchedulerDatum

Equations

• Scheduler.Computational.SchedulerMachine = { init := Scheduler.State.SchedulerDatum.init, STS := Scheduler.Computational.RelationFormat }