Require Export DTime.
Require Export Node.


Section Node.

  Context { n : @Node }.
  Context { dtc : @DTimeContext }.

  Class Msg := MkMsg { msg : Type }.

  Context { m : Msg }.

  Record DirectedMsg :=
    MkDMsg
      {
        dmMsg   : msg;
        dmDst   : list name; (* list of destinations *)
        dmDelay : PosDTime;      (* delay in ms *)
      }.

  Definition DirectedMsgs := list DirectedMsg.

End Node.
