Library mcertikos.conlib.conmtlib.SingleAbstractDataType

Require Import Coqlib.
Require Import Maps.
Require Import Values.
Require Import liblayers.compat.CompatLayers.

Class SingleData :=
  {
    dshare: Type;
    init_dshare: dshare;
    processor_id : dshare → Z;
    proc_id: dshare → Z;
    dproc: Type;
    main_init_dproc: dproc;
    nomain_init_dproc: dproc
  }.

Section WithData.

Context `{single_data: SingleData}.

Definition EData := ZMap.t (option dproc).
Definition CData := dshare × ZMap.t (option dproc).
Definition PData := dshare × dproc.

End WithData.