// 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