Social Network

Consider the following model of distributed social network.

sig User {}
sig Post {}
sig DistributedSN {
servers : set Server,
    friends : User -> User
}
sig Server {
     posts : User -> Post, 
     capacity : Int
}

1. Write the following invariants:
   • Each post is owned by at most one user
   • A user cannot be his or her own friend
   • Friendship is a symmetric relation
   • Server capacity is positive
   • Servers cannot exceed their capacity
2. Explore different (alternative) replication strategies for posts:
   • Each post is stored in at most one server
   • Each post is stored in at least two servers
3. Specify the following operations ensuring they preserve the above invariants
   • addPost[n1,n2:DistributedSN,u:User,p:Post]: add post p by user u.
   • delPost[n1,n2:DistributedSN,u:User,p:Post]: delete post p from user u.
   • addFriend[n1,n2:DistributedSN,u,v:User]: add v as fried of u.
   • addServer[n1,n2:DistributedSN,s:Server]: add new server s to network n1.
   • delServer[n1,n2:DistributedSN,s:Server]: delete server s from network n1.
4. Check the following algebraic properties of these operations:
   • delPost undos addPost
   • delServer undos addServer