This file specifies synchronous communication between a sender, AOBJ, and a receiver, BOBJ, via an intermediary port, PORT-OBJ.

*** a theory of labelled transition systems with an idle transition, skip

th OBJECT is
  sort Action .
  op skip : -> Action .

  sort State .
  op _--[_]->_ : State Action State -> Bool .

  var S : State .
  eq  S --[skip]-> S  =  true .
  *** this just says _--[skip]->_ is reflexive,
  *** but eq S --[skip]-> S' = (S == S') doesn't work in Eqlog
endth

find S1, S2 : State such that S1 --[skip]-> S2 = true .


*** A simple data type for the values communicated: natural numbers

obj PNAT is
  sort Nat .
  op 0 : -> Nat .
  op s : Nat -> Nat .
endo


*** The "sender" object, AOBJ, whose state consists of two registers:
*** the first is "local"; the second is used to send values to BOBJ.

obj AOBJ is
  pr PNAT .

  sort Action .
  op askip : -> Action .   *** idle transition
  op inc   : -> Action .   *** increment 1st register
  op write : -> Action .   *** put value in 1st register to 2nd

  sort State .
  op A[_,_] : Nat Nat -> State .
  
  op _--A[_]->_ : State Action State -> Bool .

  vars M N : Nat .
  eq  A[M,N]  --A[askip]->  A[M,N]     =  true .
  eq  A[M,N]  --A[ inc ]->  A[s(M),N]  =  true .
  eq  A[M,N]  --A[write]->  A[M,M]     =  true .
endo


*** The receiver object, BOBJ, whose state consists of two registers:
*** the 1st is used to receive values from AOBJ, the 2nd is "local".
  
obj BOBJ is
  pr PNAT .

  sort Action .
  op bskip : -> Action .   *** idle transition
  op copy  : -> Action .   *** put value in 1st register into 2nd
  op get   : -> Action .   *** get new value into 1st register

  sort State .
  op B[_,_] : Nat Nat -> State .
  
  op _--B[_]->_ : State Action State -> Bool .

  vars M M' N : Nat .
  eq  B[M,N]  --B[bskip]->  B[M,N]   =  true .
  eq  B[M,N]  --B[copy ]->  B[M,M]   =  true .
  eq  B[M,N]  --B[ get ]->  B[M',N]  =  true .
endo


*** The port object, a go-between for AOBJ and BOBJ:
*** its state consists of a single register, which is both
*** the 2nd register of AOBJ and the 1st register of BOBJ
  
obj PORT-OBJ is
  pr PNAT .
  
  sort Action .
  op pskip : -> Action .   *** idle transition
  op port  : -> Action .   *** transmit value from AOBJ to BOBJ

  sort State .
  op P[_] : Nat -> State .
  
  op _--P[_]->_ : State Action State -> Bool .

  vars M N : Nat .
  eq  P[M]  --P[pskip]->  P[M]  =  true .
  eq  P[M]  --P[ port]->  P[N]  =  true .
endo


*** morphism of transition systems
*** says that PORT-OBJ is a subobject of AOBJ:

view AP from AOBJ to PORT-OBJ is
  op  askip  to  pskip .
  op  inc    to  pskip .
  op  write  to  port .
  vars M N : Nat .
  op  A[M,N] to  P[N] .
endv

*** and that PORT-OBJ is a subobject of BOBJ:

view BP from BOBJ to PORT-OBJ is
  op  bskip  to  pskip .
  op  copy   to  pskip .
  op  get    to  port .
  vars M N : Nat .
  op  B[M,N] to  P[M] .
endv


*** make these views explicit:

obj CONNECTIONS is
  pr AOBJ + PORT-OBJ + BOBJ .

  op apa : Action.AOBJ -> Action.PORT-OBJ .
  eq apa(askip) = pskip .
  eq apa(inc)   = pskip .
  eq apa(write) = port .

  op bpa : Action.BOBJ -> Action.PORT-OBJ .
  eq bpa(bskip) = pskip .
  eq bpa(copy)  = pskip .
  eq bpa(get)   = port .

  op aps : State.AOBJ -> State.PORT-OBJ .
  vars M N : Nat .
  eq aps(A[M,N]) = P[N] .

  op bps : State.BOBJ -> State.PORT-OBJ .
  eq bps(B[M,N]) = P[M] .
endo


*** The next module gives the behaviour of the system as a limit of
***
***    AOBJ         BOBJ
***      \          /
***       \        /
***        \      /
***         \    /
***        PORT-OBJ

obj SYS is
  pr CONNECTIONS .

  sort Action .
  op ([_:_:_]) : Action.AOBJ Action.PORT-OBJ Action.BOBJ -> Action .
  op [skips] : -> Action .
  eq [skips] = [askip : pskip : bskip] .

  sort State .
  op ([_:_:_]) : State.AOBJ State.PORT-OBJ State.BOBJ -> State .
  op _--_->_ : State Action State -> Bool .

  var AA : Action.AOBJ .
  var AP : Action.PORT-OBJ .
  var AB : Action.BOBJ .
  vars SA SA' : State.AOBJ .
  vars SP SP' : State.PORT-OBJ .
  vars SB SB' : State.BOBJ .
  cq  [SA : SP : SB]  --[AA : AP : AB]->  [SA' : SP' : SB']  =  true
      if   aps(SA) == SP  and  bps(SB) == SP
      and  apa(AA) == AP  and  bpa(AB) == AP
      and  SA --A[AA]-> SA' == true
      and  SP --P[AP]-> SP' == true
      and  SB --B[AB]-> SB' == true
      and  aps(SA') == SP'  and  bps(SB') == SP' .
  *** the clauses involving aps, etc., restrict transitions to
  *** states and actions that are well-defined in the limit.
endo