Hi,
As some of you may be familiar, we have developed a web version of Alloy (and Electrum), called Alloy4Fun, that can be used to create models online and easily share models (and instances). It allows hiding some paragraphs in a model, which enables the sharing of small specification challenges, to be automatically checked for correctness with a hidden check command.
I was wondering if it would be a nice idea to share some challenges here, mainly for people that are learning the logic, but maybe also for others to have some fun. The idea would be to share a small model, with a very brief description (not too detailed on purpose) and the goal would be to guess the specification of the properties that should hold in that model. Part of the fun (or frustration, lets see…) is that you might end up not completely agree with the correct specification, but guessing what was in the challenger’s creator mind is part of the game.
Here is a first example of a challenge (this one is “pure” Alloy, no mutable relations nor temporal logic):
http://alloy4fun.inesctec.pt/AdWsm4H5pKGgCDJQK
Some notes:
- You should write your candidate spec (one or more properties) inside predicate
spec. You can actually change the rest of the model, but that is cheating
- If you press the execute button on the right you will either get a “No counter examples found” message, meaning you solved the challenge, or you will get a counter-example instance (already “beautified” with a minimal theme)
- Notice that the counter-example can either be an instance that holds in your (incorrect) spec but not in the correct one, or the other way around, so think carefully about which one is the case
- You can move the atoms around and ask for more counter-examples
Not sure if this is a good idea or just silly. Please let me know!
Good luck!
Alcino