diff --git a/4a1s/MFES/PL - Aula 4.md b/4a1s/MFES/PL - Aula 4.md index a2a49ce..92be624 100644 --- a/4a1s/MFES/PL - Aula 4.md +++ b/4a1s/MFES/PL - Aula 4.md @@ -26,20 +26,30 @@ 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 } pred inv3 { // Users can see ads posted by everyone, // but only see non ads posted by followed users. - + }