Specification of a Communication Channel in Eqlog

```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

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

obj NATLIST is pr PNAT .
sort NatList .
op [_] : Nat -> NatList .
op _++_ : NatList NatList -> NatList [assoc] .
op empty : -> NatList .
var L : NatList .
eq  L ++ empty  =  L .
endo

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

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

obj IN-PORT is
pr PNAT .
sort Action .
op skip : -> Action .
op be : Nat -> Action .
sort State .
op In[_] : Nat -> State .
op _--I[_]->_ : State Action State -> Bool .
vars M N : Nat .
eq  In[M] --I[ skip]-> In[M]  =  true .
eq  In[M] --I[be(N)]-> In[N]  =  true .
endo

obj OUT-PORT is
pr PNAT .
sort Action .
op oskip : -> Action .
op be : Nat -> Action .
sort State .
op Out[_] : Nat -> State .
op _--O[_]->_ : State Action State -> Bool .
vars M N : Nat .
eq  Out[M] --O[oskip]-> Out[M]  =  true .
eq  Out[M] --O[be(N)]-> Out[N]  =  true .
endo

obj CHANNEL is
pr NATLIST .
sort Action .
op get : Nat -> Action .
op send : Nat -> Action .
op get_&send_ : Nat Nat -> Action .
sort State .
op ([_:_:_]) : Nat NatList Nat -> State .
op _--C[_]->_ : State Action State -> Bool .
var C : State .
var L : NatList .
vars M N P Q : Nat .

eq  [M : L : N] --C[get(P)]->
[P : [P] ++ L : N]  =  true .

eq  [M : empty : N] --C[send(P)]-> C  =  false .

eq  [M : L ++ [P] : N] --C[send(P)]->
[M : L : P]  =  true .

eq  [M : L ++ [P] : N] --C[get Q &send P]->
[Q : [Q] ++ L : P]  =  true .

eq  [M : empty : N] --C[get Q &send(Q)]->
[Q : empty : Q]  =  true .
endo
```

To Eqlog homepage
To Systems index page
To Joseph Goguen homepage
Maintained by Joseph Goguen