- 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
- Each post is stored in at most one server
- Each post is stored in at least two servers
- 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 friend 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.
- delPost undoes addPost
- delServer undoes addServer