// Here is one solution to Exercise 2.
// Try commenting out some of the facts, and see what sort of
// models Alloy comes up with.
// e.g. What happens if we leave off "acyclic"? Or "zeroIsNotASuccessor"?
// Things called Numbers exist.
// Each number may have zero or one successors.
// (Why do we say zero or one? Ideally, *every* number should
// have a successor. But Alloy only creates small universes of finite
// sizes; in these universes, there *will* be a "largest number",
// which has no successor.
sig Number { successor : lone Number }
// There is a number called Zero.
one sig Zero extends Number {}
// Every number is either Zero, or Zero.successor,
// or Zero.successor.succesor, ... etc.
// (This forces Zero to be the "root" of our number system.)
fact zeroIsRoot {
all n : Number | n in Zero.*successor
}
// Numbers don't produce *cycles* (where a number
// is its own successor, for instance).
fact acyclic { no d: Number | d in d.^successor }
// Predicate for showing models.
// We ask to see models with more than 2 numbers.
pred show() {
#Number > 2
}
run show for 3