From ea1f7e819f128cefb72db2a42b6de0df778ff8f8 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 10 Jul 2023 11:13:32 +0200
Subject: [PATCH] test: the order of variables in to_state (<dir>_oracle.lus)
should be the same as the one used in State.to_string (in state.ml)
---
lib/sasacore/genOracle.ml | 44 +++++++++++++++----
salut/test/Makefile.inc | 7 +++
salut/test/bfs-spanning-tree/Makefile | 4 +-
.../bfs_spanning_tree_oracle.lus | 44 ++++++++++++++-----
salut/test/kclustering/kclustering_oracle.lus | 24 +++++-----
salut/test/rsp_tree/rsp_tree_oracle.lus | 18 ++++----
6 files changed, 98 insertions(+), 43 deletions(-)
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index efc23cde..936a7b24 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/06/2023 (at 11:51) by Erwan Jahier> *)
+(* Time-stamp: <modified the 10/07/2023 (at 10:57) by Erwan Jahier> *)
open Process
@@ -44,7 +44,7 @@ let (f: Topology.t -> string option -> 'v Process.t list -> string) =
List.fold_left
(fun acc p ->
let l = SasaState.to_rif_decl p.pid p.init in
- List.fold_left (fun acc (n,t) -> (n, Data.type_to_string t)::acc) acc l
+ List.fold_left (fun acc (n,t) -> (n, Data.type_to_string t)::acc) acc (List.rev l)
)
[]
(List.rev pl)
@@ -79,13 +79,15 @@ let (f: Topology.t -> string option -> 'v Process.t list -> string) =
match vars_list with
| []->""
| e::[]->(Printf.sprintf "%s) " e)
- | e::tail-> (if (count mod struct_nb_var) = 0 then
- (Printf.sprintf "to_state(%s, " e ) ^ (struct_string tail (count-1))
- else if (count mod struct_nb_var) = 1 then
- (Printf.sprintf "%s), " e) ^ (struct_string tail (count-1))
- else
- (Printf.sprintf "%s, " e) ^ (struct_string tail (count-1))
- ) in
+ | e::tail-> (
+ if (count mod struct_nb_var) = 0 then
+ (Printf.sprintf "to_state(%s, " e ) ^ (struct_string tail (count-1))
+ else if (count mod struct_nb_var) = 1 then
+ (Printf.sprintf "%s), " e) ^ (struct_string tail (count-1))
+ else
+ (Printf.sprintf "%s, " e) ^ (struct_string tail (count-1))
+ )
+ in
Printf.sprintf "\tConfig = [%s];\n" (struct_string (List.map fst vars) vars_nb)
else
Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
@@ -118,6 +120,20 @@ var
%s %s %s
ok = %s_oracle(legitimate,%s Enab, Acti, Config, round, round_nb);
tel
+
+
+node oracle_debug(legitimate:bool;%s%s) \nreturns (ok:bool;
+ lustre_config : state^card;
+ lustre_enabled : bool^actions_number^card;
+-- lustre_cost:int;
+ lustre_round:bool;
+ lustre_round_nb:int;
+%s
+);
+let
+ %s %s %s
+ ok, lustre_config, lustre_enabled,lustre_round,lustre_round_nb = %s_oracle_debug(legitimate,%s Enab, Acti, Config, round, round_nb);
+tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
algo
@@ -134,6 +150,16 @@ tel
(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
+ array_decl
+ array_def_acti
+ array_def_enab
+ array_def_config
+ algo
+ (if Register.get_potential () = None then "" else "potential,")
+
(if Register.get_potential () = None then "" else "potential:real; ")
input_decl
array_decl
diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc
index f811dc9a..c279f534 100644
--- a/salut/test/Makefile.inc
+++ b/salut/test/Makefile.inc
@@ -67,6 +67,13 @@ endif
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"
+# ditto, but using nodes where all locals are outputs
+# provided that <xxx>_oracle.lus define a <xxx>_oracle_debug node
+# (cf, e.g., salut/test/ring-orientation/ring_orientation_oracle.lus)
+%.lurette.debug:
+ make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
+ lurette -sut "sasa -seed 172317971 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle_debug -exec"
+
# ditto, without a seed
%.lurette_no_seed:
make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
diff --git a/salut/test/bfs-spanning-tree/Makefile b/salut/test/bfs-spanning-tree/Makefile
index f6d19367..9b1fa683 100644
--- a/salut/test/bfs-spanning-tree/Makefile
+++ b/salut/test/bfs-spanning-tree/Makefile
@@ -10,9 +10,9 @@ include ./Makefile.dot
##############################################################################
# Non-regression tests
-test: tree3.lurette
+test: tree13.lurette
$(RUN_KIND2) tree 3 closure
- $(RUN_KIND2) tree 2 theorem
+ $(RUN_KIND2) tree 2 theorem
clean: genclean
diff --git a/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 1e0cae5f..3b350dd9 100644
--- a/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -1,22 +1,22 @@
-- Here, we use the Lustre version of the algorithm as a test oracle for the ocaml version
-
+
include "../../lib/utils.lus"
-function to_state( par:int ; d:int)
+function to_state(d:int; par:int)
returns(res : state);
let
- res = state { par=par; d=d };
+ res = state { d=d ; par=par };
tel;
node bfs_spanning_tree_oracle(
legitimate : bool;
ocaml_enabled : bool^actions_number^card;
- active : bool^actions_number^card;
- ocaml_config : state^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
round:bool;
- round_nb:int;
-)
+ round_nb:int;
+)
returns (ok : bool);
var
lustre_config : state^card;
@@ -24,14 +24,38 @@ var
lustre_round:bool;
lustre_round_nb:int;
let
- lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+ ok, lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+ bfs_spanning_tree_oracle_debug(legitimate, ocaml_enabled,active, ocaml_config, round, round_nb);
+
+tel;
+
+node toto(d:state^2) returns (nd:state^2);
+let
+ nd=d -> pre nd;
+tel;
+
+node bfs_spanning_tree_oracle_debug(
+ legitimate : bool;
+ ocaml_enabled : bool^actions_number^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
+ round:bool;
+ round_nb:int;
+)
+returns (ok : bool;
+ lustre_config : state^card;
+ lustre_enabled : bool^actions_number^card;
+ lustre_round:bool;
+ lustre_round_nb:int);
+let
+ lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
- ok = lustre_enabled = ocaml_enabled
+ ok = lustre_enabled = ocaml_enabled
-- compare the sasa dot interpretation and the salut dot to lustre compilation
and lustre_config = ocaml_config
-- and lustre_round = round
- and lustre_round_nb = round_nb
+ and lustre_round_nb = round_nb
;
tel
diff --git a/salut/test/kclustering/kclustering_oracle.lus b/salut/test/kclustering/kclustering_oracle.lus
index 451322b5..7ac783b2 100644
--- a/salut/test/kclustering/kclustering_oracle.lus
+++ b/salut/test/kclustering/kclustering_oracle.lus
@@ -1,9 +1,9 @@
-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
-
+
include "../../lib/utils.lus"
include "cost.lus"
-function to_state(par:int; alpha:int; isRoot:bool)
+function to_state(isRoot:bool; alpha:int; par:int)
returns ( res : state);
let
res = state { isRoot=isRoot; par=par; alpha=alpha };
@@ -13,11 +13,11 @@ node kclustering_oracle(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
- active : bool^actions_number^card;
- ocaml_config : state^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
round : bool;
- round_nb : int;
-)
+ round_nb : int;
+)
returns (ok : bool);
var
lustre_cost:int;
@@ -26,20 +26,18 @@ var
lustre_round:bool;
lustre_round_nb:int;
let
- lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+ lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
lustre_cost = cost(lustre_enabled, lustre_config);
- ok = lustre_enabled = ocaml_enabled
+ ok = lustre_enabled = ocaml_enabled
-- compare the sasa dot interpretation and the salut dot to lustre compilation
- and lustre_config = ocaml_config
+ and lustre_config = ocaml_config
-- and lustre_round = round
- and lustre_round_nb = round_nb
+ and lustre_round_nb = round_nb
-- compare the lustre and the ocaml version of the processes
-- and Lustre::real2int(ocaml_cost) = lustre_cost
- -- compare the cost functions
+ -- compare the cost functions
;
tel
-
-
diff --git a/salut/test/rsp_tree/rsp_tree_oracle.lus b/salut/test/rsp_tree/rsp_tree_oracle.lus
index 6b825f28..0a3d066d 100644
--- a/salut/test/rsp_tree/rsp_tree_oracle.lus
+++ b/salut/test/rsp_tree/rsp_tree_oracle.lus
@@ -1,5 +1,5 @@
-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
-
+
include "../../lib/utils.lus"
function intVstatus (i:int)
@@ -11,7 +11,7 @@ let
else EF;
tel;
-function to_state( d:int; par:int; st:int)
+function to_state( st:int; par:int; d:int)
returns ( res : state);
let
res = state { st=intVstatus(st); par=par; d=d };
@@ -20,11 +20,11 @@ tel;
node rsp_tree_oracle(
legitimate : bool;
ocaml_enabled : bool^actions_number^card;
- active : bool^actions_number^card;
- ocaml_config : state^card;
+ active : bool^actions_number^card;
+ ocaml_config : state^card;
round : bool;
round_nb : int;
-)
+)
returns (ok : bool);
var
lustre_config : state^card;
@@ -32,15 +32,15 @@ var
lustre_round:bool;
lustre_round_nb:int;
let
- lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+ lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
- ok = lustre_enabled = ocaml_enabled
+ ok = lustre_enabled = ocaml_enabled
-- compare the sasa dot interpretation and the salut dot to lustre compilation
and lustre_config = ocaml_config
-- and lustre_round = round
--- and lustre_round_nb = round_nb
+-- and lustre_round_nb = round_nb
;
- -- compare the lustre and the ocaml version of the processes
+ -- compare the lustre and the ocaml version of the processes
tel
--
GitLab