When you open up Alloy, the default run in the menu is “Run Default for 4 but 4 int, 4 seq expect 1.” I know what for 4 and but 4 int mean but I don’t know what “expect 1” means! Further, it doesn’t look like the spec mentions it at all. Does anyone here know?
We introduced the expect clause to support a kind of regression test script: expect N would mean that when you run the command, you expect N solutions. It turned out that counting solutions was too dependent on symmetry and other settings, so we reverted to 1 and 0 as the options. So expect 1 means that the command is expected to produce an instance; expect 0 means that no instances are expected.
Oh, how interesting! Is that useful for normal model authors in any way, or only for folks working on developing Alloy?
I find it very useful, since when I make some changes to a model I can just select Execute All and check if everything still executes “as expected”.