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