Alice/my_digital_garden
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

vault backup: 2023-10-16 12:43:35

Browse source
This commit is contained in:
Alice 2023-10-16 12:43:35 +01:00
parent dc84ec14c2
commit 73ad0a8f0d
1 changed files with 22 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
4a1s/MFES/PL - Aula 4.md
View file

@ -29,14 +29,14 @@ pred inv1 {
all x,y : User, z: Photo | x->z in posts and y->z in posts implies x=y all x,y : User, z: Photo | x->z in posts and y->z in posts implies x=y
// or (equivalent to 2nd formula) // or (equivalent to 2nd formula)
all x,y : User, z: Photo | x in posts: z and y in posts: z implies x=y 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) // or (equivalent to 1st and 2nd formula)
all y: Photo | some posts: y all y: Photo | some posts.y
all y: Photo | lone posts: y all y: Photo | lone posts.y
// or (equivalent to 1st and 2nd formula) // or (equivalent to 1st and 2nd formula)
all y:Photo | one posts: y all y:Photo | one posts.y
} }
@ -45,15 +45,30 @@ pred inv2 {
all x: User | x->x not in follows all x: User | x->x not in follows
//or //or
all x: User | x not in x:follows all x: User | x not in x.follows
} }
pred inv3 { pred inv3 {
// Users can see ads posted by everyone, // Users can see ads posted by everyone,
// but only see non ads posted by followed users. // but only see non ads posted by followed users.
all x : User, y :Photo | x->y sees implies (y in Ad) or 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) (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
} }