library MessageLists

from Basic/StructuredDatatypes get Set, Map

spec Peer[sort Address] = dspec
  sort PeerId;
  observe Peer label PeerL
    op id: Peer -> PeerId;
      addr: Peer ->? Address;
    preds isOnline: Peer;
    cats
      goesOnline: PeerL;
      goesOffline: PeerL;
      changesState: PeerL;
    forall l: PeerL
      . goesOnline(l) => l affects isOnline
      . goesOffline(l) => l affects isOnline
      . l affects isOnline => l affects addr
  end_obs
  forall l: PeerL; p, p': Peer
    . changesState(l)
    . isOnline(p') if p --l--> p' /\ goesOnline(l)
    . not isOnline(p') if p --l--> p' /\ goesOffline(l)
    . def(addr(p)) if isOnline(p)
end_dspec

spec BasePeer = Peer[sort Address]

spec Net[BasePeer] = Set[sort PeerId fit Elem |-> PeerId] and
    Map[sort PeerId fit S |-> PeerId]
      [sort Peer fit T |-> Peer]
    and Map[sort PeerId fit S |-> PeerId]
      [sort PeerL fit T |-> PeerL]
then dspec
  sorts Net = Map[PeerId, Peer]; NetI = Map[PeerId, PeerL];
  observe Net info NetI
    ops dom: Net -> Set[PeerId]
  end_obs
  forall id: PeerId; n, n': Net; i: NetI; g: GroupId
  . dom(i) isSubsetOf dom(n) if i:: n ----> n'
  . lookup(id, n) --lookup(id, i)--> lookup(id, n')
    if i:: n ----> n' /\ id eps dom(i)
  . lookup(id, n) = lookup(id, n')
    if i:: n ----> n' /\ id eps dom(n) /\ not id eps dom(i)
end_dspec

spec BaseNet = Net[BasePeer]

spec Groups[BaseNet] = Set[sort GroupId fit Elem |-> GroupId]
then dspec
  ops joined, left: PeerL -> Set[GroupId];
    members: Net * GroupId -> Set[PeerId];
  observe Peer label PeerL
    op groups: Peer -> Set[GroupId];
    cats joins, leaves: PeerL;
    forall l: PeerL
    . joins(l) => l affects groups
    . leaves(l) => l affects groups
  end_obs
  forall p, p': Peer; l: PeerL; g: GroupId; n: Net; id: PeerId
  . groups(p') = (groups(p) - left(l)) union joined(l)
    if p --l--> p'
  . left(l) = {} if not leaves(l)
  . joined(l) = {} if not joins(l)
  . id eps members(n, g) <=> g eps groups(lookup(id, n))
end_dspec

spec BaseGroups = Groups[BaseNet]

spec Messages[BaseNet] = Set[sort Msg fit Elem |-> Msg] then
  ops
    orig, dest: Msg -> Address;
    sent, recvd: PeerL -> Set[Msg];
  forall m: Msg; p, p': Peer; l: PeerL; id: PeerId;
    n, n': Net; i: NetI
  . isOnline(p)
    if p --l--> p' /\ isNonEmpty(recvd(l) union sent(l))
  . dest(m) = addr(p) if p --l--> p' /\ m eps recvd(l)
  . orig(m) = addr(p) if p --l--> p' /\ m eps sent(l)
  . m eps recvd(lookup(id, i))
    if i:: n ----> n' /\ l eps range(i) /\ m eps sent(l)
    /\ id eps dom(n) /\ addr(lookup(id, n)) = dest(m)
end

spec BaseMessages = Messages[BaseNet]

spec MsgLists[BaseMessages][BaseGroups] =
  ops addr: GroupId -> Address;
    forward: Msg * Address -> Msg;
  forall g: GroupId; m: Msg; a: Address; id: PeerId;
    n, n': Net; i: NetI; l: PeerL
  . dest(forward(m, a)) = a
  . orig(forward(m, a)) = orig(m)
  . forward(m, addr(lookup(id, n))) eps sent(l)
    if i :: n ----> n' /\ l eps range(i) /\ m eps sent(l)
    /\ addr(g) = dest(m) /\ g eps groups(lookup(id, n))
    /\ isOnline(lookup(id, n))
end

spec BaseMsgLists = MsgLists[BaseMessages][BaseGroups]

spec AuthGroups[BaseGroups] =
  op owner: GroupId -> PeerId;
  pred authorises: PeerL * GroupId * PeerId;
  forall i: NetI; g: GroupId; id, id2: PeerId; l: PeerL;
    n, n': Net
  . isOnline(lookup(id, n))
    if i[l/id] :: n ----> n'
    /\ (authorises(l, g, id2) \/ joins(l))
  . authorises(lookup(owner(g), i), g, id)
    if i[l/id] :: n ----> n' /\ g eps joined(l)
end

spec BaseAuthGroups = AuthGroups[BaseGroups]

spec AuthMsgLists = MsgLists[BaseMessages][BaseAuthGroups]