Library rt.restructuring.model.processor.multiprocessor

From mathcomp Require Export fintype.
From rt.restructuring.behavior Require Export all.

Section Schedule.

  Variable Job: JobType.
  Variable processor_state: Type.
  Context `{ProcessorState Job processor_state}.

  Definition processor (num_cpus: nat) := 'I_num_cpus.

  Variable num_cpus : nat.

  Definition identical_state := processor num_cpus → processor_state.

End Schedule.