Library rt.restructuring.behavior.schedule.varspeed

From rt.restructuring.behavior Require Export schedule.

Section State.

  Variable Job: JobType.

  Inductive processor_state :=
    Idle
  | Progress (j : Job) (speed : nat).

  Section Service.

    Variable j : Job.

    Definition scheduled_in (s : processor_state) : bool :=
      match s with
      | Idle ⇒ false
      | Progress j' _ ⇒ j' == j
      end.

    Definition service_in (s : processor_state) : nat :=
      match s with
      | Idle ⇒ 0
      | Progress j' s ⇒ if j' == j then s else 0
      end.

    Definition idle_in (s : processor_state) : nat := if s is Idle then 1 else 0.

  End Service.

  Global Instance pstate_instance : ProcessorState Job processor_state :=
    {
      scheduled_in := scheduled_in;
      service_in := service_in;
      idle_in := idle_in
    }.
  Proof.
      by move⇒ j []//= j' s→.
  Defined.
End State.