The theme to this tutorial is "lead by mistake". We will present you with an Alloy model which is well formed, but which initially makes some conceptual mistakes and has some shortcomings. We will then go through the process of identifying those mistakes, understanding why they occurred, and fixing them. We will iterate this process until we have a final draft.
We choose this approach, not only because it imitates the actual modeling process, but also because it will allow us to begin with a simple model, using only a small part of Alloy syntax, and gradually introduce complexities and more advanced syntax as it is needed. As a result, this tutorial will not introduce you to every Alloy command, but we will make sure you are comfortable with the important ones.
The goal of a writing a model is to describe some aspect of a system (but not the entire system), constrain it to exclude ill-formed examples, and check properties about it. For instance, you might describe the procedure a company uses to reroute mail internally, add some constraints about how the mail carriers behave, and then check to see if each piece of mail either gets to its destination or returned to sender. Your modeling tool (in this case, Alloy), would then either say "this property always holds for problems up to size X" or "this property does not always hold, and here is a counter example".
There are two kinds of problems that can arise:
Alloy is similar to several other existing languages and modeling techniques, but with several key differences.
We begin our tutorial with a simple model of a file system. It has a notion of a "file system object" which can be either a file or a directory. Every file system object knows its parent, and directories also know their contents. We will also create the notion of a "root directory", which resides at the top of the file system.
We will begin by defining files, directories, and file system objects, and make sure that they have the appropriate fields (parent, contents, etc.). We then show how to write simple facts to constrain the file system and to impose simple sanity constraints. For instance: every file system object must be either a file or a directory (not both, not neither); the file system is connected, the root has no parent; and so on.
It is easy to forget simple constraints like this, since they are so obvious to our intuition. We will show you how to view example file systems to make sure that they do not have any bizarre behaviour that you wished to preclude.
We will show you how to make assertions about properties you think (or hope) are true as a result of the sanity constraints you wrote. We'll show you how to check these assertions, and what to do when they fail to hold. For instance, we will verify that a file system is acyclic, even though we do not explicitly force it to be so.
The file system we write will have some shortcomings; most prominently, it will be static. In the following lessons, we will introduce dynamic operations, such as move and delete.
By the end of the first lesson, you will have written a simple static file system, constrained it to exclude ill-formed file-systems, and verified some properties about it.