diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index 1510f64fe617c7d71c0781c3d6483ec2b9c77b31..f02599a00e6c021f2b68db827ed46c3f9d8d9b96 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,17 +1,18 @@
-(* Time-stamp: <modified the 26/06/2019 (at 12:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 05/07/2019 (at 11:30) by Erwan Jahier> *)
open Process
let (f: 'v Process.t list -> string) =
fun pl ->
- let degree = 0 in
- let diameter = 0 in
+ let degree = Register.max_degree () in
+ let diameter = Register.diameter () in
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
-
- let al = List.flatten (List.map (fun p -> List.map (fun a -> p.pid^"_"^a) p.actions) pl) in
+
+ let al = List.map (fun p -> List.map (fun a -> p.pid^"_"^a) p.actions) pl in
+ let al = List.flatten al in
let enabl = List.map (fun a -> "Enab_"^a) al in
let input_decl = (String.concat ","(al@enabl)) ^ ":bool" in
let array_decl = Printf.sprintf "\tActi:bool^%d^%d;\n\tEnab:bool^%d^%d;\n" m n m n in
@@ -20,33 +21,39 @@ let (f: 'v Process.t list -> string) =
let array_def_acti =
Printf.sprintf "\tActi = [%s];\n"
(String.concat ","
- (List.map (fun p -> "["^(String.concat "," (List.map (acti_name p) p.actions))^"]") pl))
+ (List.map (fun p ->
+ "["^(String.concat "," (List.map (acti_name p) p.actions))^"]") pl))
in
let array_def_enab =
Printf.sprintf "\tEnab = [%s];\n"
(String.concat ","
- (List.map (fun p -> "["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
+ (List.map (fun p ->
+ "["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
+ in
+ let algo = Filename.basename (Sys.getcwd()) in
+ let algo = (* Make sure that we generate valid Lustre idents *)
+ Str.global_replace (Str.regexp "[-,\\.]") "_" algo
in
- Printf.sprintf "%sconst n=%d;
+ Printf.sprintf "%sinclude \"%s_oracle.lus\"
+const n=%d;
const m=%d;
const degree=%d;
const diameter=%d;
-
node oracle(%s) returns (ok:bool);
var
%slet
- %s
- %s
- ok = false; -- XXX set me !
+ %s %s
+ ok = %s_oracle<<m,n>>(Enab,Acti);
tel
"
- (Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
- n m degree diameter
- input_decl
- array_decl
- array_def_acti
- array_def_enab
-
-
+ (Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
+ algo
+ n m degree diameter
+ input_decl
+ array_decl
+ array_def_acti
+ array_def_enab
+ algo
+
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index f28ef9a055ad72d839625ea8c80d29f7852931ea..f1cfbb4242be0e68ee94af09e4e23f7805f0df53 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 26/06/2019 (at 14:50) by Erwan Jahier>
+# Time-stamp: <modified the 05/07/2019 (at 11:09) by Erwan Jahier>
test: test0 test2 lurette0 lurette1
@@ -31,11 +31,11 @@ lurette0:cmxs fig5.1-noinit.lut
-env "$(sasa) fig5.1-noinit.dot -custd -rif" \
-sut "lutin fig5.1-noinit.lut -n distributed"
-lurette1:cmxs fig5.1-noinit.lut
+lurette1:cmxs fig5.1.lut
rdbg -lurette -o lurette.rif \
- -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
- -sut "lutin fig5.1-noinit.lut -n distributed" \
- -oracle "lv6 fig5.1-noinit_oracle.lus -n oracle"
+ -env "$(sasa) fig5.1.dot -custd -rif" \
+ -sut "lutin fig5.1.lut -n distributed" \
+ -oracle "lv6 fig5.1_oracle.lus -n oracle"
lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null
@@ -46,6 +46,11 @@ rdbg: cmxs fig5.1-noinit.lut
-env "$(sasa) fig5.1-noinit.dot -custd -rif" \
-sut-nd "lutin fig5.1-noinit.lut -n distributed"
+rdbg2: cmxs fig5.1.lut
+ rdbg -o lurette.rif \
+ -env "$(sasa) fig5.1.dot -custd -rif" \
+ -sut-nd "lutin fig5.1.lut -n distributed"
+
manual:cmxs fig5.1-noinit.lut
lurette -o lurette.rif --sim2chro \
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index 9f32e43ba6f9c870606bcde83fbc4febbc319aeb..9cbb3388c11b49ec005dc2bcb130739af90f9e4f 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -1,4 +1,4 @@
--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+-- -- Time-stamp: <modified the 05/07/2019 (at 11:34) by Erwan Jahier>
--
-- Computing rounds in Lustre
-- The inputs are 2 arrays Enab and Acti, where:
@@ -14,12 +14,11 @@ var
let
pres = true -> pre res;
mask = merge pres (true -> mask_init<<m, n>> (Enab, Acti) when pres)
- (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
-
+ (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
res = boolred<<0,0,n>>(mask); -- when all are false,
tel
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+function mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
var
enab:bool^n; -- at least one action is enabled
acti:bool^n; -- at least one action is active
@@ -34,7 +33,8 @@ let
res = not(a=>b);
tel
-node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
+function mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n)
+returns (res : bool^n);
var
acti:bool^n; -- at least one action is active
let
@@ -53,7 +53,7 @@ let
tel
-----------------------------------------------------------------------------
-node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
+function silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
var
enab:bool^n; -- at least one action is enabled
let