my_digital_garden/4a1s/MFES/PL - Aula 4.md

16 Outubro 2023 - #MFES 

## Alloy4Fun

```c
sig User {
	follows : set User,
	sees : set Photo,
	posts : set Photo,
	suggested : set User
}

sig Influencer extends User {}

sig Photo {
	date : one Day
}
sig Ad extends Photo {}

sig Day {}
// Specify the following properties.
// You can check their correctness with the different commands and
// when specifying each property you can assume all the previous ones to be true.

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 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
	
	//or
	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 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
	
	//or
	all x :User, y :Photo | y in x.sees implies y in x.follows.posts + Ad
	
	//or
	all x :User | x.sees in x.follows.posts + Ad
}


pred inv4 {
	// If a user posts an ad then all its posts should be labeled as ads. 

}


pred inv5 {
	// Influencers are followed by everyone else.
	all x: Influencer | follows.x = User-x
}


pred inv6 {
	// Influencers post every day.
	all x: Influencer, y : Day | x.posts.date = y
}


pred inv7 {
	// Suggested are other users followed by followed users, but not yet followed.
	
}


pred inv8 {
	// A user only sees ads from followed or suggested users.

}
```