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”.
(post deleted by author)
Hello,
I’m using expect in my run commands. However, the CLI Alloy Analyzer produces the same result regardless of the use of expect. Is there any way I can show the result of a command as SAT when it produces no instance, as expected?
Ps: I’m using Alloy-6-2.0
Thank you!