Theory Dijkstra_Shortest_Path.Test

section ‹Performance Test›
theory Test
  imports Dijkstra_Impl_Adet
begin
text ‹
  In this theory, we test our implementation of Dijkstra's algorithm for larger,
  randomly generated graphs.
›

text "Simple linear congruence generator for (low-quality) random numbers:"
definition "lcg_next s = ((81::nat)*s + 173) mod 268435456" 

text "Generate a complete graph over the given number of vertices,
    with random weights:"
definition ran_graph :: "nat ⇒ nat ⇒ (nat list×(nat × nat × nat) list)" where
  "ran_graph vertices seed == 
    ([0::nat..<vertices],fst 
     (while (λ (g,v,s). v < vertices)
     (λ (g,v,s). 
     let (g'',v'',s'') = (while (λ (g',v',s'). v' < vertices)
      (λ (g',v',s'). ((v,s',v')#g',v'+1,lcg_next s'))
      (g,0,s))
     in (g'',v+1,s''))
     ([],0,lcg_next seed)))"


text ‹
  To experiment with the exported code, we fix the node type to natural numbers,
  and add a from-list conversion:
›
type_synonym nat_res = "(nat,((nat,nat) path × nat)) rm"
type_synonym nat_list_res = "(nat × (nat,nat) path × nat) list"

definition nat_dijkstra :: "(nat,nat) hlg ⇒ nat ⇒ nat_res" where
  "nat_dijkstra ≡ hrfn_dijkstra"

definition hlg_from_list_nat :: "(nat,nat) adj_list ⇒(nat,nat) hlg" where 
  "hlg_from_list_nat ≡ hlg.from_list"

definition 
  nat_res_to_list :: "nat_res ⇒ nat_list_res" 
  where "nat_res_to_list ≡ rm.to_list"

value "nat_res_to_list (nat_dijkstra (hlg_from_list_nat (ran_graph 4 8912)) 0)"

ML_val ‹
let
  (* Configuration of test: *)
  val vertices = @{code nat_of_integer} 1000; (* Number of vertices *)
  val seed = @{code nat_of_integer} 123454; (* Seed for random number generator *)
  val cfg_print_paths = true; (* Whether to output complete paths *)
  val cfg_print_res = true; (* Whether to output result at all *)

  (* Internals *)
  fun string_of_edge (u,(w,v)) = let
    val u = @{code integer_of_nat} u;
    val w = @{code integer_of_nat} w;
    val v = @{code integer_of_nat} v;
  in
    "(" ^ string_of_int u ^ "," ^ string_of_int w ^ "," ^ string_of_int v ^ ")"
  end

  fun print_entry (dest,(path,weight)) = let
    val dest = @{code integer_of_nat} dest;
    val weight = @{code integer_of_nat} weight;
  in
    writeln (string_of_int dest ^ ": " ^ string_of_int weight ^
      ( if cfg_print_paths then 
          " via [" ^ commas (map string_of_edge (rev path)) ^ "]"
        else ""
      )
    )
  end

  fun print_res [] = ()
    | print_res (a::l) = let val _ = print_entry a in print_res l end;

  val start = Time.now();
  val graph = @{code hlg_from_list_nat} (@{code ran_graph} vertices seed);
  val rt1 = Time.toMilliseconds (Time.now() - start);

  val start = Time.now();
  val res = @{code nat_dijkstra} graph (@{code nat_of_integer} 0);
  val rt2 = Time.toMilliseconds (Time.now() - start);
in
  writeln (string_of_int (@{code integer_of_nat} vertices) ^ " vertices: " 
  ^ string_of_int rt2 ^ " ms + "
  ^ string_of_int rt1 ^ " ms to create graph = " 
  ^ string_of_int (rt1+rt2) ^ " ms");

  if cfg_print_res then
    print_res (@{code nat_res_to_list} res)
  else ()
end;
›

end