Require Export Quorum.
Require Export Process.


Section Received_or_generated.

  Context { pd  : @Data }.
  Context { pn  : @Node }.
  Context { pk  : @Key }.
  Context { pm  : @Msg }.
  Context { qc  : @Quorum_context pn}.
  Context { dtc : @DTimeContext }.
  Context { iot : @IOTrusted }.


  Local Open Scope eo.
  Local Open Scope proc.


  Definition received_or_generated {S}
             (eo   : EventOrdering)
             (sm   : MStateMachine S)
             (Cond : Event -> S -> Prop)
             (Rec  : Event -> S -> S -> Event -> S -> Prop)
             (Gen  : Event -> S -> S -> Event -> S  -> Prop) :=
    forall (e : Event) (st : S ),
      state_sm_on_event sm e = Some st
      -> Cond e st
      ->
    exists e' st1 st2,
      e' ⊑ e
      /\ state_sm_before_event sm e' = Some st1
      /\ state_sm_on_event sm e' = Some st2
      /\ (Rec e' st1 st2 e st \/ Gen e' st1 st2 e st).

  Definition received_or_generated_loc {S}
             (eo   : EventOrdering)
             (i    : node_type)
             (sm   : MStateMachine S)
             (Cond : Event -> node_type -> S -> Prop)
             (Rec  : Event -> S -> S -> Event -> node_type -> S -> Prop)
             (Gen  : Event -> S -> S -> Event -> node_type -> S  -> Prop) :=
    forall (e : Event) (st : S ),
      loc e = node2name i
      -> state_sm_on_event sm e = Some st
      -> Cond e i st
      ->
    exists e' st1 st2,
      e' ⊑ e
      /\ state_sm_before_event sm e' = Some st1
      /\ state_sm_on_event sm e' = Some st2
      /\ (Rec e' st1 st2 e i st \/ Gen e' st1 st2 e i st).


End Received_or_generated.
