module INFO (SIZE, FIFO) is

-------------------------------------------------------------------------------

function exists_idle (fifo: Fifo, info: Info_Array): Bool is
   require fifo != {};
   var extension: Extension, i: Nat in
      extension := head (fifo).extension;
      i := 0;
      while i < N loop
         if (info[i].state == idle) and
            compatible (extension, info[i].extension)
         then
            return true
         end if;
         i := i + 1
      end loop;
      return false
   end var
end function

-------------------------------------------------------------------------------

function exists_scheduled_master (info: Info_Array): Bool is
   var i: Nat in
      i := 0;
      while i < N loop
         if info[i].state == scheduled_master then
            return true
         end if;
         i := i + 1
      end loop;
      return false
   end var
end function

-------------------------------------------------------------------------------

function find_idle (extension: Extension, info: Info_Array): Pid is
   var i: Nat in
      i := 0;
      while i < N loop
         if (info[i].state == idle) and
            compatible (extension, info[i].extension)
         then
            return Pid (i)
         end if;
         i := i + 1
      end loop;
      -- this point of the code is never reached
      return Pid (i)
   end var
end function

-------------------------------------------------------------------------------

function find_max_master (info: Info_Array, out var maxc: Int): Pid is
   var pe: Pid, i: Nat, c: Int in
      pe := Pid (0);
      maxc := 0;
      for i := 0 while i < N by i := i + 1 loop
         if info[i].state == scheduled_master then
            c := get_stack_frame (info, Pid (i), info[i].sp).count;
            if c > maxc then
               maxc := c;
               pe := Pid (i)
            end if
         end if
      end loop;
      return pe
   end var
end function

-------------------------------------------------------------------------------

function reset_status (in out info: Info_Array, id: Pid) is
   info[Nat (id)] := info[Nat (id)].{state -> idle,
                                     stack -> job_stack (none),
                                     sp -> 0}
end function

-------------------------------------------------------------------------------

function set_state (in out info: Info_Array, id: Pid, state: State) is
   info[Nat (id)] := info[Nat (id)].{state -> state}
end function

-------------------------------------------------------------------------------

function set_stack (in out info: Info_Array, id: Pid, stack: Job_Stack) is
   info[Nat (id)] := info[Nat (id)].{stack -> stack}
end function

-------------------------------------------------------------------------------

function set_stack_pointer (in out info: Info_Array, id: Pid, sp: Nat) is
   info[Nat (id)] := info[Nat (id)].{sp -> sp}
end function

-------------------------------------------------------------------------------

function get_stack_frame (info: Info_Array, id: Pid, sp: Nat): Job is
   var stack: Job_Stack in
      stack := info[Nat (id)].stack;
      return stack[sp]
   end var
end function

-------------------------------------------------------------------------------

function set_stack_frame (in out info: Info_Array, id: Pid, sp: Nat, job: Job) is
   var stack: Job_Stack in
      stack := info[Nat (id)].stack;
      stack[sp] := job;
      info[Nat (id)] := info[Nat (id)].{stack -> stack}
   end var
end function

-------------------------------------------------------------------------------

end module