vault backup: 2023-10-16 12:23:35
This commit is contained in:
parent
fe0dac55f0
commit
6922a46e3d
1 changed files with 13 additions and 3 deletions
|
@ -26,13 +26,23 @@ sig Day {}
|
|||
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
|
||||
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
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue