108 lines
No EOL
2.2 KiB
Markdown
108 lines
No EOL
2.2 KiB
Markdown
16 Outubro 2023 - #MFES
|
|
|
|
## Alloy4Fun
|
|
|
|
```c
|
|
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 posts and y->z in posts implies x=y
|
|
|
|
// or (equivalent to 2nd formula)
|
|
all x,y : User, z: Photo | x in posts.z and y in posts.z implies x=y
|
|
|
|
// or (equivalent to 1st and 2nd formula)
|
|
all y: Photo | some posts.y
|
|
all y: Photo | lone posts.y
|
|
|
|
// or (equivalent to 1st and 2nd formula)
|
|
all y:Photo | one posts.y
|
|
}
|
|
|
|
|
|
pred inv2 {
|
|
// Users cannot follow themselves.
|
|
all x: User | x->x not in follows
|
|
|
|
//or
|
|
all x: User | x not in x.follows
|
|
}
|
|
|
|
|
|
pred inv3 {
|
|
// Users can see ads posted by everyone,
|
|
// but only see non ads posted by followed users.
|
|
all x : User, y :Photo | x->y in sees implies (y in Ad) or
|
|
(all z:User | z->y in posts implies x->z in follows)
|
|
|
|
//or
|
|
all x :User, y :Photo | x in sees.y implies (y in Ad) or
|
|
(all z:User | z in posts.y implies z in x.follows)
|
|
|
|
//or
|
|
all x :User, y :Photo | x in sees.y implies (y in Ad) or
|
|
(posts.y in x.follows)
|
|
|
|
//or
|
|
all x :User, y :Photo | x in sees.y implies (y in Ad) or
|
|
(y in x.follows.posts)
|
|
|
|
//or
|
|
all x :User, y :Photo | x in sees.y implies y in x.follows.posts + Ad
|
|
|
|
//or
|
|
all x :User, y :Photo | y in x.sees implies y in x.follows.posts + Ad
|
|
|
|
//or
|
|
all x :User | x.sees in x.follows.posts + Ad
|
|
}
|
|
|
|
|
|
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.
|
|
all x: Influencer | follows.x = User-x
|
|
}
|
|
|
|
|
|
pred inv6 {
|
|
// Influencers post every day.
|
|
all x: Influencer, y : Day | x.posts.date = y
|
|
}
|
|
|
|
|
|
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.
|
|
|
|
}
|
|
``` |