-- Mesge Board
-- 17/11/2009
-- Yoshinao Isobe (AIST & NII)

---------------------------------------------------------
--                  Data, function, chennel
---------------------------------------------------------

N = 2      -- the number of users
M = 2      -- the maximum number of messages on the board
null = -1

-- datatype

nametype ID = {0..N-1}
nametype MID = {null..N-1}

datatype Name = myChan
nametype Chan = (Name,{0..N-1})   -- private channel names

datatype String = Hello | Bye | Empty
nametype Message = diff(String,{Empty})

nametype MessInfo = (MID,Message)
nametype MessList = FiniteSeq(MessInfo,M)

datatype Request = ReqOn.Chan
                 | ReqOff.ID
                 | ReqAdd.Message
                 | ReqRem.ID
                 | ReqSet.ID
                 | ReqMov.ID

datatype Reply = RepOn.ID
               | RepOff.ID
               | RepData.MessList

datatype ButtonEvent = On | Off
datatype MouseEvent  = Move | Drag | ClickL | ClickR

-- functions for sequences

FiniteSeq(A,0) = {<>}
FiniteSeq(A,n) = union({<x>^s | x <- A, s <- FiniteSeq(A,n-1)}, FiniteSeq(A,n-1))

remID(<>,j) = <>
remID(<i>^list,j) = if (i==j) then list else <i>^remID(list,j)

remM(<>,j) = <>
remM(<(i,m)>^list,j) = if (i==j) then list else <(i,m)>^remM(list,j)

putM(<>,j) = <>
putM(<(i,m)>^list,j) = if (i==j) then <(null,m)>^list else <(i,m)>^putM(list,j)

getM(<>,j,n) = <>
getM(<(i,m)>^list,j,0) = if (i==null) then <(j,m)>^list else <(i,m)>^list 
getM(<(i,m)>^list,j,n) = <(i,m)>^getM(list,j,n-1)

write(<>,i,y) = <>
write(<x>^list,0,y) = <y>^list
write(<x>^list,i,y) = <x>^write(list,i-1,y)

read(<x>^list,0) = x
read(<x>^list,i) = read(list,i-1)

makecopy(0,x) = <>
makecopy(i,x) = <x>^makecopy(i-1,x)

-- function for Request

reqOn  = 0
reqOff = 1
reqAdd = 2
reqRem = 3
reqSet = 4
reqMov = 5

reqCom(ReqOn.x)  = reqOn
reqCom(ReqOff.x) = reqOff
reqCom(ReqAdd.x) = reqAdd
reqCom(ReqRem.x) = reqRem
reqCom(ReqSet.x) = reqSet
reqCom(ReqMov.x) = reqMov

reqId(ReqOff.x) = x
reqId(ReqRem.x) = x
reqId(ReqSet.x) = x
reqId(ReqMov.x) = x

reqMs(ReqAdd.x) = x
reqCh(ReqOn.x) = x

-- function for Reply

repOn   = 0
repOff  = 1
repData = 2

repCom(RepOn.x)   = repOn
repCom(RepOff.x)  = repOff
repCom(RepData.x) = repData

repId(RepOn.id) = id
repMs(RepData.m) = m

-- make free ID

freeID(idList,i) = if (length(idList)<N)
                   then if (elem(i,idList))
                        then freeID(idList,i+1)
                        else i
                   else N

-- channel

channel button : Chan.ButtonEvent
channel mouse  : Chan.MouseEvent
channel ack    : ID

channel start  : Chan
channel stop   : Chan

channel display: Chan.MessList

channel upChan : Request
channel private: Chan.Reply

channel except  : Chan
channel linkLost: Chan

datatype ErrorMess = Overflow | Zero

channel error : ErrorMess

OutputEvents =
  {| display |} 

InputEvents =
  {| button, mouse, start, stop |}

UserEvents(ch) = 
  {| button.ch, mouse.ch, start.ch, stop.ch, display.ch |}

---------------------------------------------------------
--                     Process
---------------------------------------------------------

-- Servder --

Server(idList,mList,chList) = 
   upChan?x ->
     if (reqCom(x)==reqOn) then Connect(idList,mList,chList,freeID(idList,0),reqCh(x))
     else if (reqCom(x)==reqOff) then Disconnect(idList,mList,chList,reqId(x))
     else if (reqCom(x)==reqAdd) then AddMessage(idList,mList,chList,reqMs(x))
     else if (reqCom(x)==reqRem) then RemMessage(idList,mList,chList,reqId(x))
     else if (reqCom(x)==reqSet) then SetMessage(idList,mList,chList,reqId(x))
     else if (reqCom(x)==reqMov) then MovMessage(idList,mList,chList,reqId(x))
     else Server(idList,mList,chList)

Connect(idList,mList,chList,id,ch) = 
  if (length(idList)<N) 
  then
     (private.ch!RepOn.id -> 
      Server(idList^<id>,mList,write(chList,id,ch)) []
     (except.ch -> Server(idList,mList,chList)))
  else
      error.Overflow -> STOP

Disconnect(idList,mList,chList,id) = 
  if (length(idList)>0) 
  then
    (private.read(chList,id)!RepOff.id -> 
     Server(remID(idList,id),putM(mList,id),chList) []
    (except.read(chList,id) -> Server(idList,mList,chList)))
  else
      error.Zero -> STOP

AddMessage(idList,mList,chList,m) =
  if (length(mList)<M)
  then Broadcast(idList,mList^<(null,m)>,chList)
  else Broadcast(idList,mList,chList)

RemMessage(idList,mList,chList,id) =
  Broadcast(idList,remM(mList,id),chList)

SetMessage(idList,mList,chList,id) =
  if (length(mList)>0)
  then Broadcast(idList,putM(mList,id),chList) |~|
      (|~| i:{0..length(mList)-1} @
           Broadcast(idList,getM(putM(mList,id),id,i),chList))
  else Broadcast(idList,mList,chList)

MovMessage(idList,mList,chList,id) =
  Broadcast(idList,mList,chList)


Broadcast(idList,mList,chList) = Loop(idList,mList,chList,idList)

Loop(idList,mList,chList,<>) = Server(idList,mList,chList)
Loop(idList,mList,chList,<i>^list) = 
   (private.read(chList,i)!RepData.mList -> Loop(idList,mList,chList,list)) []
   (except.read(chList,i) -> Loop(remID(idList,i),putM(mList,i),chList,list))

LinkException(s) = 
    [] ch:Chan @ elem(ch,s) & except.ch -> LinkException(s) []
    [] ch:Chan @ (not elem(ch,s)) & linkLost.ch -> LinkException(s^<ch>)

-- Client Receiver --

  CRun(ch,id,st) =
    private.ch?x ->
      if (not st) 
      then
        if (repCom(x) == repOn) then ack!repId(x) -> CRun(ch,repId(x),true)
        else CRun(ch,id,st)
      else
        if (repCom(x) == repOff) then ack!id -> CRun(ch,id,false)
        else if (repCom(x) == repData) then display.ch!repMs(x) -> CRun(ch,id,true)
        else CRun(ch,id,st)


-- Client Sender 
-- st=true iff online

Listener(ch,id,st) =
   (button.ch?x -> 
      if (not st) then
        if (x==On) then upChan!ReqOn.ch -> ack?id -> Listener(ch,id,true)
        else Listener(ch,id,st)
      else
        if (x==Off) then upChan!ReqOff.id -> ack?z -> Listener(ch,-1,false)
        else Listener(ch,id,st))
   []
   (mouse.ch?x ->
      if (not st) then
         Listener(ch,id,st)
      else
        if (x==ClickL) then |~| s:String @ 
           if (s!=Empty) then upChan!ReqAdd.s -> Listener(ch,id,st)
           else Listener(ch,id,st)
        else if (x==ClickR) then upChan!ReqRem.id -> Listener(ch,id,st)
        else if (x==Move) then upChan!ReqSet.id -> Listener(ch,id,st)
        else if (x==Drag) then upChan!ReqMov.id -> Listener(ch,id,st)
        else Listener(ch,id,st))

---------------------------------------------------------
--                     Composition
---------------------------------------------------------

ServerException = 
   (Server(<>,<>,makecopy(N,(myChan,0))) [| {| except |} |] LinkException(<>))
          \{| except |}

ClientRun(ch) = (CRun(ch,-1,false) [|{|ack|}|] Listener(ch,-1,false)) \ {|ack|}

Client(ch) = start.ch -> 
             (ClientRun(ch) /\ stop.ch -> linkLost.ch -> STOP)

Clients = ||| ch:Chan @ Client(ch)

System = (ServerException [| {| upChan, private, linkLost |} |] Clients)
         \ {| upChan, private, linkLost |}

----------------------------------------------------------
--                     Verification 1
----------------------------------------------------------

-- The user 0 can continue to use her/his interface 
-- without respect to the behaviors of the others.

SpecMain(ch) = 
  button.ch?x -> SpecMain(ch) |~|
  mouse.ch?x -> SpecMain(ch) |~|
  |~| mlist:MessList @ display.ch!mlist -> SpecMain(ch)

Spec(ch) =
  start.ch ->
  (SpecMain(ch) /\ stop.ch -> STOP)

Spec0 = Spec((myChan,0))

Eager(X,P) = P \ X
Lazy(X,P) = (P [|X|] CHAOS(X))\X

EagerSet(ch) = diff(OutputEvents, UserEvents(ch))
LazySet(ch) = diff(InputEvents, UserEvents(ch))

EagerSystem(ch) = Eager(EagerSet(ch), System)
LazyEagerSystem(ch) = Lazy(LazySet(ch), EagerSystem(ch))

CH=(myChan,0)

assert System :[livelock free]
assert Spec(CH) :[livelock free]
assert EagerSystem(CH) :[livelock free]
assert Spec(CH) [F= LazyEagerSystem(CH)

----------------------------------------------------------
--                     Verification 2
----------------------------------------------------------

-- a message can be chosen and can be held forever.

dispHello0 = display.(myChan,0).<(0,Hello)>
     stop0 = stop.(myChan,0)

   AllowedTr = dispHello0 -> KeepMessage
 KeepMessage = dispHello0 -> KeepMessage

-- a message can be eventually released after stop.
-- (check if a message can be held by someone after he has stopped)

ForbiddenTr = dispHello0 -> stop0 -> KeepMessage   -- shoud be False

-- the following 2 checks may take 1 hour for each by 2GHz CPU (Core2).

assert System \ diff(Events,{dispHello0}) [T= AllowedTr
assert System \ diff(Events,{dispHello0,stop0}) [T= ForbiddenTr