diff --git a/src/dot2lus.ml b/src/dot2lus.ml index bcbdbfe88938dfd4b80101557daeb5419a1a31c1..94b12bebf58da9220432c938d5555add9a582023 100644 --- a/src/dot2lus.ml +++ b/src/dot2lus.ml @@ -19,147 +19,147 @@ let algo_name (node : Topology.node) = (* prints includes, graph constants and helper functions *) let output_prelude output (graph : Topology.t) = - (* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *) - let b2s b = if b then "t" else "f" in - - let (array_to_string : bool array -> string) = - fun a -> - let l = Array.fold_right (fun b acc -> (b2s b)::acc) a [] in - "["^(String.concat "," l)^"]" in - - let (matrix_to_string : bool array array -> string) = - fun m -> - let l = Array.fold_right (fun a acc -> (array_to_string a)::acc) m [] in - "[\n\t"^(String.concat ",\n\t" l)^"]" in - - (* include Lustre algos *) - graph.nodes - |> List.map algo_name - |> List.sort_uniq String.compare - |> List.iter (Printf.fprintf output "include \"%s.lus\"\n"); - - (* define graph constants *) - output_string output "\n"; - Printf.fprintf output "const card = %d;\n" (List.length graph.nodes); - Printf.fprintf output "const links_number = %d;\n" (Topology.get_nb_link graph); - let dmin, dmax = Topology.get_degree graph in - Printf.fprintf output "const max_degree = %d;\n" dmax; - Printf.fprintf output "const min_degree = %d;\n" dmin; - Printf.fprintf output "const mean_degree = %f;\n" (Topology.get_mean_degree graph); - Printf.fprintf output "const is_directed = %b;\n" graph.directed; - Printf.fprintf output "const is_cyclic = %b;\n" (Topology.is_cyclic graph); - Printf.fprintf output "const is_connected = %b;\n" (Topology.is_connected graph); - - (* dot attributes *) - let already_defined = function - | "card" - | "links_number" - | "max_degree" - | "min_degree" - | "mean_degree" - | "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 output "const %s = %s;\n" name value) - graph.attributes; - - (* adjacency matrix *) - output_string output "const t = true;\n"; - output_string output "const f = false;\n"; - Printf.fprintf output - "const adjacency = %s;\n" - (graph |> Topology.to_adjacency |> matrix_to_string); - - (* helper functions *) - output_string output " -function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int); -var - found : int; -let - found = - with (N = 1) then (if s[0] then 0 else -1) - else dot2lus_first_set<<N-1>>(s[1 .. N-1]); - x = - if s[0] then 0 - else if found < 0 then -1 - else found + 1; -tel;\n"; - Printf.fprintf output " -function dot2lus_action_of_activation(activation : bool^%s) returns (action : %s); -let - action = %s(dot2lus_first_set<<%s>>(activation)); -tel;\n" action_number action_type action_of_int action_number + (* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *) + let b2s b = if b then "t" else "f" in + + let (array_to_string : bool array -> string) = + fun a -> + let l = Array.fold_right (fun b acc -> (b2s b)::acc) a [] in + "["^(String.concat "," l)^"]" in + + let (matrix_to_string : bool array array -> string) = + fun m -> + let l = Array.fold_right (fun a acc -> (array_to_string a)::acc) m [] in + "[\n\t"^(String.concat ",\n\t" l)^"]" in + + (* include Lustre algos *) + graph.nodes + |> List.map algo_name + |> List.sort_uniq String.compare + |> List.iter (Printf.fprintf output "include \"%s.lus\"\n"); + + (* define graph constants *) + output_string output "\n"; + Printf.fprintf output "const card = %d;\n" (List.length graph.nodes); + Printf.fprintf output "const links_number = %d;\n" (Topology.get_nb_link graph); + let dmin, dmax = Topology.get_degree graph in + Printf.fprintf output "const max_degree = %d;\n" dmax; + Printf.fprintf output "const min_degree = %d;\n" dmin; + Printf.fprintf output "const mean_degree = %f;\n" (Topology.get_mean_degree graph); + Printf.fprintf output "const is_directed = %b;\n" graph.directed; + Printf.fprintf output "const is_cyclic = %b;\n" (Topology.is_cyclic graph); + Printf.fprintf output "const is_connected = %b;\n" (Topology.is_connected graph); + + (* dot attributes *) + let already_defined = function + | "card" + | "links_number" + | "max_degree" + | "min_degree" + | "mean_degree" + | "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 output "const %s = %s;\n" name value) + graph.attributes; + + (* adjacency matrix *) + output_string output "const t = true;\n"; + output_string output "const f = false;\n"; + Printf.fprintf output + "const adjacency = %s;\n" + (graph |> Topology.to_adjacency |> matrix_to_string); + + (* helper functions *) + output_string output " + function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int); + var + found : int; + let + found = + with (N = 1) then (if s[0] then 0 else -1) + else dot2lus_first_set<<N-1>>(s[1 .. N-1]); + x = + if s[0] then 0 + else if found < 0 then -1 + else found + 1; + tel;\n"; + Printf.fprintf output " + function dot2lus_action_of_activation(activation : bool^%s) returns (action : %s); + let + action = %s(dot2lus_first_set<<%s>>(activation)); + tel;\n" action_number action_type action_of_int action_number (* prints the actual Lustre node that implements the input topology *) let output_topology output (graph : Topology.t) name = - let make_index (graph : Topology.t) : (Topology.node_id -> int) = - let index_map = Hashtbl.create (List.length graph.nodes) in - graph.nodes - |> List.map (fun (n : Topology.node) -> n.id) - |> List.iteri (fun index node_id -> Hashtbl.add index_map node_id index); - Hashtbl.find index_map (* returns the partially applied find *) in - - let sprint_neighbor_list neighbor_ids list : string = - match neighbor_ids with - | [] -> "[]" - | n :: ns -> - let prefix, sufix = Printf.sprintf "[ %s[%d]" list n, " ]" in - let concat acc n = acc ^ (Printf.sprintf ", %s[%d]" list n) in - (List.fold_left concat prefix ns) ^ sufix in - - Printf.fprintf output - "\nnode %s(p : bool^%s^card; initials : %s^card)\n" - name action_number state_type; - - Printf.fprintf output - "returns (p_c : %s^card; Enab_p : bool^%s^card);\n" - state_type action_number; - - output_string output "var\n"; - - Printf.fprintf output "\tprev_p_c : %s^card;\n\n" state_type; - graph.nodes - |> List.iteri (fun i _ -> Printf.fprintf output "\tsel_%d : bool;\n" i); - - output_string output "let\n"; - - output_string output "\tprev_p_c = initials -> pre(p_c);\n\n"; - graph.nodes - |> List.iteri (fun i _ -> - Printf.fprintf output - "\tsel_%d = false -> boolred<<1,%s,%s>>(p[%d]);\n" - i action_number action_number i); - - let index_of_id = make_index graph in - graph.nodes - |> List.iteri (fun i n -> - let algo = algo_name n in - let neighbors = graph.succ n.id |> List.map (fun (_, id) -> index_of_id id) in - let deg = List.length neighbors in - let nl = sprint_neighbor_list neighbors "p_c" in - let pnl = sprint_neighbor_list neighbors "prev_p_c" in - Printf.fprintf output - "\n\tp_c[%d] =\n\t\tif not sel_%d then prev_p_c[%d]\n\t\telse " - i i i; - if !clock then Printf.fprintf output - "current(%s_step<<%d>>(\n\t\t\tprev_p_c[%d], \n\t\t\t%s, \n\t\t\tdot2lus_action_of_activation(p[%d])\n\t\t) when sel_%d);\n" - algo deg i pnl i i - else Printf.fprintf output - "%s_step<<%d>>(\n\t\t\tprev_p_c[%d], \n\t\t\t%s, \n\t\t\tdot2lus_action_of_activation(p[%d])\n\t\t);\n" - algo deg i pnl i; - Printf.fprintf output - "\tEnab_p[%d] = %s_enable<<%d>>(p_c[%d], %s);\n" - i algo deg i nl); - - output_string output "tel;\n" + let make_index (graph : Topology.t) : (Topology.node_id -> int) = + let index_map = Hashtbl.create (List.length graph.nodes) in + graph.nodes + |> List.map (fun (n : Topology.node) -> n.id) + |> List.iteri (fun index node_id -> Hashtbl.add index_map node_id index); + Hashtbl.find index_map (* returns the partially applied find *) in + + let sprint_neighbor_list neighbor_ids list : string = + match neighbor_ids with + | [] -> "[]" + | n :: ns -> + let prefix, sufix = Printf.sprintf "[ %s[%d]" list n, " ]" in + let concat acc n = acc ^ (Printf.sprintf ", %s[%d]" list n) in + (List.fold_left concat prefix ns) ^ sufix in + + Printf.fprintf output + "\nnode %s(p : bool^%s^card; initials : %s^card)\n" + name action_number state_type; + + Printf.fprintf output + "returns (p_c : %s^card; Enab_p : bool^%s^card);\n" + state_type action_number; + + output_string output "var\n"; + + Printf.fprintf output "\tprev_p_c : %s^card;\n\n" state_type; + graph.nodes + |> List.iteri (fun i _ -> Printf.fprintf output "\tsel_%d : bool;\n" i); + + output_string output "let\n"; + + output_string output "\tprev_p_c = initials -> pre(p_c);\n\n"; + graph.nodes + |> List.iteri (fun i _ -> + Printf.fprintf output + "\tsel_%d = false -> boolred<<1,%s,%s>>(p[%d]);\n" + i action_number action_number i); + + let index_of_id = make_index graph in + graph.nodes + |> List.iteri (fun i n -> + let algo = algo_name n in + let neighbors = graph.succ n.id |> List.map (fun (_, id) -> index_of_id id) in + let deg = List.length neighbors in + let nl = sprint_neighbor_list neighbors "p_c" in + let pnl = sprint_neighbor_list neighbors "prev_p_c" in + Printf.fprintf output + "\n\tp_c[%d] =\n\t\tif not sel_%d then prev_p_c[%d]\n\t\telse " + i i i; + if !clock then Printf.fprintf output + "current(%s_step<<%d>>(\n\t\t\tprev_p_c[%d], \n\t\t\t%s, \n\t\t\tdot2lus_action_of_activation(p[%d])\n\t\t) when sel_%d);\n" + algo deg i pnl i i + else Printf.fprintf output + "%s_step<<%d>>(\n\t\t\tprev_p_c[%d], \n\t\t\t%s, \n\t\t\tdot2lus_action_of_activation(p[%d])\n\t\t);\n" + algo deg i pnl i; + Printf.fprintf output + "\tEnab_p[%d] = %s_enable<<%d>>(p_c[%d], %s);\n" + i algo deg i nl); + + output_string output "tel;\n" let dot2lus dotfile lusfile =