------------------------------------------------------------------------
-- A formalisation of CBS, close to "A calculus of broadcasting
-- systems" by K.V.S. Prasad, but using mixed induction and
-- coinduction instead of explicit guarded definitions
------------------------------------------------------------------------

module CBS where

open import Coinduction
open import Data.Product
open import Function.Equality
open import Function.Equivalence
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Sets with decidable propositional equality

record Data : Set₁ where
  field
    El     : Set
    ⟨_⟩_≟_ : Decidable (_≡_ {A = El})

open Data public

------------------------------------------------------------------------
-- Processes

-- Messages; τ stands for a silent message.

data Msg α : Set where
  msg : (v : El α) → Msg α
  τ   : Msg α

-- Processes. Instead of explicit guarded definitions I have used
-- mixed induction and coinduction.

infix  _&⟨_,_⟩ _∣_ _[_]

data Proc (α : Data) : Set₁ where
  ¿       : (f : El α → ∞ (Proc α)) → Proc α
  _&⟨_,_⟩ : (f : El α → ∞ (Proc α)) (w : Msg α) (p : ∞ (Proc α)) → Proc α
  _∣_     : (p₁ p₂ : Proc α) → Proc α
  _[_]    : ∀ {β} (ϕ : El α ⇔ El β) (p : Proc β) → Proc α

------------------------------------------------------------------------
-- Some derived operators

-- Swallows all received messages.

∅ : ∀ {α} → Proc α
∅ = ¿ λ _ → ♯ ∅

-- Swallows messages until it gets a chance to send.

_¡_ : ∀ {α} → Msg α → Proc α → Proc α
w ¡ p = (λ _ → ♯ (w ¡ p)) &⟨ w , ♯ p ⟩

------------------------------------------------------------------------
-- Single-step semantics

-- Application of translation functions.

infixr  _↑_ _↓_

_↑_ : ∀ {α β} → El α ⇔ El β → Msg β → Msg α
ϕ ↑ msg x = msg (Equivalence.from ϕ ⟨$⟩ x)
ϕ ↑ τ     = τ

_↓_ : ∀ {α β} → El α ⇔ El β → Msg α → Msg β
ϕ ↓ msg x = msg (Equivalence.to ϕ ⟨$⟩ x)
ϕ ↓ τ     = τ

-- Actions are messages along with information about whether they are
-- sent or received.

data SendRecv : Set where
  ! : SendRecv
  ¿ : SendRecv

Action : Data → Set
Action α = Msg α × SendRecv

-- Two processes cannot simultaneously send something.

infix  _·_≡_

data _·_≡_ : SendRecv → SendRecv → SendRecv → Set where
  !¿ : ! · ¿ ≡ !
  ¿! : ¿ · ! ≡ !
  ¿¿ : ¿ · ¿ ≡ ¿

-- The single-step relation.

infix  _[_]⟶_

data _[_]⟶_ {α} : Proc α → Action α → Proc α → Set₁ where
  τ          : ∀ {p}       → p            [ τ     , ¿ ]⟶ p
  ¿-recv     : ∀ {f     v} → ¿ f          [ msg v , ¿ ]⟶ ♭ (f v)
  &-recv     : ∀ {f w p v} → f &⟨ w , p ⟩ [ msg v , ¿ ]⟶ ♭ (f v)
  &-send     : ∀ {f w p}   → f &⟨ w , p ⟩ [ w     , ! ]⟶ ♭ p
  compose    : ∀ {p₁ p₁′ p₂ p₂′ ♮₁ ♮₂ ♮₃ w}
               (¬‼     : ♮₁ · ♮₂ ≡ ♮₃)
               (p₁⟶p₁′ : p₁ [ w , ♮₁ ]⟶ p₁′)
               (p₂⟶p₂′ : p₂ [ w , ♮₂ ]⟶ p₂′) →
                    p₁ ∣ p₂ [ w , ♮₃ ]⟶ p₁′ ∣ p₂′
  trans-send : ∀ {β} {p p′ : Proc β} {ϕ u} (p⟶p′ : p [ u     , ! ]⟶ p′) → ϕ [ p ] [ ϕ ↑ u , ! ]⟶ ϕ [ p′ ]
  trans-recv : ∀ {β} {p p′ : Proc β} {ϕ w} (p⟶p′ : p [ ϕ ↓ w , ¿ ]⟶ p′) → ϕ [ p ] [ w     , ¿ ]⟶ ϕ [ p′ ]

------------------------------------------------------------------------
-- Strong bisimulation

-- The largest strong bisimulation.

infix  _∼_

record _∼_ {α} (p₁ p₂ : Proc α) : Set₁ where
  inductive
  field
    ⇒ : ∀ {p₁′ w ♮} → p₁ [ w , ♮ ]⟶ p₁′ →
        ∃ λ p₂′ → p₂ [ w , ♮ ]⟶ p₂′ × ∞ (p₁′ ∼ p₂′)

    ⇐ : ∀ {p₂′ w ♮} → p₂ [ w , ♮ ]⟶ p₂′ →
        ∃ λ p₁′ → p₁ [ w , ♮ ]⟶ p₁′ × ∞ (p₁′ ∼ p₂′)