Alloy models may contain "open" statements, like this one:
open util/integer
The Alloy "open" statement is roughly similar to the Java "import" or the C/C++ "include" in that it tells the tool to look at some source in another file.
Alloy will look for util/integer.als in two places:
First of all, if the module is one of the sample model that comes with Alloy 4, it will load it.
This includes all the "util" modules
such as util/ordering and util/boolean, as well as the example models such as examples/algorithms/dijkstra.
You can see the list of sample models by clicking on the File menu, then click on "open sample models".
Failing that, it will infer the location of the file based on the location of the current model and the name of the current model.
For example, let's suppose we are analyzing the model "C:\Desktop\main.als"
with the following content:
model filesystem/main open filesystem/debug as DEBUG open filesystem/library/dirmodel as DIR open filesystem/library/filemodel as FILE
The "filesystem/debug" module is on the same level as "filesystem/main", so we will infer that it is at C:\Desktop\debug.als
The dirmodel and filemodel are in a subdirectory called "library", so we will infer that they are at C:\Desktop\library\dirmodel.als and C:\Desktop\library\filemodel.als