vault backup: 2023-10-16 12:53:35
This commit is contained in:
parent
73ad0a8f0d
commit
54d66491fe
1 changed files with 9 additions and 3 deletions
|
@ -69,24 +69,30 @@ pred inv3 {
|
||||||
|
|
||||||
//or
|
//or
|
||||||
all x :User, y :Photo | x in sees.y implies y in x.follows.posts + Ad
|
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 {
|
pred inv4 {
|
||||||
// If a user posts an ad then all its posts should be labeled as ads.
|
// If a user posts an ad then all its posts should be labeled as ads.
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
pred inv5 {
|
pred inv5 {
|
||||||
// Influencers are followed by everyone else.
|
// Influencers are followed by everyone else.
|
||||||
|
all x: Influencer | follows.x = User-x
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
pred inv6 {
|
pred inv6 {
|
||||||
// Influencers post every day.
|
// Influencers post every day.
|
||||||
|
all x: Influencer, y : Day | x.posts.date = y
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue