diff --git a/test/async-unison/async_unison_oracle.lus b/test/async-unison/async_unison_oracle.lus index e3203a0882847df3f459cd93b242eb95b0321e17..9373c1609736e690f5a6538c6e1b84d8668e2a16 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 541fcd6073ea412385a81ed07b29edfeff4e009d..5d3dafd862d50bda20273f29f99a88f817805a5c 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 2810aee24b705dd2cd1d933ab34b8795edecbe12..a2dc8c9c582b319aa1cfdfc48b637ec00e5462d4 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;