合金分析仪作为常数求解器

Question

1. 朋友是一个社交网络，其成员可以通过友谊关系。
2. 成员可以发布仅包含文本的帖子，并可以选择发布照片。
3. 每张照片都有标题，并且最多可以关联到另一个帖子。
4. 成员可以喜欢帖子和照片。

我是合金分析仪的初学者，正在尝试为上述社交网络建模。请帮助我，在此先谢谢！

Answer 1

您可以在https://github.com/vinahradau/finma的Z和Alloy中找到较大的规格。

这是我想出的Alloy Friends模型：

module Friends

sig Friends{
likes: Likable -> Member
}

sig Member{
friends: set Member 
}

sig Text{

}

abstract sig Likable{
author: one Member 
}

sig Photo extends Likable{
caption: one Text,
post: lone Post 
}

sig Post extends Likable{
text: one Text,
photo: set Photo
}

pred like(friends: Friends, member: Member, likable: Likable){
friends.likes = friends.likes ++ likable -> member 
}

fact{
all t : Text | all p1 : Photo | all p2 : Photo | t = p1.caption and t = p2.caption => p1 = p2 
all t : Text | all p1 : Post | all p2 : Post | t = p1.text and t = p2.text => p1 = p2 
all t : Text | all p1 : Photo | all p2 : Post | t = p1.caption => t != p2.text 
all m : Member | m not in m.friends 
all l : Likable | l.author not in Friends.likes[l] 
}

run like for 5 Friends, 5 Text, 5 Member, 5 Photo, 5 Post