Larger scope to make sure?

Questions
1

I’m looking into it too early in learning alloy, probably, but I’m curious, what scope do alloy practitioners usually use. I’ve found the following in an old paper:

The dirty work of finding solutions (or looking for counterexamples to universal claims) is left to the sophisticated SAT systems on which Alloy is built. One must make compromises, of course – Alloy cannot express higher order constructs, and it is limited to searching finite state spaces – but in practice these compromises are rarely problematical. If a counterexample to a claim cannot be found in a relatively small state space, say 3-5 atoms per signature, then it is highly unlikely (but not impossible) that a counterexample exists in an infinite universe.

Scope of 3 to 5 seems surprisingly low, that’s why I’m asking.

The more you want to be sure, the larger the scope, right? What is the largest scope you’ve seen in use?

2

Notice first that the scope can be different for every signature in your model. But yes this is usually low due to the combinatorial explosion problem. This is less an issue that it may seem: @DanielJackson’s insight when creating Alloy is what he called the small scope hypothesis, which says that, for many models, if a property can be violated, it can be violated for a small scope. Small scopes are also effective in a “positive” mode, when you want to explore possible instances and don’t necessarily need big, overwhelming instances.

When considering traces as in Alloy 6, a larger scope is often needed to witness interesting behaviors, so the default scope for traces is 10.

1 Like