Library NetAuxDefs

Require Import List.
Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.NetAuxBasics.

Inductive tfs (m : Mode) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | tfsBase (i : nat) (n : Network) (p : reachableNet n) :
    tfsStartStateNet i n -> currModeNet m i n -> tfs m zeroTime i n p
  | tfsDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    tfs m t i n p -> tfsStateNet i n' -> tfs m t i n' (reachNetDisc n n' a p w)
  | tfsDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    tfs m t i n p -> tfs m (t +dt+ d) i n' (reachNetDel n n' d p w).

Inductive pending (i : nat) : forall n : Network, reachableNet n -> Prop :=
  | pendingBase (a : ActDiscNet) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') (m : Mode) (t x y : Time) :
    initStateNet m i n -> ovWaitStateNet m t x y i n' -> pending i n' (reachNetDisc n n' a p w)
  | pendingWait (a : ActDiscNet) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') (m : Mode) (t x y : Time) :
    pending i n p -> ovWaitStateNet m t x y i n -> ovWaitStateNet m t x y i n' -> pending i n' (reachNetDisc n n' a p w)
  | pendingWaitReady (a : ActDiscNet) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') (m : Mode) (l : Position) (t x y : Time) :
    pending i n p -> ovWaitStateNet m t x y i n -> ovReadyStateNet m t l i n' -> pending i n' (reachNetDisc n n' a p w)
  | pendingReady (a : ActDiscNet) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') (m : Mode) (l : Position) (t : Time) :
    pending i n p -> ovReadyStateNet m t l i n -> ovReadyStateNet m t l i n' -> pending i n' (reachNetDisc n n' a p w).

Inductive nextSince (m : Mode) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | nextSinceBase (a : ActDiscNet) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') (l : Position) (t t' x y : Time) :
    pending i n p -> ovReadyStateNet m t l i n -> ovWaitStateNet m t' x y i n' ->
    nextSince m zeroTime i n' (reachNetDisc n n' a p w)
  | nextSinceDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    nextSince m t i n p -> nextSinceStateNet i n' -> nextSince m t i n' (reachNetDisc n n' a p w)
  | nextSinceDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    nextSince m t i n p -> nextSince m (t +dt+ d) i n' (reachNetDel n n' d p w).

Inductive currSince (m : Mode) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | currSinceBase (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    nextSince m t i n p -> switchCurrStateNet i n -> switchListenStateNet i n' ->
    currSince m t i n' (reachNetDisc n n' a p w)
  | currSinceDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    currSince m t i n p -> currModeNet m i n' -> currSince m t i n' (reachNetDisc n n' a p w)
  | currSinceDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    currSince m t i n p -> currSince m (t +dt+ d) i n' (reachNetDel n n' d p w).

Inductive sent (v : list BaseType) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | sentBase (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- anTau -NA> n')
    (q q' : ProcTerm) (l : Position) (h h' : Interface) (k : ModeState) :
    [| q, l, h, k |] @ i .: n -> [| q', l, h', k |] @ i .: n' ->
    q -PA- (outAct chanOutProc v) -PA> q' -> h -i- (aiIn chanOutProc v) -i> h' ->
    sent v zeroTime i n' (reachNetDisc n n' anTau p w)
  | sentDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    sent v t i n p -> sent v t i n' (reachNetDisc n n' a p w)
  | sentDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    sent v t i n p -> sent v (t +dt+ d) i n' (reachNetDel n n' d p w).

Inductive delivered (v : Message) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | deliveredBase (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- (anOut v i) -NA> n') :
    delivered v zeroTime i n' (reachNetDisc n n' (anOut v i) p w)
  | deliveredDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    delivered v t i n p -> delivered v t i n' (reachNetDisc n n' a p w)
  | deliveredDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    delivered v t i n p -> delivered v (t +dt+ d) i n' (reachNetDel n n' d p w).

Inductive received (v : list BaseType) : Time -> nat -> forall n : Network, reachableNet n -> Prop :=
  | receivedBase (a : ActDiscNet) (i : nat) (n n' : Network) (p : reachableNet n)
  (w : n -NA- a -NA> n') (e e' : Entity) (l : Position) (r : Distance) :
    e @ i .: n -> e' @ i .: n' -> e -EA- (aeTagIn ([- v, l, r -])) ->> e' ->
    received v zeroTime i n' (reachNetDisc n n' a p w)
  | receivedDisc (a : ActDiscNet) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -NA- a -NA> n') :
    received v t i n p -> received v t i n' (reachNetDisc n n' a p w)
  | receivedDel (d : Delay) (t : Time) (i : nat) (n n' : Network) (p : reachableNet n) (w : n -ND- d -ND> n') :
    received v t i n p -> received v (t +dt+ d) i n' (reachNetDel n n' d p w).


Definition msgBadPathNet := liftEntNet msgBadPathEnt.
Definition notifBadPathNet := liftEntNet notifBadPathEnt.
Definition msgAbortPathNet := liftEntNet msgAbortPathEnt.
Definition notifAbortPathNet := liftEntNet notifAbortPathEnt.


Theorem msgBad_modeState_eq (n n' : Network) (a : ActDiscNet) (i : nat) k :
  msgBadPathNet i n -> mState_in_net k i n -> n -NA- a -NA> n' ->
  mState_in_net k i n'. Admitted.
Theorem notifBad_modeState_eq (n n' : Network) (a : ActDiscNet) (i : nat) k :
  notifBadPathNet i n -> mState_in_net k i n -> n -NA- a -NA> n' ->
  mState_in_net k i n'. Admitted.
Theorem msgAbort_modeState_eq (n n' : Network) (a : ActDiscNet) (i : nat) k :
  msgAbortPathNet i n -> mState_in_net k i n -> n -NA- a -NA> n' ->
  mState_in_net k i n'. Admitted.
Theorem notifAbort_modeState_eq (n n' : Network) (a : ActDiscNet) (i : nat) k :
  notifAbortPathNet i n -> mState_in_net k i n -> n -NA- a -NA> n' ->
  mState_in_net k i n'. Admitted.