1.1 KiB
1.1 KiB
16 Outubro 2023 - #MFES
Alloy4Fun
sig User {
follows : set User,
sees : set Photo,
posts : set Photo,
suggested : set User
}
sig Influencer extends User {}
sig Photo {
date : one Day
}
sig Ad extends Photo {}
sig Day {}
// Specify the following properties.
// You can check their correctness with the different commands and
// when specifying each property you can assume all the previous ones to be true.
pred inv1 {
// Every image is posted by one user.
all y: Photo | some x: User | x->y in posts
all x,y : User, z: Photo | x->z in posta
}
pred inv2 {
// Users cannot follow themselves.
}
pred inv3 {
// Users can see ads posted by everyone,
// but only see non ads posted by followed users.
}
pred inv4 {
// If a user posts an ad then all its posts should be labeled as ads.
}
pred inv5 {
// Influencers are followed by everyone else.
}
pred inv6 {
// Influencers post every day.
}
pred inv7 {
// Suggested are other users followed by followed users, but not yet followed.
}
pred inv8 {
// A user only sees ads from followed or suggested users.
}