Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** * The Restricted Supply Model *)

(** In the following, we define a processor state that includes the
    possibility of the processor becoming unavailable, where the jobs
    executing in the unavailable state do not progress (= don't get
    any service). We allow jobs to be scheduled in unavailable states
    in order to preserve work-conservation. *)
Section State.

  (** We define the state of a processor at a given time to be one of
      four possible cases: *)
  Inductive processor_state {Job : JobType} :=
  (** The processor is idle. We _could_ service a job, so we are
      wasting the capacity of the supply. *)
  | Idle
  (** A job is being executed. *)
  | Active (j : Job)
  (** A job is scheduled, but the processor is unavailable and yields
      no service. *)
  | Unavailable (j : Job)
  (** The processor is unavailable, and no job is being scheduled. *)
  | Inactive.

  (** Consider any type of jobs. *)
  Context (Job : JobType).

  (** Next, we define the semantics of the processor state with
      restricted supply. *)
  Section Service.

    (** Let [j] denote any job. *)
    Variable j : Job.

    (** It is scheduled in a given state [s] iff [j] is the job mentioned
        in the state. *)
    Definition rs_scheduled_on (s : processor_state) : bool :=
      match s with
      | Idle | Inactive => false
      | Active j' | Unavailable j' => j' == j
      end.

    (** Processor states [Idle] and [Active _] indicate that the
        processor is ready to produce [1] unit of supply. If the
        processor is in state [Unavailable _] or [Inactive], it
        produces [0] unit of work. *)
    Definition rs_supply_on (s : @processor_state Job) : work :=
      match s with
      | Idle | Active _ => 1
      | _ => 0
      end.

    (** Job [j] receives service only if the given state [s] is
        [Active j]. *)
    Definition rs_service_on (s : processor_state) : work :=
      if s is Active j'
      then if j' == j then 1 else 0
      else 0.

  End Service.

  (** Finally, we connect the above definitions with the generic Prosa
      interface for abstract processor states. *)
  Program Definition rs_processor_state : ProcessorState Job :=
    {|
      State                       := processor_state;
      scheduled_on j s (_ : unit) := rs_scheduled_on j s;
      supply_on s (_ : unit)      := rs_supply_on s;
      service_on j s (_ : unit)   := rs_service_on j s
    |}.
  
Job: JobType
forall (j : Job) (s : processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
(fun (j0 : Job) (s0 : processor_state) =>
 fun=> rs_service_on j0 s0) j s r <=
(fun s0 : processor_state => fun=> rs_supply_on s0) s
  r
 by move=> j s r; case s, r => //=; case: (_ == _). Qed.
  
Job: JobType
forall (j : Job) (s : processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
~~
(fun (j0 : Job) (s0 : processor_state) =>
 fun=> rs_scheduled_on j0 s0) j s r ->
(fun (j0 : Job) (s0 : processor_state) =>
 fun=> rs_service_on j0 s0) j s r = 0
 by move=> j s r; case s, r => //=; case: (_ == _). Qed.

End State.