open import Tagged -- silent / send / receive
open import GeneralLemmas using (Dec; _≡_) 
module Network
  (Node : Set)
  (_≟_ :  (n n' : Node)  Dec (n  n'))  -- param by decidable equality on nodes
  {Machine Msg : Set}
  (⟶Machine :  Node  Machine          -- param by a transition relation in general 
               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 -- (nodes | n -> m)
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 -- 'net with sync message passing'
  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 -- 'net with async message passing' 
  step :  {nodes} msgsl msgsr {tmsg m' i}  let (msgsin , msgsout) = detag tmsg in 
  -- at least one (possibly both) of msgsin, msgsout is empty
    (⟶Machine i (nodes i) tmsg m') 
    (nodes , msgsl ++ msgsin ++ msgsr)  ⟶Async (update nodes i m' , msgsl ++ msgsout ++ msgsr)
  -- the data is pulled by the machines, so if it is not there it is no problem, they just wait.

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