Alloy has two commands for checking the ‘world’:
check asks if a property is true in every world in the collection described by the format text (code). It tries to find a counter example, and if you ask it to it will try to find all counter examples.
run generates all examples of a property. So it doesn’t fail with counter examples or anything.
A note about scope
These commands only check within a scope – the maximum size of the world, because otherwise it could be infinite (e.g. checking against every possible integer etc).
A world is measured in terms of the number of atoms in each signature. The size of each signature can be given as a range, or exactly. The default is 4 for everything.
Problems with scopes
They may be too small apparently. This got a bit confusing.