From e76ba20335e9496e6226797c4555bdbb3d49cc14 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 5 Jul 2019 11:37:25 +0200
Subject: [PATCH] Update: enhance the oracle generation (-glos)
The generation scheme is now makes it easier to write oracles that do
not depend on the topology. The idea is to generate an oracle
(specific to the graph) that includes a file that the user should
provide, and which ougth to define a generic oracle, i.e., depending
on m and n (process and actions numbers).
---
lib/sasacore/genOracle.ml | 47 +++++++++++++++++++--------------
test/bfs-spanning-tree/Makefile | 15 +++++++----
test/lustre/round.lus | 12 ++++-----
3 files changed, 43 insertions(+), 31 deletions(-)
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index 1510f64f..f02599a0 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 f28ef9a0..f1cfbb42 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 9f32e43b..9cbb3388 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
--
GitLab