open import Tagged open import GeneralLemmas using (Dec; _≡_) module Network (Node : Set) (_≟_ : (n n' : Node) → Dec (n ≡ n')) {Machine Msg : Set} (⟶Machine : Node → Machine → Tagged Msg → Machine → Set) where open import GeneralLemmas open import Relation SyncNetwork = Node → Machine AsyncNetwork = (Node → Machine) × List Msg update : {A : Set} → (Node → A) → Node → A → Node → A update nodes n m n' with n' ≟ n update nodes n m n' | yes p = m update nodes n m n' | no ¬p = nodes n' data _⟶Sync_ (nodes : SyncNetwork) : SyncNetwork → Set where silent-step : ∀ {i m'} → (⟶Machine i (nodes i) silent m') → nodes ⟶Sync update nodes i m' comm-step : ∀ {s r msg sender' receiver'} → let nodes' = update nodes s sender' in (⟶Machine s (nodes s) (send msg) sender') → (⟶Machine r (nodes' r) (receive msg) receiver') → nodes ⟶Sync update nodes' r receiver' data _⟶Async_ : AsyncNetwork → AsyncNetwork → Set where step : ∀ {nodes} msgsl msgsr {tmsg m' i} → let (msgsin , msgsout) = detag tmsg in (⟶Machine i (nodes i) tmsg m') → (nodes , msgsl ++ msgsin ++ msgsr) ⟶Async (update nodes i m' , msgsl ++ msgsout ++ msgsr) _⟶Async⁺_ = _⟶Async_ ⁺ _⟶Sync⁺_ = _⟶Sync_ ⁺ ⟶Sync-to-⟶Async⁺ : ∀ {a b} → a ⟶Sync b → (a , []) ⟶Async⁺ (b , []) ⟶Sync-to-⟶Async⁺ (silent-step s) = [ step [] [] s ] ⟶Sync-to-⟶Async⁺ (comm-step s₁ s₂) = step [] [] s₁ ∷ [ step [] [] s₂ ]