Skip to content

Generate oracle skeletons from the dot

Such skeletons could contains

  • a node computing the silence (silent)
  • a node after_n
  • some useful constants (card, degree, diameter)
  • a node that gathers variables into arrays
const card=7;
const degree=3;
const diameter=7;

node after_n(n:int; x:bool) returns (res:bool);
var cpt:int;
let
  cpt = 0 -> pre cpt + 1;
  res = cpt <= n or x;
tel
node silent(Enab_a, act: bool^card) returns (ok:bool);
let
  ok = after_n(42, boolred<<0,0,card>>(Enab_a));
tel

node oracle(Enab_p1_a, Enab_p2_a, Enab_p3_a, Enab_p4_a, Enab_p5_a,
	Enab_p6_a, Enab_p7_a, p1_a, p2_a, p3_a, p4_a, p5_a, p6_a,
	p7_a:bool) returns (ok:bool);
var
  Enab_a,a: bool^card;
let
  Enab_a = [Enab_p1_a,Enab_p2_a,Enab_p3_a,Enab_p4_a,Enab_p5_a,Enab_p6_a,Enab_p7_a];
  act = [p1_a, p2_a, p3_a, p4_a, p5_a, p6_a, p7_a];
  ok = true;
tel