From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Coq Require Import Streams. From Coq Require Import SetoidClass.

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import ZUtils.
From Padec Require Import All_In.
From Padec Require Import AlgorithmMP.

Open Scope signature_scope.
Set Implicit Arguments.

Section RelModelMP.

  Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork} {Algo: MPAlgorithm}.

  Inductive MsgTag : Type :=
    | lost : MsgTag
    | rejected : MsgTag
    | received : MsgTag
    | pending : MsgTag.

  Instance MsgTag_Setoid : Setoid MsgTag :=
    {|equiv:=eq|}.

  Definition MsgTag_dec : Decider (equiv (A:=MsgTag)).

  Record Message :Type :=
    {
      destination: Node*InChannel;
      contents: Msg;
      status: MsgTag
    }.

  Definition eqMessage: relation Message :=
    fun m1 m2 =>
      destination m1 == destination m2 /\
      contents m1 == contents m2 /\
      status m1 == status m2.

#[refine] Instance Message_Setoid : Setoid Message := {|equiv:=eqMessage |}.

  Record Env : Type :=
    {
      Node_env : Node -> State ;

      Channel_env : list Message
    }.
  Record Event: Type :=
    {
      active_node: Node;
      recv_id: nat
 
    }.


  Definition Exec:= Stream (Env*Event).

  Definition eqEnv: relation Env := fun g1 g2 =>
      (Node_env g1 =~= Node_env g2) /\
      (Channel_env g1 == Channel_env g2).

  Instance eqEnv_per: PER eqEnv.

  Instance Env_partial_setoid:
    PartialSetoid Env:=
    {| pequiv:=eqEnv |}.

  Definition eqEvent: relation Event :=
    fun ev1 ev2 =>
      (active_node ev1 == active_node ev2) /\
      (recv_id ev1 == recv_id ev2).

  Instance eqEvent_equiv: Equivalence eqEvent.

  Instance Event_setoid:
    Setoid Event:=
    {| equiv:=eqEvent |}.

  Definition getMessage (env: Env) (msgid: nat):
    option Message := nth_error (Channel_env env) msgid.

  Instance nth_error_compat: forall (A:Type) (SA: PartialSetoid A),
      Proper fequiv (nth_error (A:=A)).

  Instance Channel_env_compat: Proper fequiv Channel_env.

  Definition tag_message (sender:Node)
             (pmsg: OutChannel * Msg) :
    option Message :=
    option_map (fun node_and_inchan => {|
      destination := node_and_inchan;
      contents := snd pmsg;
      status := pending;
                  |}) (inLink (sender,fst pmsg)).

  Definition append_new_messages
             (CE:list Message) (sender:Node)
             (sent: list (OutChannel*Msg)) :=
    CE ++ map_filter (tag_message sender) sent.

  Fixpoint mark_as_read (CE:list Message) (msgid:nat) :=
    match CE with
    | nil => nil
    | cons mesg q =>
      match msgid with
        O => cons {| destination:=destination mesg;
                     contents:=contents mesg;
                     status:=received |} q
      | S id' => cons mesg (mark_as_read q id')
      end
    end.


  Definition update_fun (A B:Type) (R:relation A)
             (Adec:Decider R) (F:A -> B) (a:A) (b:B) : A -> B :=
    fun a_ => if Adec a a_ then b else F a_.

  Definition update_env
             (g:Env) (ev:Event)
             (output: State*(list (OutChannel*Msg)))
    : Env := {|
              Node_env:=
                update_fun (Node_dec) (Node_env g) (active_node ev) (fst output);
              Channel_env:=
                (mark_as_read (Channel_env g) (recv_id ev))
                  ++ (map_filter (tag_message (active_node ev)) (snd output))
            |}.

  Definition read_mesg
             (g:Env) (ev:Event ) : option (InChannel*Msg) :=
    match getMessage g (recv_id ev) with
    | None => None
    | Some mesg =>
      
      Some (snd (destination mesg),contents mesg)
    end.

  Definition RchangeTag : relation Message := fun m1 m2 =>
    (m1 == m2) \/ (status m1 == pending /\
                          (status m2 == rejected \/ status m2 == lost) /\
                          destination m1 == destination m2 /\
                          contents m1 == contents m2).

  Definition RUN (p:Env*Event) :=
    update_env (fst p) (snd p)
               (run
                  (Node_env (fst p) (active_node (snd p)))
                  (read_mesg (fst p) (snd p))).

  Record Step
         (p2:Env*Event)
         (p1:Env*Event): Prop :=
    {
      Step_proper_r:> Proper pequiv p1;
      Step_proper_l: Proper pequiv p2;

      
      h_msg_select:
        match getMessage (fst p1) (recv_id (snd p1)) with
        | None => True
        | Some message =>
          fst (destination message) == (active_node (snd p1))
          /\
          status message == pending
        end;

      
      h_change_tag: (Node_env (RUN p1) =~= Node_env (fst p2)) /\
          eqlistA RchangeTag (Channel_env (RUN p1)) (Channel_env (fst p2));
   }.

  Definition h_fifo_step (g:Env) (ev:Event) :=
    match getMessage g (recv_id ev) with
    | None => True
    | Some message =>
      Forall (fun m => ~(status m == pending /\
                         destination m == destination message))
             (firstn (recv_id ev) (Channel_env g))
    end.
  Definition h_fifo_exec (exec : Exec) :=
    ForAll (fun e => h_fifo_step (fst (hd e)) (snd (hd e))) exec.

  Definition h_non_lossy_step (env : Env) :=
    Forall (fun m => ~(status m == lost)) (Channel_env env).
  Definition h_non_lossy_exec (exec : Exec) :=
    ForAll (fun e => h_non_lossy_step (fst (hd e))) exec.

  Definition h_non_bounded_step (env : Env) :=
    Forall (fun m => ~(status m == rejected)) (Channel_env env).
  Definition h_non_bounded_exec (exec : Exec) :=
    ForAll (fun e => h_non_bounded_step (fst (hd e))) exec.

  Definition h_bounded_step (capa : nat) (gg : Env) (g2 : Env) :=
    True.
  Definition h_bounded_exec (capa : nat) (exec : Exec) :=
    ForAll (fun e => h_bounded_step capa (RUN (hd e)) (fst (hd (tl e)))) exec.

  Definition ProcessFairness (exec: Exec): Prop :=
    forall n, ForAll (Exists (fun e => active_node (snd (hd e)) == n)) exec.




  Definition is_sent (exec: Exec) (dest: Node * InChannel) (msgId:nat) : Prop :=
    let ee1 := hd exec in
      let ee2 := hd (tl exec) in
        getMessage (fst ee1) msgId == None /\
        match getMessage (fst ee2) msgId with
          | None => False
          | Some message => (destination message == dest) /\
                     ~(status message == rejected)
        end.

  Definition is_received (exec: Exec) (dest: Node * InChannel) (msgId:nat) : Prop :=
    let ee1 := hd exec in
      match getMessage (fst ee1) msgId with
          | None => False
          | Some message => (destination message == dest) /\
                     (status message == received)
      end.

  Definition FairLossy (exec: Exec): Prop :=
    forall dest,
      (ForAll (Exists (fun e => exists msgId, is_sent e dest msgId)) exec) ->
      (ForAll (Exists (fun e => exists msgId, is_received e dest msgId)) exec)
  .

  Definition MessageTransmission (exec: Exec): Prop :=
    ForAll (fun e =>
              forall msgId, ~(getMessage (fst (hd e)) msgId == None) ->
                Exists (fun ee =>
                          match getMessage (fst (hd ee)) msgId with
                          | None => False
                          | Some message => ~(status message == pending)
                          end) e
           ) exec.



End RelModelMP.

Close Scope signature_scope.
Unset Implicit Arguments.