include "ctrl.cat"
let data = [R]; dd-restrict; [DATA]; intrinsic; [W]
let addr = [R]; dd-restrict; [NDATA]; intrinsic; [M]
let pom = po & (M*M)
let sim = (same-instr & ((EXEC*SPEC) | (SPEC*EXEC))) \ id
let instances = classes(same-instance)
let depi = lift(instances,(rf-reg-restrict|rfi)^-1)
in
let diffw =(loc & (W * W)) \ id
let diff = ((rfe^-1;diffw;rf)|(rf^-1;diffw;rfe))
let diffi = lift(instances,diff)
let bisim = delift(bisimulation(depi,lift(instances,same-instr)\diffi))\id
let equiv = (W*W) & bisim
let ctrl = ctrlequiv equiv
let AE = always-exec equiv
let DW = zyva equiv Dmins
let rf-mem = rf \ rf-reg
show rf-reg
show rf-mem
as rf
show co|fr
as ca