Merge branch 'add-exec-proc-state1' of...

Merge branch 'add-exec-proc-state1' of https://gitlab.mpi-sws.org/kbedarka/rt-proofs into add-exec-proc-state1

model/processor/ideal_uni_exceed.v

@@ -50,9 +50,8 @@ Section State.
     }
   Qed.
 
-  (** Finally, we register the processor state and an [eqType]. *)
-  HB.instance Definition _ := hasDecEq.Build exceedance_processor_state
-                                eqn_exceedance_processor_state.
+  (** Finally, we register the processor state as an [eqType]. *)
+  HB.instance Definition _ := hasDecEq.Build exceedance_processor_state eqn_exceedance_processor_state.
 
   (** Next, we need to define the notions of service and supply for the
       processor state under consideration. *)
@@ -75,24 +74,24 @@ Section State.
         This is required to specify in which states a processor can offer
         productive work to a job. Note that when analysing a schedule of the
         [exceedance_processor_state], we want to model all instances of
-        [ExceedanceExecution] as blackouts and therefore, the supply in this
+        [ExceedanceExecution] as blackouts w.r.t. to nominal service and, therefore, the supply in this
         processor state is defined to be [0]. *)
     Definition exceedance_supply_on (proc_state :  exceedance_processor_state)
       (_ : unit) : work :=
       match proc_state with
-      |NominalExecution _ => 1
-      |ExceedanceExecution _ => 0
-      |Idle => 1
+      | NominalExecution _ => 1
+      | ExceedanceExecution _ => 0
+      | Idle => 1
       end.
 
     (** Finally we need to define in which states a job actually receives
-        service. In our case, a job [j] only receives service when the system
-        is [NominalExecution j] state. *)
+        nominal service. In our case, a job [j] receives nominal service only when the system
+        is in the [NominalExecution j] state. *)
     Definition exceedance_service_on (proc_state : exceedance_processor_state) (_ : unit) : work :=
       match proc_state with
-      |NominalExecution j' => j' == j
-      |ExceedanceExecution _ => 0
-      |Idle => 0
+      | NominalExecution j' => j' == j
+      | ExceedanceExecution _ => 0
+      | Idle => 0
       end.
 
   End ExceedanceService.