From 5a2eef37b9e47465e8a4ef87aa24cde4d430c67c Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Fri, 9 Feb 2024 10:38:43 +0100
Subject: [PATCH] test: add missing static args to oracles (now lv6 report such
errors)
---
test/async-unison/async_unison_oracle.lus | 3 ++-
test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus | 7 +++----
test/rsp-tree/rsp_tree_oracle.lus | 3 ++-
3 files changed, 7 insertions(+), 6 deletions(-)
diff --git a/test/async-unison/async_unison_oracle.lus b/test/async-unison/async_unison_oracle.lus
index e3203a08..9373c160 100644
--- a/test/async-unison/async_unison_oracle.lus
+++ b/test/async-unison/async_unison_oracle.lus
@@ -23,7 +23,8 @@ let
(i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
tel
-node async_unison_oracle (Legitimate:bool; pot:real;Enab, Acti: bool^an^pn; State : int^pn; round:bool; round_nb:int)
+node async_unison_oracle<<const an:int; const pn:int>>
+ (Legitimate:bool; pot:real;Enab, Acti: bool^an^pn; State : int^pn; round:bool; round_nb:int)
returns (res:bool);
let
res = redge(Legitimate) => (round_nb <= diameter*card);
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 541fcd60..5d3dafd8 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -37,14 +37,13 @@ tel
function first_element<<const an : int>> (X:bool^an) returns (res:bool);
let
res = X[0];
-tel
+tel
function first_column<<const an : int; const pn: int>>(X:bool^an^pn) returns (Z:bool^pn);
let
- Z = map<<first_element<<an>>,pn>>(X);
+ Z = map<<first_element<<an>>,pn>>(X);
tel
function all_CD_are_false (tab_enab:bool^an^pn) returns (res:bool);
let
- res = not (red<<or,pn>>(false,first_column(tab_enab))) ;
+ res = not (red<<or,pn>>(false,first_column<<an,pn>>(tab_enab))) ;
tel
-----------------------------------------------------------------------------
-
diff --git a/test/rsp-tree/rsp_tree_oracle.lus b/test/rsp-tree/rsp_tree_oracle.lus
index 2810aee2..a2dc8c9c 100644
--- a/test/rsp-tree/rsp_tree_oracle.lus
+++ b/test/rsp-tree/rsp_tree_oracle.lus
@@ -19,7 +19,8 @@ let
res = state { st=intVstatus(st); par=par; d=d };
tel;
-node rsp_tree_oracle(legit:bool; Enab, Acti:bool^an^pn; config: state^pn; round:bool; round_nb:int)
+node rsp_tree_oracle<<const an:int; const pn:int>>
+(legit:bool; Enab, Acti:bool^an^pn; config: state^pn; round:bool; round_nb:int)
returns (res:bool);
var
Silent:bool;
--
GitLab