Apply suggestions from code review

Co-authored-by: João Pereira <[email protected]>
mlimbeck · Nov 14, 2023 · dc6f540 · dc6f540
1 parent d1a45a2
commit dc6f540
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -25,10 +25,11 @@ type DataPlaneSpec adt {
 	}
 }
 
-// TopologySpec provides information about the entire network topology.
+// TopologySpec describes the entire network topology.
 // coreAS: IDs of the core Autonomous Systems
 // links: representation of the network topology as a graph.
-//		links[(a1,x)] == (a2,y) means that AS a1 and AS a2 share an edge via interface x and y, respectively.
+//     `links[(a1,x)] == (a2,y)` means that the interface x of AS a1 is connected
+//     to the interface y of AS a2.
 type TopologySpec adt {
 	TopologySpec_{
 		coreAS		set[IO_as]

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -71,7 +71,7 @@ pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm {
 	})
 }
 
-// helper func
+// helper function, not defined in IO spec
 ghost
 decreases
 pure func asidToKey(asid IO_as) IO_key{