diff --git a/Models/RingSSync.v b/Models/RingSSync.v
index 1b4f6c01399d25cfc7971a80a0cd729a09c3faf2..8eec2e0fee0cfe15851cd7e83fa54518e354a4ae 100644
--- a/Models/RingSSync.v
+++ b/Models/RingSSync.v
@@ -1,6 +1,6 @@
 Require Import Utf8.
-From Pactole Require Export Setting Util.Fin Util.Bijection Spaces.Ring
-  Observations.MultisetObservation.
+From Pactole Require Export Setting Util.Fin Util.Bijection Spaces.Graph
+  Spaces.Ring Observations.MultisetObservation.
 
 Set Implicit Arguments.
 
@@ -8,7 +8,7 @@ Section RingSSync.
 
 Context {RR : RingSpec} {Robots : Names}.
 
-Global Instance Loc : Location := make_Location ring_node.
+Global Existing Instance NodesLoc.
 
 Global Instance St : State location := OnlyLocation (fun _ => True).
 
diff --git a/Spaces/Graph.v b/Spaces/Graph.v
index c72ab0201de14bc00682f9068d317ad1c2934b7b..46c1253ef78ab180a9a74352bad4cd34040a24fe 100644
--- a/Spaces/Graph.v
+++ b/Spaces/Graph.v
@@ -10,7 +10,7 @@
 
 
 Require Import Rbase SetoidDec.
-From Pactole Require Import Util.Coqlib Util.Fin.
+From Pactole Require Import Util.Coqlib Util.Fin Core.State.
 Set Implicit Arguments.
 
 
@@ -47,3 +47,6 @@ Instance finite_node_EqDec n : EqDec (finite_node_Setoid n) := @fin_dec n.
 Definition FiniteGraph (n : nat) E := Graph (finite_node n) E.
 Existing Class FiniteGraph.
 Global Identity Coercion proj_graph : FiniteGraph >-> Graph.
+
+Definition NodesLoc {V E : Type} {G : Graph V E} : Location
+  := make_Location V.