Skip to content
Snippets Groups Projects
Commit a7cf82f7 authored by Pierre Roux's avatar Pierre Roux Committed by Björn Brandenburg
Browse files

Remove var. speed processor model Global Instance

parent c1a5a957
No related branches found
No related tags found
No related merge requests found
...@@ -45,12 +45,12 @@ Section State. ...@@ -45,12 +45,12 @@ Section State.
(** Finally, we connect the above definitions to the generic Prosa interface (** Finally, we connect the above definitions to the generic Prosa interface
for processor states. *) for processor states. *)
Global Program Instance pstate_instance : ProcessorState Job := Program Definition pstate_instance : ProcessorState Job :=
{ {|
State := processor_state; State := processor_state;
scheduled_on := varspeed_scheduled_on; scheduled_on := varspeed_scheduled_on;
service_on := varspeed_service_on service_on := varspeed_service_on
}. |}.
Next Obligation. Next Obligation.
move: r H. move: r H.
case: s=>//= j' v _. case: s=>//= j' v _.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment