Got Tripped at Alloy4Fun Photo Sharing Social Network

Hello, I have been looking at Alloy thanks to hwayne and glad to come back see Alloy 6 extended with temporal logic! I am trying to get back to learning Alloy and going through the Alloy 6 book. And I am a bit embarrassed I got tripped right at the first exercise.

In Exercise 1.a. of Structural design with Alloy, the photo sharing social network model, we have pred inv3:

// Users can see ads posted by everyone,
// but only see non ads posted by followed users.

Intuitive enough, I put in my constraints. But I get this counterexample:


As I read it, it says it should be rejected that a user sees a photo they themselves posted.

Uhh, excuse me? Which photo sharing social network considers it reasonable to prohibit a user from seeing photos they themselves posted?

This really shocked me, because coming from the flow of the book, I was having fun finding non-sensical instances Alloy generates from the under-constrained file system spec. Here it seems so hilariously over-constrained.

Reading it over 3 times, as well as looking at several more test cases, I finally got where I misunderstood: User.sees in the model does not mean what the user can see, that is what is permitted to the user, but what is presented to the user in a Instagram like stream. The stream does not present a user’s own posts.

The shock also comes from how it is a different game: instead of translating a well written intensional description into Alloy, using extensional intuition to verify the sensibleness, this game is now more akin to detective work, figuring out intensional specification from extensional test cases. It really shows the value of Alloy in helping bridge the gap between intensional and extensional understanding, especially for a newcomer getting to know an existing model. But the aftertaste of the shock feels more bitter than necessary. At the moment it did not feel like empowerment, but rather deflating, even betrayal.

Such may be the uncanny valley of misunderstanding. I suppose I would not feel this way either if the description is very well written, or if the game is fully adversarial and gives barely any description if at all.



Indeed. We were not sure about including these Alloy4Fun exercises in the book, and maybe they will not be included in the final version. We use them in classes where students can play the game with the tutor in person, so I believe a bit less frustrating.

Yes, but I also see some educational value in trying to figure out what exactly a (maybe not so well-written) requirement means.

If you like that, I did propose some challenges in that style - just search for “Guess the spec” in this forum.


That’d be a shame. :slightly_smiling_face:

I’m not an educator, but from the POV of someone following along: the initial impression was that the exercise was a bit rough. This statement veers close to making it feel like a cheap gotcha.

IDK how realistic this want is, but when I go through the first exercise of the book and am told it’s to practice relational logic, I’d like to have as few other things to worry about to start with.

Note: this is a minor gripe in something I am grateful was made. Kudos!

I found and finished “Guess the spec #1” and it was a lot of fun! Thank you for making them.

Hi, I’ve also been struggling with the inv3 predicate. I started with the simple definition u.sees = Ad + u.follows.posts, but got a counterexample where an influencer posts an ad but doesn’t see it. It took me some time to understand that sees might miss some photos that the user can see. I wonder if renaming sees to seen would make it clearer?