In order to ensure the model-finding problem is decidable, the Alloy Analyzer performs model-finding over restricted scopes consisting of a user-defined finite number of objects.
Um sicherzustellen, dass das Problem der Modellsuche entscheidbar ist, führt der Alloy Analyzer eine Modellsuche über einem beschränkten Gültigkeitsbereich bestehend aus einer endlichen Anzahl benutzerdefinierter Objekte aus.