; ---------- SORTS -----------------------------------------------

TYPE 
  graph = no <-> no;
  noset = no-set;
ENDTYPE


; ---------- FUNCTIONS -------------------------------------------

FUNC succ(g:graph , n:no): no-set
RETURNS ran(g/{n});

FUNC pred(g:graph, n:no) : no-set
RETURNS {p1(x) | x <- g : p2(x)==n};

FUNC reachable(g:graph, n:no) : no-set
RETURNS let (s=succ(g,n),
             g1=[* p1(x) -> p2(x) | x <- g : p2(x) notin s *]  )
       in ( {n} U s U UNION({reachable(g1,x) | x <- s}));

FUNC tclose(g:graph) : graph
RETURNS { <x,y>  |x <- dom(g),y <-ran(g): ifpath(g,x,y) };

FUNC ifpath (g:graph, ori:no, dest:no): bool
RETURNS dest in reachable(g,ori);

FUNC path(g:graph, ori:no, dest:no) : no-list
PRE  ifpath (g, ori, dest) -> 
       strcat("There is no path from ", itoa(ori)," to ",itoa(dest))
RETURNS if ori==dest 
 then <ori>
 else let ( g1= remNo(g,ori),
            x = choice({y| y<-succ(g,ori) : ifpath(g1,y,dest)}))
      in  <ori:path(g1,x,dest)>;

;for directed graphs
FUNC connectedComp(g:graph): noset-set
RETURNS 
  if (g == [* *]) then {}
  else let (y=choice(dom(g)),
            a=reachable(g,y))
       in ({a} U connectedComp(g\a));


addedgeNO(g,o,d)=g U [* o->d, d->o *];

addedgeO(g,o,d)=g U [* o->d *];

remNo(g,n)=[* p1(x) -> p2(x) | x <- g : p1(x) != n && p2(x) != n *];

mkgraph()= [* *];


; ---------- TEST -------------------------------------------

G<- mkgraph();
G<- addedgeNO(G,1,2);
G<- addedgeNO(G,1,3);
G<- addedgeNO(G,3,4);
G<- addedgeNO(G,4,5);
G<- addedgeNO(G,5,6);
G<- addedgeNO(G,8,0);
G<- addedgeNO(G,0,9);
G1 <- tclose(G);

pp(if(card(G)==14 /\ card(G1) == 45  -> 'ok ,
      else                           -> 'error));