From ff0da0525b179c86486b56f9d4ee8c492e224acc Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 21 Jun 2023 11:26:03 +0200
Subject: [PATCH] new: add the distance matrix (int^n^n) in the salut generated
code This is necessary to compute the heigth in a tree and will probably be
useful for other purposes
---
lib/sasacore/topology.ml | 37 +++++++++++++++-
lib/sasacore/topology.mli | 3 +-
salut/src/dot2lus.ml | 66 +++++++++++++++-------------
salut/test/kclustering/cost.lus | 41 ++++++++----------
salut/test/rsp_tree/tree4.lus | 77 ---------------------------------
salut/test/run-kind2.sh | 23 ++++++----
6 files changed, 103 insertions(+), 144 deletions(-)
delete mode 100644 salut/test/rsp_tree/tree4.lus
diff --git a/lib/sasacore/topology.ml b/lib/sasacore/topology.ml
index 60574d21..47db5f5e 100644
--- a/lib/sasacore/topology.ml
+++ b/lib/sasacore/topology.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 30/05/2022 (at 14:49) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2023 (at 22:55) by Erwan Jahier> *)
open Graph
open Graph.Dot_ast
@@ -70,7 +70,7 @@ let (get_init: Dot_ast.attr list -> string) =
let compare_alpha_num str1 str2 =
(* if str1 and str2 are of the form [^0-9][0-9]+, we use the alphabetic
- order for the first part, and the numeric order for the second part.
+ order for the first part, and the numeric order for the second part.
nb : this is the case for node names generated by gg
*)
try
@@ -90,6 +90,27 @@ 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)
+
+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
+
+
let (do_graph_attr : attrs -> (Dot_ast.id * Dot_ast.id option) list -> attrs) =
fun acc l ->
let f acc = function
@@ -187,6 +208,18 @@ 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 ->
match t.nodes with
diff --git a/lib/sasacore/topology.mli b/lib/sasacore/topology.mli
index 4c711ae0..d1f82887 100644
--- a/lib/sasacore/topology.mli
+++ b/lib/sasacore/topology.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 20/09/2021 (at 09:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2023 (at 15:07) by Erwan Jahier> *)
(** {1 Topology: internal representation of Graphs } *)
@@ -25,6 +25,7 @@ val read: string -> t
(** {1 Various eponymous util functions } *)
val to_adjacency: t -> bool array array
+val to_distance: t -> int array array
val get_nb_link: t -> int
val get_mean_degree : t -> float
val is_connected : t -> bool
diff --git a/salut/src/dot2lus.ml b/salut/src/dot2lus.ml
index 2280ed18..4cee2817 100644
--- a/salut/src/dot2lus.ml
+++ b/salut/src/dot2lus.ml
@@ -13,32 +13,30 @@ let action_of_int = "action_of_int"
let clock = ref false
+
+let (array_to_string : ('a -> string) -> 'a array -> string) =
+ fun tostr a ->
+ let l = Array.fold_right (fun b acc -> (tostr b)::acc) a [] in
+ "["^(String.concat "," l)^"]"
+
+let (matrix_to_string : ('a -> string) -> 'a array array -> string) =
+ fun tostr m ->
+ let l = Array.fold_right (fun a acc -> (array_to_string tostr a)::acc) m [] in
+ "[\n\t"^(String.concat ",\n\t" l)^"]"
+
+
let algo_name (node : Topology.node) = Filename.remove_extension node.file
(* prints includes, graph constants and helper functions *)
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";
-
- (* 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 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);
@@ -54,7 +52,7 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
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"
@@ -75,22 +73,28 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
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 |> matrix_to_string);
+ (graph |> Topology.to_adjacency |> (matrix_to_string b2s));
+
+ Printf.fprintf lustre_const
+ "const distance = %s;\n"
+ (graph |> Topology.to_distance |> (matrix_to_string string_of_int));
(* State.lus File *)
output_string lustre_topology"
include \"state.lus\"";
-
+
(* Neighbors type *)
output_string lustre_topology "
type neigh = struct { state:state; reply:int; weight:int };\n";
-
+
(* helper functions *)
output_string lustre_topology "
function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int);
@@ -121,7 +125,7 @@ let output_topology lustre_topology (graph : Topology.t) name =
|> 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
| [] -> "[]"
@@ -133,28 +137,28 @@ let output_topology lustre_topology (graph : Topology.t) name =
Printf.fprintf lustre_topology
"\nnode %s(p : bool^%s^card; initials : %s^card)\n"
name action_number state_type;
-
+
Printf.fprintf lustre_topology
"returns (p_c : %s^card; Enab_p : bool^%s^card; round:bool; round_nb:int);\n"
state_type action_number;
-
+
output_string lustre_topology "var";
-
+
Printf.fprintf lustre_topology "\tprev_p_c : %s^card;\n\n" state_type;
graph.nodes
|> List.iteri (fun i _ -> Printf.fprintf lustre_topology "\tsel_%d : bool;\n" i);
-
+
output_string lustre_topology "let
round = round<<actions_number,card>>(Enab_p, p);
round_nb = round_count(round, legitimate<<actions_number,card>>(Enab_p,p_c));
";
-
+
output_string lustre_topology "\tprev_p_c = initials -> pre(p_c);\n\n";
graph.nodes
|> List.iteri (fun i _ ->
Printf.fprintf lustre_topology
- "\tsel_%d = false -> n_or<<%s>>(p[%d]);\n" i action_number i);
-
+ "\tsel_%d = false -> nary_or<<%s>>(p[%d]);\n" i action_number i);
+
let index_of_id = make_index graph in
graph.nodes
(*liste des noms des noeuds *)
@@ -176,7 +180,7 @@ let output_topology lustre_topology (graph : Topology.t) name =
Printf.fprintf lustre_topology
"\tEnab_p[%d] = %s_enable<<%d>>(p_c[%d], %s);\n"
i algo deg i nl);
-
+
Printf.fprintf lustre_topology "tel;\nnode topology = %s;\n%!" name
(*Generate a new state.lus file*)
@@ -226,7 +230,7 @@ let _ =
let usage = "salut <dotfile> [-o lusfile] [--clock] [--help]" in
let dotfile = ref "" in
let lusfile = ref "" in
-
+
let anon_parse arg =
match !dotfile with
| "" -> dotfile := arg
diff --git a/salut/test/kclustering/cost.lus b/salut/test/kclustering/cost.lus
index c9d2c121..2d345d81 100644
--- a/salut/test/kclustering/cost.lus
+++ b/salut/test/kclustering/cost.lus
@@ -1,33 +1,26 @@
include "p.lus"
const debug=false;
-function parentd<<const card:int;const n:int>>(p:state ; config:state^card) returns (parp:state);
+node heigth<<const i:int>>(dummy:bool) returns (res:int);
let
-parp=with (card=n) then config[card-1]
- else if p.par=n then config[n] else parentd<<card,(n+1)>>(p,config);
-tel
-
-node depth<<const card:int>> (p:state; config:state^card) returns (nat:int);
-var parp:state;
+ res = distance[0][i] ;
+tel;
+node sum_heigth<<const n:int>>(enabled : bool^1^n; config : state^n)
+returns (pf:int);
let
-parp=parentd<<card;0>>(p,config);
-nat= with (card=1) then 1
- else if isRoot(p) then 1 else 1+ depth<<card-1>>(parp,config[1..(card-1)]);
+ pf= with (n=1) then
+ if enabled[0][0] then
+ heigth<<0>>(true)+1
+ else
+ 0
+ else
+ if enabled[n-1][0] then
+ heigth<<n-1>>(true) + 1 +
+ sum_heigth<<n-1>>(enabled[0..(n-2)],config[0..(n-2)])
+ else sum_heigth<<n-1>>(enabled[0..(n-2)],config[0..(n-2)]);
tel
-node pot<<const card:int>>(p:state;config:state^card) returns (nat:int);
+node cost(enabled : bool^1^card; config : state^card) returns (res: int);
let
-nat= if p_enable<<n>>(p,config)= [true] then depth<<card>>(p,config) else 0;
+ res=sum_heigth<<card>>(enabled,config);
tel
-
-node sum<<const card:int>>(enabled : bool^actions_number^card; config : state^card) returns (pf:int);
-let
-pf= with (card=1) then if enabled[0][0]=true then depth<<card>>(config[0],config) else 0
- else if enabled[0][0]=true then depth<<card>>(config[0],config) + sum<<card-1>>(enabled[1..(card-1)],config[1..(card-1)])
- else sum<<card-1>>(enabled[1..(card-1)],config[1..(card-1)]);
-tel
-
-node cost(enabled : bool^actions_number^card; config : state^card) returns (res: int);
-let
-res=sum<<card>>(enabled,config);
-tel
\ No newline at end of file
diff --git a/salut/test/rsp_tree/tree4.lus b/salut/test/rsp_tree/tree4.lus
deleted file mode 100644
index cee55d51..00000000
--- a/salut/test/rsp_tree/tree4.lus
+++ /dev/null
@@ -1,77 +0,0 @@
--- automatically generated by salut
-include "p.lus"
-include "root.lus"
-
-
-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;
-
-function dot2lus_action_of_activation(activation : bool^actions_number) returns (action : action);
-let
- action = action_of_int(dot2lus_first_set<<actions_number>>(activation));
-tel;
-
-node tree4(p : bool^actions_number^card; initials : state^card)
-returns (p_c : state^card; Enab_p : bool^actions_number^card);
-var
- prev_p_c : state^card;
-
- sel_0 : bool;
- sel_1 : bool;
- sel_2 : bool;
- sel_3 : bool;
-let
- prev_p_c = initials -> pre(p_c);
-
- sel_0 = false -> boolred<<1,actions_number,actions_number>>(p[0]);
- sel_1 = false -> boolred<<1,actions_number,actions_number>>(p[1]);
- sel_2 = false -> boolred<<1,actions_number,actions_number>>(p[2]);
- sel_3 = false -> boolred<<1,actions_number,actions_number>>(p[3]);
-
- p_c[0] =
- if not sel_0 then prev_p_c[0]
- else root_step<<2>>(
- prev_p_c[0],
- [ prev_p_c[1], prev_p_c[2] ],
- dot2lus_action_of_activation(p[0])
- );
- Enab_p[0] = root_enable<<2>>(p_c[0], [ p_c[1], p_c[2] ]);
-
- p_c[1] =
- if not sel_1 then prev_p_c[1]
- else p_step<<2>>(
- prev_p_c[1],
- [ prev_p_c[0], prev_p_c[3] ],
- dot2lus_action_of_activation(p[1])
- );
- Enab_p[1] = p_enable<<2>>(p_c[1], [ p_c[0], p_c[3] ], [0,0]);
-
- p_c[2] =
- if not sel_2 then prev_p_c[2]
- else p_step<<1>>(
- prev_p_c[2],
- [ prev_p_c[0] ],
- dot2lus_action_of_activation(p[2])
- );
- Enab_p[2] = p_enable<<1>>(p_c[2], [ p_c[0] ],[1]);
-
- p_c[3] =
- if not sel_3 then prev_p_c[3]
- else p_step<<1>>(
- prev_p_c[3],
- [ prev_p_c[1] ],
- dot2lus_action_of_activation(p[3])
- );
- Enab_p[3] = p_enable<<1>>(p_c[3], [ p_c[1] ],[1]);
-tel;
-node topology = tree4;
diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh
index aa7ec28e..4543ab4b 100755
--- a/salut/test/run-kind2.sh
+++ b/salut/test/run-kind2.sh
@@ -1,5 +1,5 @@
#!/bin/bash
-#set -x
+set -x
GITROOT=$(git rev-parse --show-toplevel)
LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/daemon.lus"
@@ -100,7 +100,7 @@ fi
kind2_opt="--timeout 36000 -json -v "
kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
-kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 36000 $@"
+kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 10000 $@"
# --qe_method {precise|impl|cooper}
@@ -116,25 +116,30 @@ cp ${LIB_LUS} ${TMP}
cd ${TMP}
make $main.dot || [ -f $main.dot ] || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
+start0=`date +%s.%N`
salut $main.dot
# Get rif of the lutre v6 constructs that kind2 does not handle
-lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -knc -o $main.verify.lv4
+lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -knpc -o $main.verify.lv4
# set the property to check
-sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY $prop;\ntel/" $main.verify.lv4
+cat $main.verify.lv4 | grep -v "\-\-" | sed -e "$ s/\(.*\)tel$/--%MAIN ;\n--%PROPERTY $prop;\ntel/g" > $main.verify.lv4.tmp
+mv $main.verify.lv4.tmp $main.verify.lv4
+# sed -i -e "$s/\(.*\)tel/--%MAIN ;\n--%PROPERTY $prop;\ntel/" $main.verify.lv4
+
+# using machine integers instead of int: eg, replace 42 by (uint8 42)
-# using machine integers instead of int
cat $main.verify.lv4 | \
- sed -r "s/[ =](\[)?((-)?[[:digit:]]+)/ \1(${int} \2)/g" | \
- sed -r "s/\(((-)?[[:digit:]]+)\)/(${int} \1)/g" | \
+ sed -r "s/([ \t\r\n=([<>\/\*\+]+)((-)?[[:digit:]]+)/ \1(${int} \2)/g" | \
sed -r "s/:int/:${int}/g" \
> $main.verify.${int}.lv4
+
start=`date +%s.%N`
time kind2 --color true ${kind2_opt} $main.verify.${int}.lv4
end=`time date +%s.%N`
+wallclock0=$( echo "$end - $start0" | bc -l )
wallclock=$( echo "$end - $start" | bc -l )
timestamp=`date +"%d/%m/%Y-%H:%M:%S"`
@@ -146,7 +151,7 @@ LC_NUMERIC="en_US.UTF-8"
# let's keep a track of all runs (it can expensive, it should not be lost)
# in a .org file
ALL_RESULT="${GITROOT}/salut/test/kind2-result-`uname -n`.org"
-printf "| %s | %s | %s | %s | %.2f | %s | %s | %s | %s |\n" $algo ${topology} ${size} \
- $prop $wallclock $int $solver $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}
+printf "| %s | %s | %s | %s | %.2f-%.2f | %s | %s | %s | %s |\n" $algo ${topology} ${size} \
+ $prop $wallclock0 $wallclock $int $solver $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}
echo "cf ${ALL_RESULT}"
\ No newline at end of file
--
GitLab