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.
