diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml index 7b42c8e9cbde0fbf17f8e6057248898a156b9f84..efc23cde826f722ed5317da32a619de9b22b46fb 100644 --- a/lib/sasacore/genOracle.ml +++ b/lib/sasacore/genOracle.ml @@ -1,19 +1,9 @@ -(* Time-stamp: <modified the 16/01/2023 (at 16:14) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/06/2023 (at 11:51) by Erwan Jahier> *) open Process let b2s b = if b then "t" else "f" -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 already_defined = function (* some attributes may already be defined *) | "links_number" | "max_degree" @@ -120,6 +110,7 @@ const is_a_tree=%b; const f=false; const t=true; const adjacency=%s; +const distance=%s; %s node oracle(legitimate:bool;%s%s) \nreturns (ok:bool); var @@ -140,7 +131,8 @@ tel (Register.is_cyclic ()) (Register.is_connected ()) (Register.is_tree ()) - (matrix_to_string (Topology.to_adjacency g)) + (StringOf.matrix_lv6 b2s (Topology.to_adjacency g)) + (StringOf.matrix_lv6 string_of_int (Topology.to_distance g)) (graph_attributes_to_string ()) (if Register.get_potential () = None then "" else "potential:real; ") input_decl diff --git a/lib/sasacore/stringOf.ml b/lib/sasacore/stringOf.ml index 779094abb19291459bbec4abb29bbba94bb31308..17e81d6d302cc7edc68c345b4bc5b1c603a86647 100644 --- a/lib/sasacore/stringOf.ml +++ b/lib/sasacore/stringOf.ml @@ -9,7 +9,7 @@ open Process let (env: 'v Conf.t -> 'v Process.t list -> string) = fun env pl -> let value_to_string = Register.get_value_to_string () in - let l = List.map + let l = List.map (fun p -> Printf.sprintf "%s: %s" p.pid (value_to_string (Conf.get env p.pid))) @@ -20,7 +20,7 @@ let (env: 'v Conf.t -> 'v Process.t list -> string) = let (env_rif: 'v Conf.t -> 'v Process.t list -> string) = fun env pl -> - let l = List.map + let l = List.map (fun p -> Printf.sprintf "%s" (SasaState.to_rif_data (Conf.get env p.pid))) pl @@ -39,3 +39,13 @@ let action str = let str = Str.global_replace (Str.regexp "[[]") "" str in let str = Str.global_replace (Str.regexp "[]]") "" str in str + +let (array_lv6 : ('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_lv6 : ('a -> string) -> 'a array array -> string) = + fun tostr m -> + let l = Array.fold_right (fun a acc -> (array_lv6 tostr a)::acc) m [] in + "[\n\t"^(String.concat ",\n\t" l)^"]" diff --git a/salut/src/dot2lus.ml b/salut/src/dot2lus.ml index 4cee2817e77585990bbc599aa9fba035a01337f1..fa0da192d9657d1fb557e0cd10a5e947d3bdc769 100644 --- a/salut/src/dot2lus.ml +++ b/salut/src/dot2lus.ml @@ -13,18 +13,6 @@ 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) = @@ -81,11 +69,11 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) = 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 b2s)); + (graph |> Topology.to_adjacency |> (StringOf.matrix_lv6 b2s)); Printf.fprintf lustre_const "const distance = %s;\n" - (graph |> Topology.to_distance |> (matrix_to_string string_of_int)); + (graph |> Topology.to_distance |> (StringOf.matrix_lv6 string_of_int)); (* State.lus File *) output_string lustre_topology" diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc index 2b298c840669349eeeccea14124de5f9aec8f9a3..4e23bfb43eb770798f7e465e50c68f5f36da50c7 100644 --- a/salut/test/Makefile.inc +++ b/salut/test/Makefile.inc @@ -73,8 +73,7 @@ endif # replace int by int8 (for kind2) %.verify.int8.lv4: %.verify.lv4 cat $^ | \ - sed -r "s/[ =](\[)?((-)?[[:digit:]]+)/ \1(int8 \2)/g" | \ - sed -r "s/\(((-)?[[:digit:]]+)\)/(int8 \1)/g" | \ + sed -r "s/([ \t\r\n=([<>\/\*\+]+)((-)?[[:digit:]]+)/ \1(int8 \2)/g" | \ sed -r "s/:int/:int8/g" \ > $@ @@ -103,7 +102,7 @@ endif %.lurette: make $*.dot $*_const.lus $*.cmxs $*_oracle.lus - lurette -sut "sasa -seed 172317971 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec" + lurette -sut "sasa -seed 172317971 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec" # ditto, without a seed %.lurette_no_seed: diff --git a/salut/test/kclustering/Makefile b/salut/test/kclustering/Makefile index fbaf683d283d75f87ab5de4a8f4a4cc753f4cbf9..96b50dd55f2c4b052160bc0b486cffdf22dd76a5 100644 --- a/salut/test/kclustering/Makefile +++ b/salut/test/kclustering/Makefile @@ -1,4 +1,4 @@ -TOPOLOGY ?= tree5 +TOPOLOGY ?= rtree5 DOT2LUSFLAGS ?= SASA_ALGOS := p.ml DECO_PATTERN="0-:p.ml" @@ -9,7 +9,7 @@ include ../Makefile.dot ############################################################################## # Non-regression tests -test: tree3.kind2-test tree3.lurette #lesar not work because of the modulo. +test: rtree3.kind2-test rtree3.lurette #lesar not work because of the modulo. clean: genclean rm -f $(TOPOLOGY)*.* tree3*.*