From 73ad0a8f0d8faca1ded69e2d0800bd543529b593 Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 16 Oct 2023 12:43:35 +0100 Subject: [PATCH] vault backup: 2023-10-16 12:43:35 --- 4a1s/MFES/PL - Aula 4.md | 29 ++++++++++++++++++++++------- 1 file changed, 22 insertions(+), 7 deletions(-) diff --git a/4a1s/MFES/PL - Aula 4.md b/4a1s/MFES/PL - Aula 4.md index 7d3f925..0942345 100644 --- a/4a1s/MFES/PL - Aula 4.md +++ b/4a1s/MFES/PL - Aula 4.md @@ -29,14 +29,14 @@ pred inv1 { 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 + 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 + 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 + all y:Photo | one posts.y } @@ -45,21 +45,36 @@ pred inv2 { all x: User | x->x not in follows //or - all x: User | x not in x:follows + 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 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) + + //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 } pred inv4 { // If a user posts an ad then all its posts should be labeled as ads. - + }