Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** In the following, we define a model of processors with variable execution speeds. NB: For now, the definition serves only to document how this can be done; it is not actually used anywhere in the library. *) Section State. (** Consider any type of jobs. *) Variable Job: JobType. (** We define the state of a variable-speed processor at a given time to be one of two possible cases: either a specific job is scheduled and progresses with a specific speed, or the processor is idle. *) Inductive processor_state := Idle | Progress (j : Job) (speed : nat). (** Next, we define the semantics of the variable-speed processor state. *) Section Service. (** Consider any job [j]. *) Variable j : Job. (** Job [j] is scheduled in a given state [s] if [s] is not idle and [j] matches the job recorded in [s]. *) Definition varspeed_scheduled_on (s : processor_state) (_ : unit) : bool := match s with | Idle => false | Progress j' _ => j' == j end. (** If it is scheduled in state [s], job [j] receives service proportional to the speed recorded in the state. *) Definition varspeed_service_on (s : processor_state) (_ : unit) : work := match s with | Idle => 0 | Progress j' speed => if j' == j then speed else 0 end. End Service. (** Finally, we connect the above definitions to the generic Prosa interface for processor states. *) Program Definition pstate_instance : ProcessorState Job := {| State := processor_state; scheduled_on := varspeed_scheduled_on; service_on := varspeed_service_on |}.
Job: JobType
j: Job
s: processor_state
r: unit
H: ~~ varspeed_scheduled_on j s r

varspeed_service_on j s r = 0
Job: JobType
j: Job
s: processor_state

forall r : unit, ~~ varspeed_scheduled_on j s r -> varspeed_service_on j s r = 0
Job: JobType
j, j': Job
v: nat

j' != j -> (if j' == j then v else 0) = 0
by case: ifP. Qed. End State.