Dijkstra's algorithm: Difference between revisions

Line 1,498:
 
Ouput
1) a list of 4-tuples with each tuple represents a node N, its source, length of the conectingconnecting edge to N, and the shortest distance from the some starting node to N .
2) a list of nodes on the shortest path from a chosen start to some cosenchosen end node.
 
Note needs a bit more work to exaclyexactly match the specified Rosetta Dijkstra task.
"
 
Line 1,531:
-- Main module
mod! DIJKSTRA {
-- We use two different list notations, one for esges the other for paths.
-- A four tuple used to store graph and shortest distance
-- start, end, edgeDist,pathDist
pr(LIST(4TUPLE(INT,INT,INT,INT)))
-- AEdgeList list: ofA integersfour tuple used to store finalgraph and paths and shortest path.distance
-- start, end, edgeDist,pathDist
pr(LIST(INT) *{sort List -> PathList})
pr(LIST(4TUPLE(CHARACTER,CHARACTER,INT,INT)) *{sort List -> EdgeList, op (_:_) -> (_:e_), op nil -> nilE})
-- PathList : A fourlist tupleof integers used to store graph andfinal shortest distancepath.
[List < PathList]
pr(LIST(INTCHARACTER) *{sort List -> PathList, op (_:_) -> (_:p_), op nil -> nilP})
op dijkstra___ : Int List List -> List
op exploreNeighbours___ : Int List List -> 4Tuple {memo}
ops inf finished : -> Int
op currDist__ : Int List -> Int
op relax__ : List List -> List
op connectedTo__ : Int List -> Bool
op nextNode2Explore_ : List -> 4Tuple
op connectedList___ : List Int List -> List
op unvisitedList__ : List List -> List
op shortestPath__ : Int List -> PathList
op SP___ : 4Tuple 4Tuple List -> PathList
op shortestDist__ : Int List -> Int
op SD____ : Int Int List List -> Int
 
 
vars x y z n eD pD eD1 pD1 eD2 pD2 source currentVertex startVertex : Int
 
vars graph permanent xs : List
op dijkstra___ : IntCharacter ListEdgeList ListEdgeList -> ListEdgeList
op exploreNeighbours___ : IntCharacter ListEdgeList ListEdgeList -> 4Tuple {memo}
ops inf finishedfinishedI : -> Int
op finishedC : -> Character
op currDist__ : IntCharacter ListEdgeList -> Int
op relax__ : ListEdgeList ListEdgeList -> ListEdgeList
op connectedTo__ : IntCharacter ListEdgeList -> Bool
op nextNode2Explore_ : ListEdgeList -> 4Tuple
op connectedList___ : ListEdgeList IntCharacter ListEdgeList -> ListEdgeList
op unvisitedList__ : ListEdgeList ListEdgeList -> ListEdgeList
op shortestPath__ : Int ListEdgeList -> PathList
op SP___ : 4TupleCharacter 4TupleCharacter ListEdgeList -> PathList
 
 
vars x y z n eD pD eD1 pD1 eD2 pD2 source currentVertex startVertex : Int
vars graph permanent xs : ListEdgeList
vars t t1 t2 : 4Tuple
vars s f z startVertex currentVertex : Character
 
eq inf = 500 .
eq finishedfinishedI = -1 .
eq finishedC = 'X' .
 
-- Main dijkstra function
eq dijkstra startVertex graph permanent =
if (exploreNeighbours startVertex permanent graph) == << finishedfinishedC ; finishedfinishedC ; finishedfinishedI ; finishedfinishedI >> then permanent
else (dijkstra startVertex graph ( ((exploreNeighbours startVertex permanent graph) :e permanent))) fi .
 
eq exploreNeighbours startVertex permanent graph = (nextNode2Explore
(relax (unvisitedList (connectedList graph startVertex permanent) permanent) permanent )) .
 
 
 
-- nextNode2Explore takes a list of records and returns a record with the minimum 4th element else finished
eq nextNode2Explore nilnilE = << finishedfinishedC ; finishedfinishedC ; finishedfinishedI ; finishedfinishedI >> .
eq nextNode2Explore (t1 :e nilnilE) = t1 .
eq nextNode2Explore (t2 :e (t1 :e xs)) = if (4* t1) < (4* t2) then t1 else nextNode2Explore (t2 :e xs) fi .
 
-- relaxes all edges leaving y
eq relax nilnilE permanent = nilnilE .
eq relax (<< xs ; yf ; eD ; pD >> :e xs) permanent = if (currDist xs permanent) < pD then << y ; x ; eD ; ((currDist x permanent) + eD) >> : (relax xs permanent) else << y ; x ; eD ; pD >> : (relax xs permanent) fi .
<< f ; s ; eD ; ((tcurrDist s permanent) + eD) >> :e (connectedListrelax graph sourcexs permanent)) else
else (connectedList graph<< sourcef ; s ; eD ; pD >> :e (relax xs permanent) fi .
 
 
-- Get the current best distance for a particulareparticular vertex ns.
eq currDist ns nilnilE = inf .
eq currDist ns (t :e permanent) = if ((1* t) == ns) then (4* t ) else (currDist ns permanent) fi .
 
 
eq connectedTo z nilnilE = false .
eq connectedTo z ((<< xs ; yf ; eD ; pD >>) :e xs) = if (xs == z) then true else (connectedTo z xs) fi .
 
eq connectedList nilnilE sources permanent = nilnilE .
eq connectedList (t :e graph) sources permanent = if (connectedTo sources permanent) then
(t :e (connectedList graph s permanent))
else (connectedList graph s permanent) fi .
 
eq connectedList nil source permanent = nil .
eq connectedList (t : graph) source permanent = if (connectedTo source permanent) then
(t : (connectedList graph source permanent))
else (connectedList graph source permanent) fi .
 
eq unvisitedList nilnilE permanent = nilnilE .
eq unvisitedList (t :e graph) permanent = if not(connectedTo (2* t) permanent) then (t :e (unvisitedList graph permanent)) else (unvisitedList graph permanent) fi .
 
eq unvisitedList nil permanent = nil .
eq unvisitedList (t : graph) permanent = if not(connectedTo (2* t) permanent) then (t : (unvisitedList graph permanent)) else (unvisitedList graph permanent) fi .
 
 
-- To get the shortest path from a start node to some end node we used the above dijkstra function.
-- From a given start to a given end we need to trace the path from the finish to the start and then reverse the output.
var pListeList : PathListEdgeList
varvars currentTuple : 4Tuple
vars start end : Int Character
eq SP start end nilnilE = nilnilP .
eq SP start end (currentTuple :e pListeList) = if (end == (1* currentTuple)) then ( end :p (SP start (2* currentTuple) pListeList)) else (SP start end pListeList) fi .
 
 
-- The graph to be traversed
op DirectedRosetta : -> ListEdgeList
eq DirectedRosetta = ( << 1 'a' ; 2 'b' ; 7 ; inf >> :e
<< 1 'a' ; 3 'c' ; 9 ; inf >> :e
<< 1 'a' ; 6'f' ; 14 ; inf >> :e
<< 2 'b' ; 3'c' ; 10 ; inf >> :e
<< 2 'b' ; 4 'd' ; 15 ; inf >> :e
<< 3 'c' ; 4'd' ; 11 ; inf >> :e
<< 3 'c' ; 6'f' ; 2 ; inf >> :e
<< 4 'd' ; 5'e' ; 6 ; inf >> :e
<< 5 'e' ; 6'f' ; 9 ; inf >>) .
 
-- A set of possible stratingstarting points
ops oneStart twoStart threeStart fourStart fiveStart sixStart : -> List4Tuple
eq oneStart = << 1 'a' ; 1 'a' ; 0 ; 0 >> .
eq twoStart = << 2'b' ; 2'b' ; 0 ; 0 >> .
eq threeStart = << 3 'c' ; 3 'c' ; 0 ; 0 >> .
eq fourStart = << 4'd' ; 4'd' ; 0 ; 0 >> .
eq fiveStart = << 5 'e' ; 5 'e' ; 0 ; 0 >> .
eq sixStart = << 6'f' ; 6'f' ; 0 ; 0 >> .
 
} -- End module
Line 1,634 ⟶ 1,644:
open DIJKSTRA .
--> All shortest distances starting from a(1)
red dijkstra 1'a' DirectedRosetta oneStart .
-- Gives, where :e is the edge list separator
-- Gives
-- ((((<< 5'e' ; 4'd' ; 6 ; 26 >>) :e (<< 4'd' ; 3'c' ; 11 ; 20 >>)) :e ((<< 6'f' ; 3'c' ; 2 ; 11 >>) :e (<< 3'c' ; 1'a' ; 9 ; 9 >>))) :e ((<< 2'b' ; 1'a' ; 7 ; 7 >>) :e (<< 1'a' ; 1'a' ; 0 ; 0 >>))) :ListEdgeList
 
--> Shortest path from a(1) to e(5)
red reverse (SP 1'a' 5'e' (dijkstra 1'a' DirectedRosetta oneStart)) .
-- Gives, where :p is the path list separator
-- Gives
-- ((1'a' :p 3)'c' :p (4'd' :p 'e' 5)):PathList
 
--> Shortest path from a(1) to f(6)
red reverse (SP 1'a' 6'f' (dijkstra 1'a' DirectedRosetta oneStart)) .
-- Gives, where :p is the path list separator
-- Gives
-- ((1'a' :p 3)'c' :p 6)'f':PathList
eof
</lang>
101

edits