From c1a5a957bdf1d88e4ce5359155068e40c75086bd Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 24 Mar 2022 14:42:32 +0100
Subject: [PATCH] Remove spin processor model Global Instance
---
model/processor/spin.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/model/processor/spin.v b/model/processor/spin.v
index e3a1faad3..7bbbe392f 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -48,12 +48,12 @@ Section State.
(** Finally, we connect the above definitions with the generic Prosa
interface for abstract processor states. *)
- Global Program Instance pstate_instance : ProcessorState Job :=
- {
+ Program Definition pstate_instance : ProcessorState Job :=
+ {|
State := processor_state;
scheduled_on := spin_scheduled_on;
service_on := spin_service_on
- }.
+ |}.
Next Obligation.
move: r H.
case: s=>//= j' _.
--
GitLab