oracle_utils.lus

include "round.lus"
include "demon.lus"
include "utils.lus"


-----------------------------------------------------------------------------
-- An algo is silent when no action is enable
node silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
var
  enab:bool^pn; -- at least one action is enabled
let
  enab = map<< red<<or, an>>, pn >>(false^pn, Enab);
  ok = not(red<<or, pn>>(false, enab)); 
tel

-----------------------------------------------------------------------------
node move_count (tab_acti:bool^an^pn) returns (nb_act:int);
let
  nb_act = (0 -> pre(nb_act)) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));    
tel