graph.led

/---
Node:= Nat
Arc:= Nat*Nat

Graph := fSet(Node)*fSet(Arc)

vertices:Graph -> fSet(Node)
vertices(G) := G[1]

edges: Graph -> fSet(Arc)
edges(G) := G[2]
-------/

Vertices x and y are adjacent in G if some edge of G as one of the two as a source and the other as a destination.

/------
adjacent: Node*Node*Graph -> Bool
adjacent(x,y,G) iff (x,y) in edges(G) or (y,x) in edges(G)
-------/



If S is a set of vertices of graph G, frontier(S,G) is the set of all nodes in G that are adjacent in G to some member of S.

/------------------------------------------------------
frontier: fSet(Node)*Graph->fSet(Node)

frontier(S,G):=
  {x | x in vertices(G) & ( x in S or some y in S.adjacent(x,y,G))} 
-------------------------------------------------------/


If S is a nonempty set of nodes of graph G, reachable(S) is the set of vertices of G reachable from S by undirected paths.

/---------------------------------------
reachable:fSet(Node)*Graph -> fSet(Node)

reachable(S,G):=
  S                         if S = frontier(S,G);
  reachable(S U frontier(S,G),G) otherwise 
-----------------------------------------/

/--------------------------------------------
connected: Graph -> Bool
connected(G) iff 
  vertices(G) = {} or
  some x in vertices(G). reachable({x},G)=vertices(G)
-------------------------------------------/

Test cases

connected graph example
/---cg:=({1,2,3,4},{(1,2),(1,3),(2,4)})
----/
unconnected graph example
/---
ug:=({1,2,3,4},{(1,2),(1,3)})
---/