verify.lus

-- hint: call me with ../run-kind2.sh
include "daemon_hyp.lus"

const worst_case = diameter * diameter;

node demon = daemon_is_central<<actions_number,card>>;

node verify(active : bool^actions_number^card; init_config : state^card)
returns (enabled : bool^actions_number^card;ok : bool);
var
  config : state^card;
  legitimate, closure, converge, converge_worst_case,worst_case_is_tigth : bool;
  steps : int;
  round:bool; round_nb:int;
let
  assert(true -> demon(active, pre enabled));

  steps = 0 -> (pre(steps) + 1);
  config, enabled, round, round_nb = topology(active, init_config);
  -- stability = mutual exclusion: exactly 1 node is enabled at a time
  legitimate = legitimate<<actions_number,card>>(enabled,config);

  closure = true -> (pre(legitimate) => legitimate);
  converge_worst_case = (steps >= worst_case) => legitimate;
  worst_case_is_tigth = (steps >= worst_case-3) => legitimate;

  assert(true -> init_config = pre init_config);
  converge = true -> (not(init_config = config) or legitimate);
  ok = closure and converge_worst_case and converge;
tel;