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

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
parent d5bd7f84
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
lib/sasacore/topology.ml
+ 35
− 2
View file @ ff0da052
(* 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
......
lib/sasacore/topology.mli
+ 2
− 1
View file @ ff0da052
(* 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
......
salut/src/dot2lus.ml
+ 35
− 31
View file @ ff0da052
......@@ -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
......
salut/test/kclustering/cost.lus
+ 17
− 24
View file @ ff0da052
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
salut/test/rsp_tree/tree4.lus deleted 100644 → 0
+ 0
− 77
View file @ d5bd7f84
-- 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;
salut/test/run-kind2.sh
+ 14
− 9
View file @ ff0da052
#!/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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment