Skip to content
Snippets Groups Projects
Commit a331f5b6 authored by erwan's avatar erwan
Browse files

New: Add various graph info (card, adjency matrix, etc.) into the generated oracles

parent 6618348f
No related branches found
No related tags found
No related merge requests found
Pipeline #26704 passed
(* Time-stamp: <modified the 05/07/2019 (at 15:25) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 17:29) by Erwan Jahier> *)
open Process open Process
let b2s b = if b then "t" else "f"
let (f: 'v Process.t list -> string) = let (array_to_string : bool array -> string) =
fun pl -> fun a ->
let degree = Register.max_degree () in let l = Array.fold_right (fun b acc -> (b2s b)::acc) a [] in
let diameter = Register.diameter () in "["^(String.concat "," l)^"]"
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)^"]"
let graph_attributes_to_string () =
let al = Register.graph_attribute_list () in
let l = List.map (fun (n,v) -> Printf.sprintf "const %s=%s;\n" n v) al in
String.concat "" l
let (f: Topology.t -> 'v Process.t list -> string) =
fun g pl ->
let actions_nb = List.map (fun p -> List.length p.actions) pl in let actions_nb = List.map (fun p -> List.length p.actions) pl in
let m = List.fold_left max (List.hd actions_nb) (List.tl actions_nb) in let m = List.fold_left max (List.hd actions_nb) (List.tl actions_nb) in
let n = List.length pl in let n = List.length pl in
...@@ -38,8 +52,16 @@ let (f: 'v Process.t list -> string) = ...@@ -38,8 +52,16 @@ let (f: 'v Process.t list -> string) =
const an=%d; -- actions number const an=%d; -- actions number
const pn=%d; -- processes number const pn=%d; -- processes number
const degree=%d; const degree=%d;
const min_degree=%d;
const mean_degree=%f;
const diameter=%d; const diameter=%d;
const card=%d;
const links_number=%d;
const is_cyclic=%b;
const is_connected=%b;
const is_a_tree=%b;
const adjency=%s;
%s
node oracle(%s) returns (ok:bool); node oracle(%s) returns (ok:bool);
var var
%slet %slet
...@@ -49,7 +71,18 @@ tel ...@@ -49,7 +71,18 @@ tel
" "
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha) (Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
algo algo
m n degree diameter m n
(Register.max_degree ())
(Register.min_degree ())
(Register.mean_degree ())
(Register.diameter ())
(Register.card ())
(Register.links_number ())
(Register.is_cyclic ())
(Register.is_connected ())
(Register.is_tree ())
(matrix_to_string (Topology.to_adjency g))
(graph_attributes_to_string ())
input_decl input_decl
array_decl array_decl
array_def_acti array_def_acti
......
(* Time-stamp: <modified the 25/06/2019 (at 11:13) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 16:35) by Erwan Jahier> *)
(** generates oracle skeletons *) (** generates oracle skeletons *)
val f: 'v Process.t list -> string val f: Topology.t -> 'v Process.t list -> string
(* Time-stamp: <modified the 04/07/2019 (at 10:35) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 17:27) by Erwan Jahier> *)
type 's neighbor = { type 's neighbor = {
state: 's ; state: 's ;
...@@ -275,3 +275,7 @@ let (get_graph_attribute : string -> string) = ...@@ -275,3 +275,7 @@ let (get_graph_attribute : string -> string) =
let (set_graph_attribute : string -> string -> unit) = let (set_graph_attribute : string -> string -> unit) =
Hashtbl.replace tbls.graph_attributes Hashtbl.replace tbls.graph_attributes
let (graph_attribute_list: unit -> (string * string) list) =
fun () ->
Hashtbl.fold (fun n v acc -> (n,v)::acc) tbls.graph_attributes []
(* Time-stamp: <modified the 04/07/2019 (at 10:34) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 17:27) by Erwan Jahier> *)
type 's neighbor = { type 's neighbor = {
state: 's ; state: 's ;
...@@ -44,6 +44,7 @@ val set_diameter : (unit -> int) -> unit ...@@ -44,6 +44,7 @@ val set_diameter : (unit -> int) -> unit
val get_graph_attribute : string -> string val get_graph_attribute : string -> string
val set_graph_attribute : string -> string -> unit val set_graph_attribute : string -> string -> unit
val graph_attribute_list: unit -> (string * string) list
val card : unit -> int val card : unit -> int
val min_degree : unit -> int val min_degree : unit -> int
......
(* Time-stamp: <modified the 25/06/2019 (at 11:14) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 16:34) by Erwan Jahier> *)
open Register open Register
open Sasacore open Sasacore
...@@ -285,7 +285,7 @@ let (make : bool -> string array -> 'v t) = ...@@ -285,7 +285,7 @@ let (make : bool -> string array -> 'v t) =
flush stderr; exit 1 flush stderr; exit 1
) else ) else
let oc = open_out fn in let oc = open_out fn in
Printf.fprintf oc "%s" (GenOracle.f pl); Printf.fprintf oc "%s" (GenOracle.f g pl);
flush oc; flush oc;
close_out oc; close_out oc;
exit 0); exit 0);
......
(* Time-stamp: <modified the 03/07/2019 (at 10:18) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 16:32) by Erwan Jahier> *)
open Graph open Graph
open Graph.Dot_ast open Graph.Dot_ast
...@@ -126,3 +126,17 @@ let (read: string -> t) = fun f -> ...@@ -126,3 +126,17 @@ let (read: string -> t) = fun f ->
failwith (str^ " unknown node id") failwith (str^ " unknown node id")
) )
} }
let (to_adjency: t -> bool array array) =
fun t ->
let n = List.length t.nodes in
let rank_node_tbl = Hashtbl.create n in
let m = Array.make_matrix n n false in
let rank_node = Hashtbl.find rank_node_tbl in
List.iteri (fun i n -> Hashtbl.add rank_node_tbl n.id i) t.nodes;
List.iteri
(fun i n ->
List.iter (fun (_,target) -> m.(i).(rank_node target) <- true) (t.succ n.id)
)
t.nodes;
m
(* Time-stamp: <modified the 21/06/2019 (at 18:13) by Erwan Jahier> *) (* Time-stamp: <modified the 05/07/2019 (at 16:19) by Erwan Jahier> *)
type node_id = string type node_id = string
type node = { type node = {
...@@ -16,3 +16,7 @@ type t = { ...@@ -16,3 +16,7 @@ type t = {
(** Parse a sasa dot file *) (** Parse a sasa dot file *)
val read: string -> t val read: string -> t
val to_adjency: t -> bool array array
graph fig4_1 { graph fig4_1 {
graph [k=42]
p1 [algo="root.ml" init="{d=2;par=0}"] p1 [algo="root.ml" init="{d=2;par=0}"]
p2 [algo="p.ml" init="{d=0;par=0}"] p2 [algo="p.ml" init="{d=0;par=0}"]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment