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