From a331f5b60ab2fbf1c23741ab29e45235190770f1 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 5 Jul 2019 17:30:24 +0200
Subject: [PATCH] New: Add various graph info (card, adjency matrix, etc.) into
the generated oracles
---
lib/sasacore/genOracle.ml | 47 ++++++++++++++++++++++++++-----
lib/sasacore/genOracle.mli | 4 +--
lib/sasacore/register.ml | 6 +++-
lib/sasacore/register.mli | 3 +-
lib/sasacore/sasa.ml | 4 +--
lib/sasacore/topology.ml | 16 ++++++++++-
lib/sasacore/topology.mli | 6 +++-
test/bfs-spanning-tree/fig5.1.dot | 1 +
8 files changed, 72 insertions(+), 15 deletions(-)
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index 72d13556..cfaed1f0 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,12 +1,26 @@
-(* 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
+let b2s b = if b then "t" else "f"
-let (f: 'v Process.t list -> string) =
- fun pl ->
- let degree = Register.max_degree () in
- let diameter = Register.diameter () 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)^"]"
+
+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 m = List.fold_left max (List.hd actions_nb) (List.tl actions_nb) in
let n = List.length pl in
@@ -38,8 +52,16 @@ let (f: 'v Process.t list -> string) =
const an=%d; -- actions number
const pn=%d; -- processes number
const degree=%d;
+const min_degree=%d;
+const mean_degree=%f;
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);
var
%slet
@@ -49,7 +71,18 @@ tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
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
array_decl
array_def_acti
diff --git a/lib/sasacore/genOracle.mli b/lib/sasacore/genOracle.mli
index f9d72a5d..77fc3313 100644
--- a/lib/sasacore/genOracle.mli
+++ b/lib/sasacore/genOracle.mli
@@ -1,4 +1,4 @@
-(* 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 *)
-val f: 'v Process.t list -> string
+val f: Topology.t -> 'v Process.t list -> string
diff --git a/lib/sasacore/register.ml b/lib/sasacore/register.ml
index ef4dd5ec..8385cc4f 100644
--- a/lib/sasacore/register.ml
+++ b/lib/sasacore/register.ml
@@ -1,4 +1,4 @@
-(* 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 = {
state: 's ;
@@ -275,3 +275,7 @@ let (get_graph_attribute : string -> string) =
let (set_graph_attribute : string -> string -> unit) =
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 []
diff --git a/lib/sasacore/register.mli b/lib/sasacore/register.mli
index cb2a1de0..9947c84a 100644
--- a/lib/sasacore/register.mli
+++ b/lib/sasacore/register.mli
@@ -1,4 +1,4 @@
-(* 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 = {
state: 's ;
@@ -44,6 +44,7 @@ val set_diameter : (unit -> int) -> unit
val get_graph_attribute : string -> string
val set_graph_attribute : string -> string -> unit
+val graph_attribute_list: unit -> (string * string) list
val card : unit -> int
val min_degree : unit -> int
diff --git a/lib/sasacore/sasa.ml b/lib/sasacore/sasa.ml
index be474c1f..d656ffb5 100644
--- a/lib/sasacore/sasa.ml
+++ b/lib/sasacore/sasa.ml
@@ -1,4 +1,4 @@
-(* 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 Sasacore
@@ -285,7 +285,7 @@ let (make : bool -> string array -> 'v t) =
flush stderr; exit 1
) else
let oc = open_out fn in
- Printf.fprintf oc "%s" (GenOracle.f pl);
+ Printf.fprintf oc "%s" (GenOracle.f g pl);
flush oc;
close_out oc;
exit 0);
diff --git a/lib/sasacore/topology.ml b/lib/sasacore/topology.ml
index 74b859a0..3b7f61d4 100644
--- a/lib/sasacore/topology.ml
+++ b/lib/sasacore/topology.ml
@@ -1,4 +1,4 @@
-(* 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.Dot_ast
@@ -126,3 +126,17 @@ let (read: string -> t) = fun f ->
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
diff --git a/lib/sasacore/topology.mli b/lib/sasacore/topology.mli
index 1768b046..c04cb057 100644
--- a/lib/sasacore/topology.mli
+++ b/lib/sasacore/topology.mli
@@ -1,4 +1,4 @@
-(* 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 = {
@@ -16,3 +16,7 @@ type t = {
(** Parse a sasa dot file *)
val read: string -> t
+
+
+val to_adjency: t -> bool array array
+
diff --git a/test/bfs-spanning-tree/fig5.1.dot b/test/bfs-spanning-tree/fig5.1.dot
index 78f9ff08..05e55820 100644
--- a/test/bfs-spanning-tree/fig5.1.dot
+++ b/test/bfs-spanning-tree/fig5.1.dot
@@ -1,4 +1,5 @@
graph fig4_1 {
+ graph [k=42]
p1 [algo="root.ml" init="{d=2;par=0}"]
p2 [algo="p.ml" init="{d=0;par=0}"]
--
GitLab