Hi,
Things have been very quiet around here, so here is new challenge: http://alloy4fun.inesctec.pt/ZtHaFHkZZuTT4trsQ
Just to recall how this works:
- You should write your candidate specification (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
And a tip that can help: if you write a false formula inside predicate spec, for example some none, you will only see instances that satisfy the correct specification.
Have fun,
Alcino