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₂ ]