Add missing INSTANCE FiniteSets

[Bug]

Author: lemmy

modules/Graphs.tla

@@ -2,6 +2,7 @@
 LOCAL INSTANCE Naturals
 LOCAL INSTANCE Sequences
 LOCAL INSTANCE SequencesExt
+LOCAL INSTANCE FiniteSets
 
 IsDirectedGraph(G) ==
    /\ G = [node |-> G.node, edge |-> G.edge]

tests/AllTests.tla

@@ -13,6 +13,7 @@ EXTENDS SequencesExtTests,
         FunctionsTests,
         CSVTests,
         CombinatoricsTests,
-        FoldsTests
+        FoldsTests,
+        GraphsTests
 
 ===========================================

tests/GraphsTests.tla

@@ -0,0 +1,11 @@
+------------------------- MODULE GraphsTests -------------------------
+EXTENDS Graphs, TLCExt
+
+ASSUME LET T == INSTANCE TLC IN T!PrintT("GraphsTests")
+
+ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {}]), {})
+ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {1,2,3}]), {<<1>>, <<2>>, <<3>>})
+ASSUME AssertEq(SimplePath([edge|-> {<<1,2>>, <<2,3>>}, node |-> {1,2,3}]), 
+            { <<1>>, <<2>>, <<3>>, <<1,2>>, <<2,3>>, <<1,2,3>> } )
+                
+=====================================================================