From 8d94d6d845694d76410fce3b07219442ed64b138 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Wed, 21 Feb 2024 10:10:44 +0100 Subject: [PATCH] Compute the distance using the Floyd-Marshall algorithm (which was actualy already there for the diameter) --- lib/sasacore/diameter.ml | 64 ------------ lib/sasacore/diameter.mli | 4 - lib/sasacore/register.ml | 4 +- lib/sasacore/topology.ml | 114 ++++++++++++++------ lib/sasacore/topology.mli | 4 +- salut/lib/utils.lus | 8 +- salut/src/dot2lus.ml | 145 ++++++++++++++------------ salut/test/dijkstra-ring/dune-project | 2 +- test/ghosh/util | 1 + tools/gg/graphGen.ml | 4 +- 10 files changed, 181 insertions(+), 169 deletions(-) delete mode 100644 lib/sasacore/diameter.ml delete mode 100644 lib/sasacore/diameter.mli mode change 100644 => 120000 salut/test/dijkstra-ring/dune-project create mode 120000 test/ghosh/util diff --git a/lib/sasacore/diameter.ml b/lib/sasacore/diameter.ml deleted file mode 100644 index 27a85cf4..00000000 --- a/lib/sasacore/diameter.ml +++ /dev/null @@ -1,64 +0,0 @@ - -(* take a string and the list of all node and returns the position of the node in the list *) -let (pos:string -> Topology.node list -> int) = - fun nid lid -> - fst (List.fold_left (fun (found_i,i) lid -> if (nid=lid.Topology.id) then (i,i+1) else (found_i,i+1) ) (-1, 0) lid) - -(* take a graph t and returns the Adjacency matrix of t *) -let (graph_to_adjency: Topology.t -> int array array) = - fun t-> - let taille = List.length t.nodes in - let mat = Array.make_matrix (taille) (taille) 0 in - List.iter (fun n -> - (List.iter (fun (m) -> mat.(pos n.Topology.id t.nodes).(pos m t.nodes) <- 1 ) - (t.succ n.Topology.id) ) ) (t.nodes); - mat - - -(* Initialize the Adjacency matrix for Floyd Warshall algorithm *) -let (initFW: int array array -> int array array) = - fun m -> - let n = (Array.length m.(0)) in - for i=0 to (n - 1) do - for j=0 to (n - 1) do - if (i<>j) then - (if (m.(i).(j)=1) then m.(i).(j) <- 1 else m.(i).(j) <- n+1) - else m.(i).(j) <- 0 - done; - done; - m - - -(* Apply Floyd Warshall algorithm which gives the matrix of all pairs shortest path *) -let (floydwarshall:int array array -> int array array) = - fun m -> - let w = initFW m in - let n = (Array.length m.(0)) in - for k=0 to (n - 1) do - for i=0 to (n - 1) do - for j=0 to (n - 1) do - w.(i).(j) <- (min (w.(i).(j)) (w.(i).(k) + w.(k).(j))) - done; - done; - done; - w - - -(* returns the greatest int of a matrix *) -let (max_mat: int array array -> int) = - fun mat -> - let n = (Array.length mat) and m = (Array.length mat.(0)) in - let maxi = ref (-1) in - for i=0 to (n - 1) do - for j=0 to (m - 1) do - maxi := max !maxi mat.(i).(j) - done; - done; - !maxi - -(* takes a graph t in argument and returns the diameter *) -let (get: Topology.t -> int ) = - fun t -> - let d = (max_mat(floydwarshall (graph_to_adjency t))) in - Printf.eprintf " ====> The Graph Diameter is %d \n%!" d; - d diff --git a/lib/sasacore/diameter.mli b/lib/sasacore/diameter.mli deleted file mode 100644 index b31abddc..00000000 --- a/lib/sasacore/diameter.mli +++ /dev/null @@ -1,4 +0,0 @@ - -(** Watch out, computing the diameter can be very expensive *) - -val get : Topology.t -> int diff --git a/lib/sasacore/register.ml b/lib/sasacore/register.ml index 3d21cff7..41c0e0cb 100644 --- a/lib/sasacore/register.ml +++ b/lib/sasacore/register.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 11/10/2021 (at 14:21) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/02/2024 (at 09:44) by Erwan Jahier> *) type 's neighbor = { state: 's ; @@ -340,7 +340,7 @@ let (diameter : unit -> int) = match tbls.diameter with | Some x -> x | None -> - let x = Diameter.get (get_topology ()) in + let x = Topology.diameter (get_topology ()) in tbls.diameter <- Some x; x diff --git a/lib/sasacore/topology.ml b/lib/sasacore/topology.ml index 47db5f5e..0131c6d3 100644 --- a/lib/sasacore/topology.ml +++ b/lib/sasacore/topology.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 20/06/2023 (at 22:55) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/02/2024 (at 10:00) by Erwan Jahier> *) open Graph open Graph.Dot_ast @@ -90,27 +90,92 @@ let rec (get_weight: Dot_ast.attr -> int) = type attrs = (string * string) list -(* compute the distance between 2 nodes in g denoted by their position in g.nodes *) -module StrSet = Set.Make(String) +(**********************************************************************************) +(* compute the distance between 2 nodes in g denoted by their position in g.nodes + using the Floyd Warshall algorithm +*) +(* take a string and the list of all node and returns the position of the node in the list *) +let (pos:string -> node list -> int) = + fun nid lid -> + fst (List.fold_left (fun (found_i,i) lid -> if (nid=lid.id) then (i,i+1) else (found_i,i+1) ) (-1, 0) lid) + +(* take a graph t and returns the Adjacency matrix of t *) +let (graph_to_adjency: t -> int array array) = + fun t-> + let taille = List.length t.nodes in + let mat = Array.make_matrix (taille) (taille) 0 in + List.iter (fun n -> + (List.iter (fun (m) -> mat.(pos n.id t.nodes).(pos m t.nodes) <- 1 ) + (t.succ n.id) ) ) (t.nodes); + mat + + +(* Initialize the Adjacency matrix for Floyd Warshall algorithm *) +let (initFW: int array array -> int array array) = + fun m -> + let n = (Array.length m.(0)) in + for i=0 to (n - 1) do + for j=0 to (n - 1) do + if (i<>j) then + (if (m.(i).(j)=1) then m.(i).(j) <- 1 else m.(i).(j) <- n+1) + else m.(i).(j) <- 0 + done; + done; + m + + +(* Apply Floyd Warshall algorithm which gives the matrix of all pairs shortest path *) +let (floydwarshall:int array array -> int array array) = + fun m -> + let w = initFW m in + let n = (Array.length m.(0)) in + for k=0 to (n - 1) do + for i=0 to (n - 1) do + for j=0 to (n - 1) do + w.(i).(j) <- (min (w.(i).(j)) (w.(i).(k) + w.(k).(j))) + done; + done; + done; + w + +(* tabulate everything that is expensive to compute *) +let distance_tbl = Hashtbl.create 1 +let diameter_tbl = Hashtbl.create 1 + +let to_distance t = + match Hashtbl.find_opt distance_tbl t with + | Some d -> d + | None -> + let d = floydwarshall (graph_to_adjency t) in + Hashtbl.add distance_tbl t d; + d + +(**********************************************************************************) +(* returns the greatest int of a matrix *) +let (max_mat: int array array -> int) = + fun mat -> + let n = (Array.length mat) and m = (Array.length mat.(0)) in + let maxi = ref (-1) in + for i=0 to (n - 1) do + for j=0 to (m - 1) do + maxi := max !maxi mat.(i).(j) + done; + done; + !maxi -let (distance : t -> int -> int -> int) = - fun g i j -> - assert( 0 <= i && i<=j && j < List.length g.nodes); - let ni = List.nth g.nodes i in - let nj = List.nth g.nodes j in - let (get_succ : node_id -> StrSet.t) = - fun n -> g.succ n |> List.to_seq |> StrSet.of_seq - in - let rec aux n succ cpt = - if StrSet.mem n.id succ then cpt else - let succ = - StrSet.fold (fun n acc -> StrSet.union acc (get_succ n)) succ succ - in - aux n succ (cpt+1) - in - aux ni (StrSet.singleton nj.id) 0 +(* takes a graph t in argument and returns the diameter *) +let (diameter : t -> int ) = + fun t -> + match Hashtbl.find_opt diameter_tbl t with + | Some d -> d + | None -> + let d = (max_mat(to_distance t)) in + Printf.eprintf " ====> The Graph Diameter is %d \n%!" d; + Hashtbl.add diameter_tbl t d; + d +(**********************************************************************************) let (do_graph_attr : attrs -> (Dot_ast.id * Dot_ast.id option) list -> attrs) = fun acc l -> let f acc = function @@ -208,17 +273,6 @@ let (to_adjacency: t -> bool array array) = t.nodes; m -let (to_distance : t -> int array array) = - fun t -> - let n = List.length t.nodes in - let m = Array.make_matrix n n 0 in - for i = 0 to n-1 do - for j = i to n-1 do - m.(i).(j) <- distance t i j; - m.(j).(i) <- m.(i).(j); - done - done; - m let (get_degree: t -> int*int) = fun t -> diff --git a/lib/sasacore/topology.mli b/lib/sasacore/topology.mli index d1970dd0..37d45e17 100644 --- a/lib/sasacore/topology.mli +++ b/lib/sasacore/topology.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 24/01/2024 (at 16:28) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/02/2024 (at 09:40) by Erwan Jahier> *) (** {1 Topology: internal representation of Graphs } *) @@ -31,6 +31,8 @@ val to_adjacency: t -> bool array array *) val to_distance: t -> int array array +val diameter: t -> int + val get_nb_link: t -> int val get_mean_degree : t -> float val is_connected : t -> bool diff --git a/salut/lib/utils.lus b/salut/lib/utils.lus index f38e231b..12fc87d3 100644 --- a/salut/lib/utils.lus +++ b/salut/lib/utils.lus @@ -35,7 +35,7 @@ function nary_xor_alt<<const N:int>>(s : bool^N) returns (y : bool); let y = with N=1 then s[0] else if s[0] then boolnone<<N-1>>(s[1..N-1]) - else nary_xor<<N-1>>(s[1..N-1]); + else nary_xor_alt<<N-1>>(s[1..N-1]); tel; function nary_xor_old<<const N:int>>(s : bool^N) returns (y : bool); let @@ -160,6 +160,12 @@ let else nary_xor<<n-1>>(s[1..n-1]); tel +function count <<const n:int>>(s:bool^n) returns (o:int); +let + o = with n=1 then (if s[0] then 1 else 0) else + (if s[0] then 1 else 0) + count<<n-1>>(s[1..n-1]); +tel + function nary_not <<const n:int>>(s:bool^n) returns (o:bool); let o = with n=1 then not s[0] diff --git a/salut/src/dot2lus.ml b/salut/src/dot2lus.ml index fa0da192..03960ea2 100644 --- a/salut/src/dot2lus.ml +++ b/salut/src/dot2lus.ml @@ -9,6 +9,10 @@ let action_type = "action" let action_number = "actions_number" let action_of_int = "action_of_int" +let quiet = ref false +let pverbose msg = if not !quiet then Printf.printf "%s\n%!" msg + + (* global setting, parsed from command-line options *) let clock = ref false @@ -19,72 +23,83 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) = Printf.fprintf lustre_topology "-- automatically generated by salut \n"; Printf.fprintf lustre_const "-- automatically generated by salut \n"; - (* include Lustre algos *) - graph.nodes - |> List.map algo_name - |> List.sort_uniq String.compare - |> List.iter (Printf.fprintf lustre_topology "include \"%s.lus\"\n"); - - (* define graph constants *) - output_string lustre_topology "\n"; - Printf.fprintf lustre_const "const card = %d;\n" (List.length graph.nodes); - Printf.fprintf lustre_const "const links_number = %d;\n" (Topology.get_nb_link graph); - let dmin, dmax = Topology.get_degree graph in - Printf.fprintf lustre_const "const max_degree = %d;\n" dmax; - Printf.fprintf lustre_const "const min_degree = %d;\n" dmin; - Printf.fprintf lustre_const "const mean_degree = %f;\n" (Topology.get_mean_degree graph); - Printf.fprintf lustre_const "const diameter = %d;\n" (Diameter.get graph); - Printf.fprintf lustre_const "const is_directed = %b;\n" graph.directed; - Printf.fprintf lustre_const "const is_cyclic = %b;\n" (Topology.is_cyclic graph); - Printf.fprintf lustre_const "const is_connected = %b;\n" (Topology.is_connected graph); - let neigh_list = graph.nodes |> List.map (fun (n:Topology.node) -> graph.pred n.id) in - let nb_neigh_list = neigh_list |> List.map (fun n -> string_of_int (List.length n)) in - Printf.fprintf lustre_const "const nb_neighbors = %s;\n" ("["^(String.concat "," (nb_neigh_list))^"]"); - - (* dot attributes *) - let already_defined = function - | "card" - | "links_number" - | "max_degree" - | "min_degree" - | "mean_degree" - | "diameter" - | "is_directed" - | "is_cyclic" - | "is_connected" - | "f" - | "t" - | "adjacency" -> true - | _ -> false in - List.iter - (fun (name, value) -> - if not (already_defined name) - then Printf.fprintf lustre_const "const %s = %s;\n" name value) - graph.attributes; - - (* adjacency matrix *) - output_string lustre_const "const t = true;\n"; - output_string lustre_const "const f = false;\n"; - (* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *) - let b2s b = if b then "t" else "f" in - Printf.fprintf lustre_const - "const adjacency = %s;\n" - (graph |> Topology.to_adjacency |> (StringOf.matrix_lv6 b2s)); - - Printf.fprintf lustre_const - "const distance = %s;\n" - (graph |> Topology.to_distance |> (StringOf.matrix_lv6 string_of_int)); - - (* State.lus File *) - output_string lustre_topology" + (* include Lustre algos *) + graph.nodes + |> List.map algo_name + |> List.sort_uniq String.compare + |> List.iter (Printf.fprintf lustre_topology "include \"%s.lus\"\n"); + + (* define graph constants *) + output_string lustre_topology "\n"; + pverbose "compute card"; + Printf.fprintf lustre_const "const card = %d;\n" (List.length graph.nodes); + pverbose "compute link nb"; + Printf.fprintf lustre_const "const links_number = %d;\n" (Topology.get_nb_link graph); + pverbose "compute degree"; + let dmin, dmax = Topology.get_degree graph in + Printf.fprintf lustre_const "const max_degree = %d;\n" dmax; + Printf.fprintf lustre_const "const min_degree = %d;\n" dmin; + pverbose "compute mean degree"; + Printf.fprintf lustre_const "const mean_degree = %f;\n" (Topology.get_mean_degree graph); + pverbose "compute diameter"; + Printf.fprintf lustre_const "const diameter = %d;\n" (Topology.diameter graph); + Printf.fprintf lustre_const "const is_directed = %b;\n" graph.directed; + pverbose "compute if cyclic"; + Printf.fprintf lustre_const "const is_cyclic = %b;\n" (Topology.is_cyclic graph); + pverbose "compute if connected"; + Printf.fprintf lustre_const "const is_connected = %b;\n" (Topology.is_connected graph); + pverbose "compute if connected: done"; + let neigh_list = graph.nodes |> List.map (fun (n:Topology.node) -> graph.pred n.id) in + let nb_neigh_list = neigh_list |> List.map (fun n -> string_of_int (List.length n)) in + Printf.fprintf lustre_const "const nb_neighbors = %s;\n" ("["^(String.concat "," (nb_neigh_list))^"]"); + + (* dot attributes *) + let already_defined = function + | "card" + | "links_number" + | "max_degree" + | "min_degree" + | "mean_degree" + | "diameter" + | "is_directed" + | "is_cyclic" + | "is_connected" + | "f" + | "t" + | "adjacency" -> true + | _ -> false in + List.iter + (fun (name, value) -> + if not (already_defined name) + then Printf.fprintf lustre_const "const %s = %s;\n" name value) + graph.attributes; + + (* adjacency matrix *) + output_string lustre_const "const t = true;\n"; + output_string lustre_const "const f = false;\n"; + (* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *) + let b2s b = if b then "t" else "f" in + pverbose "compute adjacency"; + Printf.fprintf lustre_const + "const adjacency = %s;\n" + (graph |> Topology.to_adjacency |> (StringOf.matrix_lv6 b2s)); + + pverbose "compute distance"; + Printf.fprintf lustre_const + "const distance = %s;\n" + (graph |> Topology.to_distance |> (StringOf.matrix_lv6 string_of_int)); + pverbose "compute distance: done"; + + (* State.lus File *) + output_string lustre_topology" include \"state.lus\""; - (* Neighbors type *) - output_string lustre_topology " + (* Neighbors type *) + output_string lustre_topology " type neigh = struct { state:state; reply:int; weight:int };\n"; - (* helper functions *) - output_string lustre_topology " + (* helper functions *) + output_string lustre_topology " function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int); var found : int; @@ -97,7 +112,7 @@ let else if found < 0 then -1 else found + 1; tel;\n"; - Printf.fprintf lustre_topology " + Printf.fprintf lustre_topology " function dot2lus_action_of_activation(activation : bool^%s) returns (action : %s); let action = %s(dot2lus_first_set<<%s>>(activation)); @@ -226,7 +241,9 @@ let _ = in let speclist = [ ("-o", Arg.Set_string lusfile, "Set output file (default is inferred from input file)"); - ("--clock", Arg.Set clock, "Generate clocked code (default is unclocked)") ] + ("--clock", Arg.Set clock, "Generate clocked code (default is unclocked)"); + ("--quiet", Arg.Set quiet, "Be more quiet<") + ] in Arg.parse speclist anon_parse usage; match !dotfile with diff --git a/salut/test/dijkstra-ring/dune-project b/salut/test/dijkstra-ring/dune-project deleted file mode 100644 index 37f995d6..00000000 --- a/salut/test/dijkstra-ring/dune-project +++ /dev/null @@ -1 +0,0 @@ -(lang dune 3.0) diff --git a/salut/test/dijkstra-ring/dune-project b/salut/test/dijkstra-ring/dune-project new file mode 120000 index 00000000..f539fb46 --- /dev/null +++ b/salut/test/dijkstra-ring/dune-project @@ -0,0 +1 @@ +../../../test/dune-project2copy \ No newline at end of file diff --git a/test/ghosh/util b/test/ghosh/util new file mode 120000 index 00000000..a0c96ec8 --- /dev/null +++ b/test/ghosh/util @@ -0,0 +1 @@ +../../salut/test/ghosh/util/ \ No newline at end of file diff --git a/tools/gg/graphGen.ml b/tools/gg/graphGen.ml index c39e8d9f..cbfc4310 100644 --- a/tools/gg/graphGen.ml +++ b/tools/gg/graphGen.ml @@ -75,7 +75,7 @@ let compute_attr : (Topology.t -> string list -> (string * string) list) = (fst x) && (snd x)) | Some x -> (fst x) && (snd x) ) | "links_number" -> string_of_int (get_nb_link g) - | "diameter" -> string_of_int (Diameter.get g) + | "diameter" -> string_of_int (Topology.diameter g) | s -> string_of_int (let s = String.split_on_char ' ' s in if List.hd s = "height" && List.length s = 2 then get_height g (List.hd (List.tl s)) @@ -142,7 +142,7 @@ let all_attr : bool -> bool -> (Topology.t -> (string * string) list) = ["diameter", string_of_int ( Printf.eprintf "Computing the diameter...\n"; flush stderr; - Diameter.get g) + Topology.diameter g) ]) -- GitLab