Skip to content
Snippets Groups Projects
Commit 5a2eef37 authored by erwan's avatar erwan
Browse files

test: add missing static args to oracles (now lv6 report such errors)

parent e5541fa3
No related branches found
No related tags found
No related merge requests found
...@@ -23,7 +23,8 @@ let ...@@ -23,7 +23,8 @@ let
(i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn]))); (i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
tel 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); returns (res:bool);
let let
res = redge(Legitimate) => (round_nb <= diameter*card); res = redge(Legitimate) => (round_nb <= diameter*card);
......
...@@ -37,14 +37,13 @@ tel ...@@ -37,14 +37,13 @@ tel
function first_element<<const an : int>> (X:bool^an) returns (res:bool); function first_element<<const an : int>> (X:bool^an) returns (res:bool);
let let
res = X[0]; res = X[0];
tel tel
function first_column<<const an : int; const pn: int>>(X:bool^an^pn) returns (Z:bool^pn); function first_column<<const an : int; const pn: int>>(X:bool^an^pn) returns (Z:bool^pn);
let let
Z = map<<first_element<<an>>,pn>>(X); Z = map<<first_element<<an>>,pn>>(X);
tel tel
function all_CD_are_false (tab_enab:bool^an^pn) returns (res:bool); function all_CD_are_false (tab_enab:bool^an^pn) returns (res:bool);
let let
res = not (red<<or,pn>>(false,first_column(tab_enab))) ; res = not (red<<or,pn>>(false,first_column<<an,pn>>(tab_enab))) ;
tel tel
----------------------------------------------------------------------------- -----------------------------------------------------------------------------
...@@ -19,7 +19,8 @@ let ...@@ -19,7 +19,8 @@ let
res = state { st=intVstatus(st); par=par; d=d }; res = state { st=intVstatus(st); par=par; d=d };
tel; 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); returns (res:bool);
var var
Silent:bool; Silent:bool;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment