fact: Definition SchedulerSpec : ADT _ := Def ADT { rep := QueryStructure SchedulerSchema, Def Constructor0 "Init" : rep := empty,, Def Method3 "Spawn" (r : rep) (new_pid cpu state : W) : rep * bool := Insert (<"pid" :: new_pid, "state" :: state, "cpu" :: cpu> : RawTuple) into r!"Processes", Def Method1 "Enumerate" (r : rep) (state : State) : rep * list W := procs <- For (p in r!"Processes") Where (p!"state" = state) Return (p!"pid"); ret (r, procs), Def Method1 "GetCPUTime" (r : rep) (id : W) : rep * list W := proc <- For (p in r!"Processes") Where (p!"pid" = id) Return (p!"cpu"); ret (r, proc) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory