diff --git a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus index ad2f064f40601fb5855c7f3fb6a699d5fde10ceb..28e934104e47b00577772a288b365d5d4678bd83 100644 --- a/test/st-KK06-algo2/st_KK06_algo2_oracle.lus +++ b/test/st-KK06-algo2/st_KK06_algo2_oracle.lus @@ -5,12 +5,12 @@ type state = int; const bigN = 2*card; -node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int) +node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; potential: real;Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int) returns (ok:bool); var moves : int; let --- Theorem 5. Algorithm 2 stabilizes in O(N n diam(G)) moves. +-- Theorem 5. Algorithm 2 stabilizes in O(N n diam(G)) moves. moves = count_move<<an,pn>>(Acti); ok = moves <= bigN * card * diameter ; tel \ No newline at end of file