Library rt.restructuring.behavior.schedule.ideal
First let us define the notion of an ideal schedule state, as done in Prosa
so far: either a job is scheduled or the system is idle.
Section State.
Variable Job: JobType.
Definition processor_state := option Job.
Global Instance pstate_instance : ProcessorState Job (option Job) :=
{
scheduled_in j s := s == Some j;
service_in j s := s == Some j;
idle_in s := if s is None then 1 else 0
}.
Proof.
by move⇒ j [j'->|].
Defined.
End State.