Commit 47eb79c0 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

Trivial fix: use proper processor type in cpu_idle def

parent 7f462118
......@@ -51,7 +51,7 @@ Module Schedule.
[exists cpu, scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
Definition is_idle (cpu: processor num_cpus) (t: time) :=
sched cpu t = None.
(* The instantaneous service of job j at time t is the number of cpus
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment