Instance of Location for any Graph

Models/RingSSync.v

 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).
 

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.