Dijkstra's algorithm: Difference between revisions

Content added Content deleted
Line 755: Line 755:


This implementation is based on suggestions from
This implementation is based on suggestions from
[https://en.wikipedia.org/w/index.php?title=Dijkstra%27s_algorithm&oldid=1117533081#Using_a_priority_queue a Wikipedia article about Dijkstra's algorithm].
[https://en.wikipedia.org/w/index.php?title=Dijkstra%27s_algorithm&oldid=1117533081#Using_a_priority_queue a Wikipedia article about Dijkstra's algorithm], although I use a different method to determine whether a queue entry is obsolete.


''Note: Currently I do not prove termination of the algorithm.''
I prove that the algorithm terminates.


<syntaxhighlight lang="ats">
<syntaxhighlight lang="ats">
Line 1,006: Line 1,006:
fn
fn
fprint_vertex_path
fprint_vertex_path
{n : int}
{n : int}
(outf : FILEref,
(outf : FILEref,
vertex_arr : arrayref (string, n),
vertex_arr : arrayref (string, n),
path : List ([i : nat | i < n] size_t i))
path : List ([i : nat | i < n] size_t i),
cost_opt : Option flt,
cost_column_no : size_t)
: void =
: void =
let
let
Line 1,015: Line 1,017:
loop {m : nat}
loop {m : nat}
.<m>.
.<m>.
(path : list ([i : nat | i < n] size_t i, m))
(path : list ([i : nat | i < n] size_t i, m),
: void =
column_no : size_t)
: size_t =
case+ path of
case+ path of
| NIL => ()
| NIL => column_no
| i :: NIL => fprint! (outf, vertex_arr[i])
| i :: NIL =>
begin
fprint! (outf, vertex_arr[i]);
column_no + strlen vertex_arr[i]
end
| i :: tail =>
| i :: tail =>
begin
begin
fprint! (outf, vertex_arr[i], " -> ");
fprint! (outf, vertex_arr[i], " -> ");
loop tail
loop (tail, column_no + strlen vertex_arr[i] + i2sz 4)
end
end


prval () = lemma_list_param path
prval () = lemma_list_param path
val column_no = loop (path, i2sz 1)
in
in
loop path
case+ cost_opt of
| None () => ()
| Some cost =>
let
var i : size_t = column_no
in
while (i < cost_column_no)
begin
fprint! (outf, " ");
i := succ i
end;
fprint! (outf, "(cost = ", cost, ")")
end
end
end


Line 1,042: Line 1,062:
source : size_t source)
source : size_t source)
(* Returns total-costs and previous-hops arrays. *)
(* Returns total-costs and previous-hops arrays. *)
:<!refwrt,!ntm> @(arrayref (flt, n),
:<!refwrt> @(arrayref (flt, n),
arrayref ([i : nat | i <= n] size_t i, n)) =
arrayref ([i : nat | i <= n] size_t i, n)) =
let
let
prval () = lemma_matrixref_param adj_matrix
prval () = lemma_matrixref_param adj_matrix
Line 1,062: Line 1,082:


val active = arrayref_make_elt<bool> (n, true)
val active = arrayref_make_elt<bool> (n, true)
var num_active : [i : nat | i <= n] size_t i = n


fun
fun
Line 1,076: Line 1,097:


fun
fun
extract_min
main_loop (pq : &pqueue_t >> _)
{m0 : nat}
:<!refwrt,!ntm> void =
if ~pqueue_is_empty pq then
.<m0>.
(pq : &pqueue_t m0 >> pqueue_t m1)
:<!refwrt> #[m1 : nat | m1 <= m0]
Option @(flt, defined_index_t) =
if pqueue_is_empty pq then
None ()
else
let
let
val @(priority, u) =
val @(priority, vertex) =
pqueue_extract_min<flt><defined_index_t> pq
pqueue_extract_min<flt><defined_index_t> pq
in
in
if ~active[vertex] then
(* Ignore any queue entries that might raise the cost. *)
if priority > cost[u] then
extract_min pq
main_loop pq
else
else
let
Some @(priority, vertex)
end
val () = active[u] := false


fun
fun
main_loop {num_active0 : nat | num_active0 <= n}
loop_over_neighbors
{v : nat | v <= n}
.<num_active0>.
.<n - v>.
(pq : &pqueue_t >> pqueue_t,
(pq : &pqueue_t >> pqueue_t,
num_active : &size_t num_active0 >> size_t num_active1)
:<!refwrt> #[num_active1 : nat | num_active1 <= num_active0]
v : size_t v)
:<!refwrt> void =
void =
if v = n then
if num_active <> i2sz 0 then
()
case+ extract_min pq of
else if ~active[v] then
| None () =>
loop_over_neighbors (pq, succ v)
(* This branch should never be reached, but the
else
corresponding sanity check is done further below. Thus
let
the proof of termination of this loop does not depend on
an exception. *)
val alternative = cost[u] + adj_matrix[u, n, v]
in
()
| Some @(priority, u) =>
if alternative < cost[v] then
begin
let
cost[v] := alternative;
val () = active[u] := false
prev[v] := u;
and () = num_active := pred num_active


fun
(* Rather than lower the priority of v, this
loop_over_neighbors
implementation inserts a new entry for v
and ignores any queue entries whose
{v : nat | v <= n}
priority exceeds cost[v]. *)
.<n - v>.
pqueue_insert<flt><defined_index_t>
(pq : &pqueue_t >> pqueue_t,
(pq, alternative, v)
v : size_t v)
end;
:<!refwrt> void =
loop_over_neighbors (pq, succ v)
if v = n then
end
()
in
else if ~active[v] then
loop_over_neighbors (pq, i2sz 0);
loop_over_neighbors (pq, succ v)
main_loop pq
else
end;
let
val alternative = cost[u] + adj_matrix[u, n, v]
end
in
if alternative < cost[v] then
begin
cost[v] := alternative;
prev[v] := u;

(* Rather than lower the priority of v, this
implementation inserts a new entry for v and
ignores obsolete queue entries. Queue entries
are obsolete if the vertex's entry in the
"active" array is false. *)

pqueue_insert<flt><defined_index_t>
(pq, alternative, v)
end;
loop_over_neighbors (pq, succ v)
end
in
loop_over_neighbors (pq, i2sz 0);
main_loop {num_active0 - 1} (pq, num_active)
end


val () = fill_pq (pq, i2sz 0)
val () = fill_pq (pq, i2sz 0)
val () = main_loop pq
val () = main_loop {n} (pq, num_active)

(* Sanity check. *)
val- true = iseqz num_active
in
in
@(cost, prev)
@(cost, prev)
Line 1,199: Line 1,249:
val- Some path_a_to_e = least_cost_path {n} (a, prev, n, e)
val- Some path_a_to_e = least_cost_path {n} (a, prev, n, e)
val- Some path_a_to_f = least_cost_path {n} (a, prev, n, f)
val- Some path_a_to_f = least_cost_path {n} (a, prev, n, f)

var u : [i : nat | i <= n] size_t i
val cost_column_no = i2sz 20
in
in
println! ("The requested paths:");
fprint_vertex_path (stdout_ref, vertex_arr, path_a_to_e);
fprint_vertex_path (stdout_ref, vertex_arr, path_a_to_e,
println! (" (cost = ", cost[e], ")");
Some cost[e], cost_column_no);
fprint_vertex_path (stdout_ref, vertex_arr, path_a_to_f);
println! (" (cost = ", cost[f], ")")
println! ();
fprint_vertex_path (stdout_ref, vertex_arr, path_a_to_f,
Some cost[f], cost_column_no);
println! ();
println! ();
println! ("All paths (in no particular order):");
for (u := i2sz 0; u <> n; u := succ u)
case+ least_cost_path {n} (a, prev, n, u) of
| None () =>
println! ("There is no path from ", vertex_arr[a], " to ",
vertex_arr[u], ".")
| Some path =>
begin
fprint_vertex_path (stdout_ref, vertex_arr, path,
Some cost[u], cost_column_no);
println! ()
end
end
end


Line 1,211: Line 1,280:
{{out}}
{{out}}
<pre>$ patscc -DATS_MEMALLOC_GCBDW dijkstra-algorithm.dats -lgc && ./a.out
<pre>$ patscc -DATS_MEMALLOC_GCBDW dijkstra-algorithm.dats -lgc && ./a.out
The requested paths:
a -> c -> d -> e (cost = 26.000000)
a -> c -> f (cost = 11.000000)</pre>
a -> c -> d -> e (cost = 26.000000)
a -> c -> f (cost = 11.000000)

All paths (in no particular order):
a -> c -> d -> e (cost = 26.000000)
a -> c -> d (cost = 20.000000)
a -> c -> f (cost = 11.000000)
a -> c (cost = 9.000000)
a -> b (cost = 7.000000)
a (cost = 0.000000)
</pre>


=={{header|AutoHotkey}}==
=={{header|AutoHotkey}}==
Retrieved from "https://rosettacode.org/wiki/Dijkstra%27s_algorithm"