Alloy has two commands for checking the ‘world’:

check

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

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).

Scopes

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.