class AtomicRegister_Rewrite
  include Bud

  state do
    scratch :del_write_log_r0, [:wid] => [:name, :val, :prev_wid]
    scratch :del_write_log_r3, [:wid] => [:name, :val, :prev_wid]
    table :dom, [:wid]
    scratch :live, [:wid] => [:name, :val, :prev_wid]
    table :write, [:wid] => [:name, :val]
    scratch :write_event, [:wid] => [:name, :val]
    range :write_keys, [:wid]
    table :write_log, [:wid] => [:name, :val, :prev_wid]
    range :write_log_keys, [:wid]
  end

  bloom do
    (dom < -(dom * write_log_keys).lefts(:wid => :wid).notin(write_log, :wid => :wid))
    (write < -(write * write_log).lefts(:wid => :wid))
    (write_log < +(write_event * live).outer(:name => :name) do |e, l|
  (e + [l.wid.nil? ? (0) : (l.wid)])
end.notin(write_log_keys, 0 => :wid))
    (write_log < -(del_write_log_r0 * del_write_log_r3).matches { |t0, t1| t0 })
    del_write_log_r0 <= ((write_log * write_keys).lefts(:wid => :wid)).notin(write, :wid => :wid)
    del_write_log_r3 <= (write_log * dom).lefts(:wid => :wid)
    dom <= (write_log { |l| [l.prev_wid] })
    live <= (write_log.notin(dom, :wid => :wid))
    write_event <= (write.notin(write_log, :wid => :wid))
    write_keys <+ write {|r| [r.wid]}
    write_log_keys <+ write_log {|r| [r.wid]}
  end
end