From e4bc28bc2c80cccec8a5f53ae6f671dcfde07870 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 11 May 2022 11:38:21 +0200
Subject: [PATCH] feat: give to the oracles the configuration, and the
potential when available
---
lib/sasacore/genOracle.ml | 24 +++++++++++++++------
test/async-unison/async_unison_oracle.lus | 10 ++++-----
test/st-KK06-algo1/st_KK06_algo1_oracle.lus | 2 +-
test/st-KK06-algo2/st_KK06_algo2_oracle.lus | 2 +-
test/unison/unison_oracle.lus | 2 +-
5 files changed, 25 insertions(+), 15 deletions(-)
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index dae26d6a..5444efb8 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 28/07/2021 (at 11:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/05/2022 (at 11:18) by Erwan Jahier> *)
open Process
@@ -54,16 +54,20 @@ let (f: Topology.t -> '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 l
)
[]
(List.rev pl)
in
- let input_state = "\n "^(String.concat ";" vars) in
+ let vars_decl = List.map (fun (v,t)-> v^":"^t) vars in
+ let input_state = "\n "^(String.concat ";" vars_decl) in
let input_trig = ";\n "^(String.concat "," al) ^ ":bool" in
let input_enab = ";\n "^(String.concat "," enabl) ^ ":bool" in
let input_decl = input_state^input_enab^input_trig in
- let array_decl = Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n" in
+ let array_decl =
+ Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:%s^pn;\n"
+ (fst (List.hd vars))
+ in
let acti_name p a = Printf.sprintf "%s_%s" p.pid (StringOf.action a) in
let enab_name p a = Printf.sprintf "Enab_%s_%s" p.pid (StringOf.action a) in
let array_def_acti =
@@ -78,6 +82,9 @@ let (f: Topology.t -> 'v Process.t list -> string) =
(List.map (fun p ->
"["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
in
+ let array_def_config =
+ Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
+ in
let algo = Filename.basename (Sys.getcwd()) in
let algo = StringOf.action algo in
Printf.sprintf "%sinclude \"%s_oracle.lus\"
@@ -96,11 +103,11 @@ const f=false;
const t=true;
const adjacency=%s;
%s
-node oracle(legitimate:bool; %s) \nreturns (ok:bool);
+node oracle(legitimate:bool;%s%s) \nreturns (ok:bool);
var
%slet
- %s %s
- ok = %s_oracle(legitimate, Enab, Acti);
+ %s %s %s
+ ok = %s_oracle(legitimate,%s Enab, Acti, Config);
tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
@@ -117,10 +124,13 @@ tel
(Register.is_tree ())
(matrix_to_string (Topology.to_adjacency 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,")
diff --git a/test/async-unison/async_unison_oracle.lus b/test/async-unison/async_unison_oracle.lus
index 3b80aebb..355905fa 100644
--- a/test/async-unison/async_unison_oracle.lus
+++ b/test/async-unison/async_unison_oracle.lus
@@ -9,7 +9,7 @@ let
tel
-- all neigbhbors are close
-function is_stable<<const l:int>>(State : int^pn) returns (res:bool)
+function is_legitimate<<const l:int>>(State : int^pn) returns (res:bool)
var
i,j:int;
let
@@ -17,16 +17,16 @@ let
j = l mod pn;
res =
with l = 0 then true
- else is_stable<<l-1>>(State) and
+ else is_legitimate<<l-1>>(State) and
(i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
tel
node async_unison_oracle (State : int^pn; Enab, Acti: bool^an^pn)
-returns (res, Stable:bool; rn:int);
+returns (res, Legitimate:bool; rn:int);
let
rn = count(round <<an,pn>>(Enab,Acti));
- Stable = is_stable <<pn*pn-1>>(State);
- res = redge(Stable) => (rn <= diameter*card);
+ Legitimate = is_legitimate <<pn*pn-1>>(State);
+ res = redge(Legitimate) => (rn <= diameter*card);
tel
node redge(x:bool) returns (res:bool);
diff --git a/test/st-KK06-algo1/st_KK06_algo1_oracle.lus b/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
index 0dd7978b..53d844d4 100644
--- a/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
+++ b/test/st-KK06-algo1/st_KK06_algo1_oracle.lus
@@ -2,7 +2,7 @@
include "../lustre/utils.lus"
node st_KK06_algo1_oracle<<const an:int; const pn:int>>
-(legitimate:bool; Enab,Acti:bool^an^pn) returns (ok:bool);
+(legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn) returns (ok:bool);
var
moves : int;
let
diff --git a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
index 4ae13435..d77ada0c 100644
--- a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
+++ b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus
@@ -3,7 +3,7 @@ include "../lustre/utils.lus"
const bigN = 2*card;
-node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn)
+node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn)
returns (ok:bool);
var
moves : int;
diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus
index 8b335998..861e7456 100644
--- a/test/unison/unison_oracle.lus
+++ b/test/unison/unison_oracle.lus
@@ -26,7 +26,7 @@ let
tel
-----------------------------------------------------------------------------
-node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn)
+node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn; Config:int^pn)
returns (ok:bool);
let
--
GitLab