Dijkstra's algorithm: Difference between revisions

=={{header|CafeOBJ}}==

<lang CafeOBJ>

"

Save this file as DijkstraRosetta.cafe.

To run the file type

CafeOBJ> in DijkstraRosetta.cafe

at the CafeOBJ command prompt.

CafeOBJ is primarily a first order specification language which can also be used as a functional programming language.

Being first order, we make no use higher order functions such as map.

Dijkstra's algorithm repeatedly chooses the nearest vertex and relaxes the edges leaving it, terminating when no more vertices are accessible from the origin.

Input

A directed positively weighted graph. The graph is represented as a list of 4tuples containing directed edges of the form (beginning, end, edgeDist,pathDist)

The tuple (start, start,0,0) means there is zero distance from start to start.

Ouput

1) a list of 4-tuples with each tuple represents a node N, its source, length of the conecting 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 cosen end node.

Note needs a bit more work to exacly match the specified Rosetta Dijkstra task.

"

-- some system settings

-- Most important is memoization (memo) which stores the value of a function instead of recomputing it each time the function is called.

full reset

set step off

set print fancy

set stats on

set verbose off

set quiet on

set memo on

-- A module defining a simple parameterized list.

mod! LIST(T :: TRIV) principal-sort List {

[Elt < List ]

op nil : -> List

op (_:_) : List List -> List {memo assoc id: nil}

op reverse_ : List -> List

op head_ : List -> Elt

var e : Elt

var l : List

eq reverse nil = nil .

eq reverse (e : l) = (reverse l) : e .

eq head e : l = e .

}

-- Main module

mod! DIJKSTRA {

-- A four tuple used to store graph and shortest distance

-- start, end, edgeDist,pathDist

pr(LIST(4TUPLE(INT,INT,INT,INT)))

-- A list of integers used to store final shortest path.

pr(LIST(INT) *{sort List -> PathList})

[List < PathList]

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

vars t t1 t2 : 4Tuple

eq inf = 500 .

eq finished = -1 .

-- Main dijkstra function

eq dijkstra startVertex graph permanent =

if (exploreNeighbours startVertex permanent graph) == << finished ; finished ; finished ; finished >> then permanent

else (dijkstra startVertex graph ( ((exploreNeighbours startVertex permanent graph) : 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 nil = << finished ; finished ; finished ; finished >> .

eq nextNode2Explore (t1 : nil) = t1 .

eq nextNode2Explore (t2 : (t1 : xs)) = if (4* t1) < (4* t2) then t1 else nextNode2Explore (t2 : xs) fi .

-- relaxes all edges leaving y

eq relax nil permanent = nil .

eq relax (<< x ; y ; eD ; pD >> : xs) permanent = if (currDist x permanent) < pD then << y ; x ; eD ; ((currDist x permanent) + eD) >> : (relax xs permanent) else << y ; x ; eD ; pD >> : (relax xs permanent) fi .

-- Get the current best distance for a particulare vertex n.

eq currDist n nil = inf .

eq currDist n (t : permanent) = if ((1* t) == n) then (4* t ) else (currDist n permanent) fi .

eq connectedTo z nil = false .

eq connectedTo z ((<< x ; y ; eD ; pD >>) : xs) = if (x == z) then true else (connectedTo z xs) 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 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 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 pList : PathList

var currentTuple : 4Tuple

vars start end : Int

eq SP start end nil = nil .

eq SP start end (currentTuple : pList) = if (end == (1* currentTuple)) then ( end : (SP start (2* currentTuple) pList)) else (SP start end pList) fi .

-- The graph to be traversed

op DirectedRosetta : -> List

eq DirectedRosetta = ( << 1 ; 2 ; 7 ; inf >> :

<< 1 ; 3 ; 9 ; inf >> :

<< 1 ; 6 ; 14 ; inf >> :

<< 2 ; 3 ; 10 ; inf >> :

<< 2 ; 4 ; 15 ; inf >> :

<< 3 ; 4 ; 11 ; inf >> :

<< 3 ; 6 ; 2 ; inf >> :

<< 4 ; 5 ; 6 ; inf >> :

<< 5 ; 6 ; 9 ; inf >>) .

-- A set of possible strating points

ops oneStart twoStart threeStart fourStart fiveStart sixStart : -> List

eq oneStart = << 1 ; 1 ; 0 ; 0 >> .

eq twoStart = << 2 ; 2 ; 0 ; 0 >> .

eq threeStart = << 3 ; 3 ; 0 ; 0 >> .

eq fourStart = << 4 ; 4 ; 0 ; 0 >> .

eq fiveStart = << 5 ; 5 ; 0 ; 0 >> .

eq sixStart = << 6 ; 6 ; 0 ; 0 >> .

} -- End module

-- We must open the module in the CafeOBJ interpreter

open DIJKSTRA .

--> All shortest distances starting from a(1)

red dijkstra 1 DirectedRosetta oneStart .

-- Gives

-- ((((<< 5 ; 4 ; 6 ; 26 >>) : (<< 4 ; 3 ; 11 ; 20 >>)) : ((<< 6 ; 3 ; 2 ; 11 >>) : (<< 3 ; 1 ; 9 ; 9 >>))) : ((<< 2 ; 1 ; 7 ; 7 >>) : (<< 1 ; 1 ; 0 ; 0 >>))):List

--> Shortest path from a(1) to e(5)

red reverse (SP 1 5 (dijkstra 1 DirectedRosetta oneStart)) .

-- Gives

-- ((1 : 3) : (4 : 5)):PathList

--> Shortest path from a(1) to f(6)

red reverse (SP 1 6 (dijkstra 1 DirectedRosetta oneStart)) .

-- Gives

-- ((1 : 3) : 6):PathList

eof

</lang>