unison_oracle.lus

include "../lustre/oracle_utils.lus"

-----------------------------------------------------------------------------
node theorem_4_11<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) 
returns (res:bool);
var
  nb_step:int;
  All_Acti:bool;
let
  nb_step = 1 -> pre(nb_step) + 1 ; 
  All_Acti = all_true<<an,pn>>(Acti);
  res = (((2*diameter-1)>= (2*diameter-1)) and is_connected) 
         => (nb_step>=(3*diameter-2)) => All_Acti  ; -- Theorem 4.11 page 40 
tel

-----------------------------------------------------------------------------
node lemma_4_10<<const an: int; const pn:int>> (Enab, Acti: bool^an^pn) 
returns (res:bool);
var
  nb_step:int;
  All_Acti:bool;
let 
  nb_step = 0 -> pre nb_step + 1 ; 
  All_Acti = all_true<<an,pn>>(Acti);
  res = (nb_step>=((3*diameter)-2)) => All_Acti ; -- from Lemma 4.10 page 40
tel

-----------------------------------------------------------------------------
node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn; Config:int^pn)
returns (ok:bool);
let
  
  ok = lemma_4_10  <<an,pn>> (Enab, Acti) and
       theorem_4_11<<an,pn>> (Enab, Acti); 
tel