From 6922a46e3d44bda4945629aad296062aa24496be Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 16 Oct 2023 12:23:35 +0100 Subject: [PATCH] vault backup: 2023-10-16 12:23:35 --- 4a1s/MFES/PL - Aula 4.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) 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. - + }