4

I have in front of me an Alloy model composed of different modules (files). The main module (the one containing the command) does not contain any signature declaration, only a command and some facts.

This model enforces that only one instance can possibly be satisfiable but after analysis, several satisfiable instances are found. I investigated the differences between the generated instances to discover that a Univ signature appeared magically (in addition to the built-in univ signature). The difference between each instance generated come from the number of atoms belonging to that mysterious addition.

After adding a signature to the main module, the Univ signature disappeared. It seems that the Alloy analyzer adds this signature by itself when no signature declarations are found in the module containing the command executed. Is this behavior generally desired ? If so, why ?

The simplest way to reproduce this behavior is to have a module containing only: run {}

Loïc Gammaitoni
  • 4,173
  • 16
  • 39

1 Answers1

3

I believe that this particular case is a bug. The original motivation is that when you have no sigs defined (at all), and just want to check some property over the built-in relations (e.g., unit, iden, none), unless a sig exists, the analyzer won't be able to produce instances with more than 0 atoms. That's why the Univ sig is automatically generated in those cases. The current implementation fails to check if the imported modules define any sigs, so in those cases, as you already realized, you end up with the mysterious Univ sig. You also correctly pointed out that an easy workaround would be to add a dummy empty sig to the module where your command is defined, e.g., 

sig Dummy {}
fact { no Dummy }

You should also check the latest experimental version, because this bug may be fixed there (not sure though).

Aleksandar Milicevic
  • 3,837
  • 1
  • 13
  • 17