My Evening With Alloy

Warning: The following is boring project related blather. Terminology has been altered so the reader might find it more amusing than it really is. But, really folks, there is only so much I can do with this stuff…

I spent most of last night working on my project. Part of my project involves working with an automatic model checking tool called Alloy. Working with Alloy is a lot like working with some sort of mute idiot-savant three-year-old that finds contradicting you to be hilarious. You know the types of little brats that insist on disagreeing with you on everything. That’s pretty much Alloy, except Alloy has a freaky grasp of first-order logic too.

Much like a three year old, Alloy has a limited vocabulary. So if you want to try to express a complicated concept you have to make an effort to figure out how to best express it in terms Alloy will understand. You can’t just tell a three year old that “Mommy is never coming home again because she was caustic, emotionally dead inside, fat, and got what was coming to her.” You have to use terms that a three-year-old will understand. I usually use something along the lines of “Mommy had to go away because she felt that you didn’t love her enough. She prefers to spend time with all of your pets that ran away in the middle of the night.”

Once you get past how to best describe something to Alloy, you get to try to take advantage of its idiot-savant ability at checking complex models….the only thing is Alloy finds it hilarious to contradict you. In fact, it insists upon only citing counter examples.

So if I ask Alloy if I’m wearing shoes, it just shrugs. If I state that I am not wearing shoes, then Alloy perks up and promptly whips out a Polaroid of my feet wearing shoes. This gets to be even more fun if I’m interested in some future possibility.

Me: “Alloy, I am wearing shoes.”
Alloy: shrug.
Me: “Alloy, I am never not wearing shoes”
Alloy: Whips out a Polaroid of me getting dressed this morning, without shoes on.
Me: “Alloy, at some point in the future I am wearing shoes.”
Alloy: shrug.
Me: “Alloy, at some point in the future I am never not wearing shoes.”
Alloy: Whips out a Polaroid of me, later tonight, with my feet up, not wearing shoes.
Me: “Hey neat trick.”

And so it goes. Except for last night, the conversation went closer to something like this.

Me: “Alloy, at some point in the future I am never not wearing shoes.”
Alloy: shrug.
Me: “Okay then. Alloy, in the future I am always wearing shoes.”
Alloy: Produces a Polaroid of me from the future without feet.
Me: “Uh, that’s disturbing. Alloy, at some point in the future I have feet.”
Alloy: shrug.
Me: “Err…. Alloy, I have feet at this very moment.”
Alloy: Produces a Polariod of me in my current clothes without feet.
Me: “That’s not right!” Looks down and notices my feet are missing. “Arghghghggh!”