Dijkstra's algorithm: Difference between revisions
→{{header|ATS}}
Line 755:
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], although I use a different method to determine whether a queue entry is obsolete.
<syntaxhighlight lang="ats">
Line 1,006:
fn
fprint_vertex_path
{n : int}
(outf : FILEref,
vertex_arr : arrayref (string, n),
path : List ([i : nat | i < n] size_t i)
cost_opt : Option flt,
cost_column_no : size_t)
: void =
let
Line 1,015 ⟶ 1,017:
loop {m : nat}
.<m>.
(path : list ([i : nat | i < n] size_t i, m)
: size_t =
case+ path of
| NIL =>
| i :: NIL =>
begin
fprint! (outf, vertex_arr[i]);
column_no + strlen vertex_arr[i]
end
| i :: tail =>
begin
fprint! (outf, vertex_arr[i], " -> ");
loop (tail, column_no + strlen vertex_arr[i] + i2sz 4)
end
prval () = lemma_list_param path
val column_no = loop (path, i2sz 1)
in
| 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
Line 1,042 ⟶ 1,062:
source : size_t source)
(* Returns total-costs and previous-hops arrays. *)
:<!refwrt
let
prval () = lemma_matrixref_param adj_matrix
Line 1,062 ⟶ 1,082:
val active = arrayref_make_elt<bool> (n, true)
var num_active : [i : nat | i <= n] size_t i = n
fun
Line 1,076 ⟶ 1,097:
fun
extract_min
{m0 : nat}
(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
val @(priority,
pqueue_extract_min<flt><defined_index_t> pq
in
if ~active[vertex] then
else
end
main_loop {num_active0 : nat | num_active0 <= n}
(pq :
:<!refwrt> #[num_active1 : nat | num_active1 <= num_active0]
if num_active <> i2sz
case+ extract_min pq
| None ()
(* This branch should never be
corresponding sanity check
the proof of termination of
an exception. *)
| Some @(priority, u) =>
val () =
and () =
fun
loop_over_neighbors
{v : nat | v
.<n -
(pq : &pqueue_t
v :
:<!refwrt> void
if v = n
loop_over_neighbors (pq,
val alternative = cost[u] + adj_matrix[u, n, v]
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 () = main_loop {n} (pq, num_active)
(* Sanity check. *)
val- true = iseqz num_active
in
@(cost, prev)
Line 1,199 ⟶ 1,249:
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)
var u : [i : nat | i <= n] size_t i
val cost_column_no = i2sz 20
in
println! ("The requested paths:");
fprint_vertex_path (stdout_ref, vertex_arr, path_a_to_e,
Some cost[e], cost_column_no);
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
Line 1,211 ⟶ 1,280:
{{out}}
<pre>$ patscc -DATS_MEMALLOC_GCBDW dijkstra-algorithm.dats -lgc && ./a.out
The requested paths:
a -> c ->
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}}==
| |||