.. _structural-design: Structural design with Alloy **************************** In this chapter we will explain how Alloy can be used to explore the design of a file system. The goal of the chapter is to introduce the key concepts of Alloy, namely the concept of signature field which was not introduced in the previous chapter, so our example will be purposely simple, a very high-level abstraction of a real file system. We will focus only on the structural aspects of the design, namely our main goal is to describe how files and directories are organised (the specification of dynamic designs is the focus of the next chapter). Given the high level of abstraction, our structural specification will resemble a domain model, formally describing the file system concepts and their relationships. Another goal of this design exploration is to elicit the set of constraints that characterise a well-formed file system. If later we develop a more detailed specification of the file system, namely of its operations, these would be the constraints we would like to verify to be kept invariant. Our final goal will be to verify that this set of constraints entails other relevant properties of a file system. In particular we are interested in verifying the property that no partitions occur in the file system, meaning that all files and directories are accessible from the root directory. Signature declaration ===================== .. index:: signature; signature declaration signature; parent signature First we will declare signatures to capture the concepts in a file system: directories and files. As we have seen in the previous chapter, a signature is a set that groups together some elements of our domain. Since both files and directories share some common properties, namely they can both appear in a directory, it is convenient to declare the respective signatures inside a top-level signature containing all file system objects. To declare a top-level signature we use the keyword :code:`sig` followed by the signature name and a list of field declarations between braces. For the moment we will not declare fields, so a signature containing all file system objects can be declared simply as follows. .. code-block:: sig Object {} .. index:: signature; subset signature To declare a subset signature, the keyword :code:`in` should be used after the signature name, followed by the name of the including (or *parent*) signature. For example, the two subset signatures of :code:`Object` containing the directories and files can be declared as follows. .. code-block:: sig File in Object {} sig Dir in Object {} .. index:: command; run In Alloy we typically start validating a design very early in the specification process, when the specification is still quite incomplete. The goal is to find design problems or specification errors as early as possible, and not let them amass to a point where debugging becomes very difficult. For example, we can immediately use a :code:`run` command to see some instances of our specification so far. .. code-block:: run example {} .. index:: instance A possible first instance returned by this command is the following. Recall that an instance is a valuation of the signatures (and fields, when the specification also declares those) that satisfies all the specified constraints, including the formula between braces in the case of :code:`run` command. A pair of empty braces is equivalent to true, so in this case we have no constraints imposed on our signatures. .. image:: instance1.png :width: 500 px :align: center .. index:: instance; exploration Alloy Analyzer; enumeration Here we have two objects, one of them is a directory and the other a file. If we press :guilabel:`New` in the visualizer toolbar we could get the following instance. .. image:: instance2.png :width: 500 px :align: center .. index:: Alloy Analyzer; options solver .. note:: Why am I not getting these instances?! The Analyzer relies on lower level `SAT `_ solvers to perform the analysis. Depending on the Analyzer version and the solver you have selected to perform the analysis, you might get instances in a different order than this. You can choose the underlying solver in the :guilabel:`Options` menu. However, irrespective of the selected solver, if you keep pressing :guilabel:`New` you will obtain all the possible (non-symmetric) instances of a specification, so you are guaranteed to obtain these. Recall that two instances are considered symmetric (or isomorphic) if they only differ in the naming of the atoms that inhabit signatures. In this instance we have a single object that is, simultaneously, a directory and a file. Obviously this is not something we wanted, but of course it is allowed since both :code:`File` and :code:`Dir` are arbitrary subsets of :code:`Object`. To disallow this we can add a constraint that forbids an object to be both a file and a directory, by specifying that :code:`File` and :code:`Dir` are disjoint sets. To impose this constraint in our specification we can specify it inside a :code:`fact`, as follows. .. code-block:: fact { no File & Dir } Recall that :code:`&` denotes set intersection and :code:`no` checks for set emptiness. If we re-execute the :code:`example` command, and iterate through our instances using :guilabel:`New` we will no longer see objects that are both files and directories, but we will eventually get an instance such as the following, where we have the problem of having an object (:code:`Object0`) that is neither a file nor a directory. .. image:: instance3.png :width: 500 px :align: center To solve this issue, we can add another constraint to our fact to require that :code:`Object` contains only atoms in :code:`File` or :code:`Dir`, by requiring that :code:`Object` is the union of both (recall that :code:`+` denotes set union and that constraints in different lines inside a fact are implicitly conjoined). .. code-block:: fact { no File & Dir Object = File + Dir } By re-executing the :code:`example` command and iterating through instances we can now confirm that the previous issues appear to be solved. .. index:: signature; sub-signature see: extends keyword; sub-signature see: in keyword, signature; subset signature It is very common to require that some subset signatures are disjoint. Alloy has a special syntax to declare those: instead of :code:`in`, the keyword :code:`extends` should be used in the signature declaration. For example, to introduce :code:`File` and :code:`Dir` as two disjoint subsets of :code:`Object` we should declare them as follows. .. code-block:: sig File extends Object {} sig Dir extends Object {} .. index:: command; check The first constraint in our fact is now redundant and can be removed. Actually, we can try to check that indeed it is redundant by issuing the following :code:`check` command that should yield no counter-example. Recall that a :code:`check` command verifies that, up to the specified scope, the formula declared between braces is implied by the declared facts. If that is not the case we will get a counter-example instance, one where the facts hold but the formula to be checked doesn't. .. code-block:: check { no File & Dir } .. index:: type-system type-system; irrelevance error constant; none When executing this command we actually get a warning: the Analyzer refuses to execute the command and tells us that the :code:`&` operator is irrelevant because the two sub-expressions that it is trying to intersect are disjoint. This is a warning issued by Alloy's type system and is one of the advantages of using :code:`extends` to declare disjoint subset signatures, instead of relying on :code:`in` and additional facts. The main goal of the type system of Alloy is to find so-called *irrelevant expressions*, essentially expressions that the Analyzer is sure to always denote an empty set and are thus most likely specification errors made by the user. If the user indeed wants to write an expression that always denotes an empty set the special constant :code:`none` should be used instead, making that intention explicit. More information about Alloy's type system can be found in [FSE04]_. Another advantage of using :code:`extends` is that in the visualizer atoms will be named according to the most specific signature they belong to, which simplifies the understanding of instances. For example, a possible instance returned by the :code:`example` command is the following, where it is now more clear that we have two files and one directory. .. image:: instance4.png :width: 500 px :align: center .. index:: signature; abstract Another frequent requirement for extension signatures is that they form a partition of the parent signature. This is the case of signature :code:`Object`, that is partitioned in two sets, :code:`File` and :code:`Dir`, and contains no atoms besides those already contained in its extensions. Again, instead of adding facts to ensure this, as we did with the constraint :code:`Object = File + Dir`, it is possible to declare a signature as *abstract*, by preceding its declaration with the keyword :code:`abstract`. Our specification of the file system objects can thus be just as follows, without any need for additional facts. .. code-block:: abstract sig Object {} sig File extends Object {} sig Dir extends Object {} .. index:: multiplicity constraint multiplicity constraint; lone keyword multiplicity constraint; one keyword multiplicity constraint; some keyword signature; multiplicity Now we would like to add a special object to denote the directory that is the root of the file system. In Alloy it is not possible in a specification to refer (and name) directly atoms that inhabit signatures. There is however a trick to do so. Signature declarations can be preceded by a *multiplicity constraint* that restricts the cardinality of that signature. There are three multiplicities that can be used in a signature declaration: :code:`some` forces the signature to always have some atoms; :code:`lone` restricts the signature to have at most one atom; and :code:`one` restricts the signature to have exactly one atom. To have a specific atom for the root directory, we can thus declare with multiplicity :code:`one` a signature :code:`Root` that extends :code:`Dir`. .. code-block:: one sig Root extends Dir {} :code:`Root` will always be a singleton set that contains the atom that will be the root directory of the file system. Since it is declared with :code:`extends`, that atom will also be named :code:`Root` in the instance visualiser. A possible instance returned by the :code:`example` command is the following, where we have three directories, one of them being (necessarily) the root directory. .. image:: instance5.png :width: 500 px :align: center .. index:: signature; enumeration signature .. tip:: Enumeration signatures. In Alloy it is very common to use extension signatures of multiplicity :code:`one` in the declaration of signatures that behave like enumerated data types. For example, the following specification declares a :code:`Color` signature that contains exactly three colours: :code:`Red`, :code:`Green`, and :code:`Blue`. .. code-block:: abstract sig Color {} one sig Red, Green, Blue extends Color {} Here we see another feature of the Alloy language: if two or more signatures share the same features (multiplicity, parent signature, etc) they can all be defined together in the same declaration. This pattern for declaring signatures that essentially correspond to enumerated data types is so common, that Alloy has a keyword :code:`enum` for that purpose. Using this keyword, the :code:`Color` signature could be declared as follows. .. code-block:: enum Color { Red, Green, Blue } However, there is a subtle difference between declaring enumeration signatures with keyword :code:`enum` and with the normal :code:`sig` keyword with multiplicity :code:`one`: the former additionally imposes a total order between the respective atoms, corresponding to the order in which they are declared inside the braces. Later we will see how total orders can be used in Alloy. Objects inside directories have an associated name, so we will need a signature to represent the latter. In our file system model we will allow files to be (hard) linked, meaning that the same file can have different names in different directories (or even inside the same directory). As such, we will also introduce a signature :code:`Entry` that will later be used as a (kind of) record to pack together an object inside a directory and the respective name. .. code-block:: sig Entry {} sig Name {} .. index:: Int signature String signature .. note:: Why not just use strings for names!? The reader may wonder if Alloy has any predefined types, such as integers or strings. If that is the case, why not just use strings to represent names, instead of declaring a new signature :code:`Name`? Actually, Alloy does have predefined types, namely :code:`Int` for (bounded) integers and :code:`String` for strings. However, these types should be avoided as much as possible, because their semantics is substantially more tricky than that of normal signatures, and analysis can be confusing and somehow crippled when using them (in particular with strings). Actually, in many cases they just have too much semantics for the intended use: for example, strings can be concatenated and there is the notion of one string being a substring of another, but for the file system specification none of this is of interest when specifying the abstract concept of a name. The only thing we will need in this case is to check for name equality, and normal signatures and atoms already provide us that basic semantics. People also tend use integers when they actually need something much more simple, semantics wise. For example, we sometimes need to specify a signature where there is some total order imposed and, in first sight, integers are very convenient for that. However, integers have a more rich semantics than just being a total order, and we can easily axiomatise a total order on a signature with some simple facts and thus avoid the analysis drawbacks that come with their usage (see :ref:`integers`). So, when should you use :code:`String` or :code:`Int`? The former has very little use, and actually, even if recognised by the Analyzer, is not even part of standard Alloy. The latter is sometimes useful, for example when you do need to perform arithmetic operations, such as additions or subtractions. A possible instance of our specification so far is the following, with two different names, two entries, one file and two directories, one of which is the root. .. image:: instance6.png :width: 500 px :align: center .. index:: scopes scopes; setting scopes scopes; exact scopes see: for keyword; seting scopes Recall that all analysis commands are executed with a (user definable) scope for each signature, that sets the maximum number of atoms that can inhabit it. By default, the scope is 3 for all top-level signatures: in our example this means that instances will have at most 3 names, 3 entries, and 3 objects. With this scope, instances with, for example, 3 files, will not be possible, because the root always exists and consumes 1 of the 3 atoms that can inhabit :code:`Object`. To change the default global scope the keyword :code:`for` followed by the desired scope should be used. You can also set a different scope for each top-level or extension signature (another difference from declaring signatures with :code:`in`), by using the keyword :code:`but` followed by a comma separated list with different scopes for each signature. You can also set an exact scope for a signature with the keyword :code:`exactly`, meaning that that signature will always be inhabited by the exact number of specified atoms. For example, to execute the :code:`example` command with a default scope of 4, up to 2 entries, and exactly 3 names, the scope should be set as follows. .. code-block:: run example {} for 4 but 2 Entry, exactly 3 Name Note that in this case, the only top-level signature that will be subject to the default scope of 4 is :code:`Object`, since specific scopes are given for the other two top-level signatures. Multiplicities on signature declarations also affect the scope: for example, a signature with multiplicity :code:`one` will always have scope of exactly 1, and an error will be thrown if you try to set an incompatible scope. There is also some interaction between the scope of extension signatures and the scope of the respective parent signatures. In particular, if the scope of extension signatures enforces a minimum number of atoms, the scope defined for the parent signature will automatically grow to accommodate that minimum number. For example, in the following command the scope of :code:`Object` will automatically grow to 4 since :code:`Object` must contain at least the root and three files. .. code-block:: run example {} for 3 but 2 Object, exactly 3 File Field declaration ================= .. index:: fields fields; field declaration relation; binary Having declared our signatures we now proceed with the declaration of *fields*. Fields are declared inside the braces of a signature declaration, and are essentially mathematical *relations* (sets of tuples) that connect atoms of the enclosing signature to other atoms (of the same or other signatures). In our example we will need a relation that connects each directory with the respective set of entries. This binary relation, which will be named :code:`entries`, is a set of ordered pairs, where the first atom of each pair is a directory and the second atom is an entry. The type of the first atoms in the tuples that form a relation dictates the signature in which it must be declared as a field. In the case of :code:`entries`, since it relates atoms of signature :code:`Dir` to atoms of signature :code:`Entry`, it must be declared as a field in the former signature. To do so, we change the declaration of :code:`Dir` as follows. .. code-block:: sig Dir extends Object { entries : set Entry } .. index:: multiplicity constraint; set keyword As we can see, a field declaration consists of its name followed by a colon and the target set, optionally preceded be a multiplicity declaration. In this case the target set is signature :code:`Entry` and the multiplicity is :code:`set`, meaning that one atom of signature :code:`Dir` can be related by :code:`entries` to an arbitrary number of atoms of signature :code:`Entry`. The other options for the multiplicity are the same that can be used in signature declarations: :code:`one`, :code:`lone`, or :code:`some`. If no multiplicity is given, the default is :code:`one`. In this book we will avoid this implicit multiplicity in field declarations, and always explicitly state the multiplicity of a field, even if it is :code:`one`. By executing command .. code-block:: run example {} we could now get the following instance. .. image:: instance7.png :width: 500 px :align: center Binary relations are depicted by the Analyzer using labelled arrows: each arrow is a pair contained in the relation, whose first atom is the source of the arrow and whose second atom is the target. In this case, relation :code:`entries` is a set that contains three pairs: :code:`(Dir,Entry0)`, :code:`(Dir,Entry1)`, and :code:`(Root,Entry2)`. In this example we have a directory :code:`Dir` with two entries and the :code:`Root` with one entry, but given the :code:`set` multiplicity constraint it would also possible to have directories without any entries. .. index:: relation; arity .. note:: Actually, everything is a relation! In chapter :ref:`overview` we alerted the reader to the fact that in Alloy every expression denotes a set. To be more precise, every expression in Alloy denotes a relation - a set of tuples - hence the Alloy motto: *everything is a relation!* In Alloy we can declare relations of arbitrary *arity*: the arity is the size of the tuples contained in it. Relation :code:`entries` is a binary relation of arity 2. Later we will see how to declare relations of higher arity, for example ternary relations of arity 3. However, signatures are in fact also relations of arity 1: they are sets of tuples of size 1. For example, in the previous instance, signature :code:`Dir` contains the following unary tuples: :code:`(Dir)` and :code:`(Root)`. Do not to confuse the name of the atom :code:`Dir` with the signature name :code:`Dir`: the former is just an automatically-generated name for one of the two inhabitants of the latter! When we start using relational logic operators to write constraints, it will be more clear why the fact that everything denotes a relation considerably simplifies the syntax and semantics of the language. .. index:: Alloy Analyzer; evaluator .. tip:: The evaluator. The Alloy instance visualiser has an evaluator that can be used to compute the value of any expression. To access this evaluator just press the :guilabel:`Evaluator` button in the toolbar of the instance visualiser window. Every expression denotes a relation. The visualiser depicts the values of the signatures and fields of an instance as labelled graphs. Another way to depict the value of a relation (of any arity) is as a table where each line is one of the tuples contained in it. This is the default way the evaluator will show the values of relational expressions. To ask for the value of an expression just type it in the evaluator and press :kbd:`Enter`. For example, here is the result of asking in the evaluator what is the value of relations :code:`Dir` and :code:`entries`. .. image:: evaluator1.png :width: 600 px :align: center The evaluator is sometimes very useful to debug your constraints: besides asking for values of relational expressions you can also ask for the values of formulas, so it is a very convenient way, for example, to know what sub-formulas of a constraint are true or not in a particular instance. To close the evaluator and return to the normal instance visualizer just press the :guilabel:`Close Evaluator` button in the toolbar. Section :ref:`evaluator` presents the evaluator in more detail. Besides :code:`entries` we will declare two more fields in our specification: the first, that we will call :code:`name`, relates each entry in a directory with the respective name; the second, that we will call :code:`object`, relates each entry in a directory with the respective file system object (either a file or a directory). Both these relations should be declared inside signature :code:`Entry` and both will have multiplicity :code:`one`, since exactly one target atom is associated with each entry. Because of this, an entry acts like a record that packs together an object inside a directory and the respective name. In section :ref:`higher-arity` we will see how this association (between directories, their contents, and the respective names) can alternatively be modelled by a ternary relation. .. code-block:: sig Entry { name : one Name, object : one Object } Let's change our :code:`run` command to ask directly for a more complex instance of our specification, namely one with a larger global scope of 4, and necessarily containing some files and some directories besides the root (recall that :code:`-` is the set difference operator, and that keyword :code:`some`, besides being used as a multiplicity constraint in declarations, can be used in formulas to check if a set (or relation) is non-empty). .. code-block:: run example { some File some Dir - Root } for 4 Executing this command could yield the following instance. .. image:: instance8.png :width: 500 px :align: center Here we can immediately see some problems with our specification, for example entries shared between directories or files not belonging to any directory. As our specification grows, instances become increasingly difficult to understand, and so, before adding facts to our specification to solve these issues, we will first see how the theme can be customised to simplify the visualisation of instances. .. _theme-customisation: Theme customisation =================== .. index:: themes; customisation To open the theme customisation menu, press the button :guilabel:`Theme` in the toolbar of instance visualiser window. The first customisation we will apply is to show the names of directory entries as attributes in the respective atoms, instead of using arrows pointing to the name. This will unclutter substantially the depiction and is a very common customisation for fields of multiplicity :code:`one`, in particular for fields that somehow act as identifiers, as is the case of :code:`name`. To do so, first select the field :code:`name`, and then tick the :guilabel:`Show as attribute` option in the top pane. This option will show the name of an entry as an attribute but still keep the respective arrows. To remove them, tick twice :guilabel:`Show as arcs` to choose the :guilabel:`Off` option. Your theme options for relation :code:`name` should look as follows. .. image:: theme1.png :width: 700 px :align: center By pressing :guilabel:`Apply` in the toolbar and then :guilabel:`Close` the instance will now be depicted as follows. .. image:: instance9.png :width: 600 px :align: center We now have some unconnected :code:`Name` atoms. Since names were only used in directory entries, where they are now shown as attribute, we can remove them from the graph. To do so, select :guilabel:`Theme` again (actually when changing many options it is better to keep the theme customisation menu open and just keep pressing :guilabel:`Apply` without closing it to see the effect), select the :code:`Name` signature, and then tick the :guilabel:`Show` option twice to choose the :guilabel:`Off` option. After pressing :guilabel:`Apply` the :code:`Name` atom will disappear. .. image:: theme2.png :width: 700 px :align: center Another common customisation is to give different colours (or different shapes) to atoms belonging to different signatures. First, we will select a different colour palette, with more subdue colours. First select the :guilabel:`general graph settings`, and select the :guilabel:`Martha` (for Martha Stewart) palette both for node and edge colours. After pressing :guilabel:`Apply` we will get some nice faded colours. .. image:: theme3.png :width: 700 px :align: center Since entries are auxiliary structures in defining the (supposedly) tree-like structure of the file system, we will paint them grey. To do so select signature :code:`Entry`, then the colour :guilabel:`Gray` in the drop-down menu in the top left-hand corner, and finally :guilabel:`Apply`. .. image:: theme4.png :width: 700 px :align: center For file system objects we will choose a more eye-catching red colour. We don't have to set this colour separately for :code:`Dir` and :code:`File`. By default most theme options of extension signatures are set as inherited from their parent signature. As such, it suffices to set the colour red for the :code:`Object` signature, and both their children will inherit this setting. Finally we will choose different shapes for different file system objects. Let's keep files as rectangles, but choose the shape :guilabel:`Trapezoid` for directories and a :guilabel:`House` for the root. The shape can be chosen in the drop-down menu in the top right-hand corner. After pressing :guilabel:`Apply` we have the following visualization. .. image:: theme5.png :width: 700 px :align: center .. index:: themes; magic layout For the moment these are all the customisations we will use, and so we can close the theme customisation menu. Notice that you can always reset your theme settings by going to the menu option :menuselection:`Theme --> Reset theme`. You can also save your theme for later use in the option :menuselection:`Theme --> Save theme`. Instead of customising manually your theme, you can also try out the :guilabel:`Magic Layout` button in the toolbar of the instance visualiser. This will "magically" choose options for visualising the different elements of your specification: sometimes the results are good enough and it will save you some work. The result of magic layout for our instance is the following. .. image:: instance10.png :width: 500 px :align: center More information about how the magic layout actually works can be found in [LED07]_. In this case we prefer our handmade customisation and so we will load back our previously saved theme by selecting :menuselection:`Theme --> Load theme`. .. image:: instance11.png :width: 500 px :align: center Property specification ====================== By inspecting the above instance we can easily detect several problems in our specification, namely: * Shared entries between directories (entry :code:`Entry3` belongs both to :code:`Dir` and :code:`Root`). * Different entries in the same directory with the same name (all entries inside :code:`Dir` have the same name :code:`Name`). * The same directory appears in more than one entry (:code:`Dir` is the object of all entries). * A file that does not belong to an entry (:code:`File`) .. index:: relational logic single: predicate, logic We should write facts to prevent these issues. In Alloy, formulas in facts are written in a variant of first-order logic called *relational logic*. Relational logic extends first-order logic with so called *relational operators*, that can be used to combine (or compose) relations (which in first-order logic are known as *predicates*) to obtain more complex relations. We have already seen some of these operators, namely the classic set operators such as intersection (:code:`&`), union (:code:`+`), and difference (:code:`-`). Notice that every relation (of any arity) is a set of tuples, so these can be applied to any relation. Let's suppose, for example, we have two binary relations, :code:`mother` and :code:`father`, that relate a person with the respective mother and father. Then the relation that gives the parents of a person can be obtained by taking the union of both, namely :code:`mother+father`. .. index:: relational operator; composition The essential operator in relational logic is *composition*, the binary operator written as :code:`.` (a dot). This operator allows us to navigate through the declared fields to obtain related atoms. Understanding how this operator works is key to be proficient in Alloy. Here, we will explain its informal semantics by means of several examples: the detailed semantics and more examples will be given in chapter :ref:`relational-logic`. In particular we will focus on the simplest, and most frequent, use of this operator, namely when applied to a set and a binary relation. For example, suppose :code:`e` is a singleton set containing an :code:`Entry` and :code:`d` a singleton set containing a :code:`Dir`. These could be, for example, parameters of a predicate or instantiated as result of a quantifier. To obtain the name of an entry you can compose it with relation :code:`name`: relational expression :code:`e.name` denotes the name of :code:`e`. Since :code:`name` is a field with multiplicity :code:`one`, the result of this composition is necessarily a singleton set. Similarly, :code:`e.object` is the singleton set with the file system object that is contained in entry :code:`e`. The notation is, on purpose, similar to that of accessing an attribute of an object in an object-oriented programming language, as the effect is essentially the same when dealing with singleton sets. However, we can also apply it to relations with multiplicity different than :code:`one` and arbitrary sets. For example, :code:`d.entries` retrieves the set of all entries in directory :code:`d`. This set can be empty or contain an arbitrary number of entries, since relation :code:`entries` has multiplicity :code:`set`. A more interesting usage is when composing a non-singleton set with a relation. For example, :code:`Entry.name` is the set of all names of all entries and :code:`Dir.entries` is the set of all entries that belong to some directory. Also, you are not forced to compose a set followed by a relation: the other way around also works. Relations can be navigated forwards, from the source signature to the target signature, but also backwards from the target signature to the source one. For example, :code:`entries.e` denotes the set of directories that contain entry :code:`e`: this set can be empty, if :code:`e` is not contained in any directory, or even have more than one directory, since when declaring a field there are no multiplicity restrictions imposed on the source signature. We can also compose with an arbitrary set on the right-hand side: for example, :code:`entries.Entry` is the set of all directories that contain some entry. Compositions can be chained to obtain atoms that are somehow indirectly related. For example, :code:`d.entries.object` denotes the set of all file system objects that are contained in the entries of directory :code:`d`. And again, it is possible to navigate backwards through composition chains. For example, :code:`entries.object.d` denotes the set of all directories with entries that contain directory :code:`d`. Having understood how :code:`.` works, we can now declare a fact that prevents the first issue identified above. We can almost directly transliterate the natural language requirement to relational logic. Given any two different directories :code:`x` and :code:`y`, the property that there should be no common entries between both can be specified as :code:`no (x.entries & y.entries)`: first we determine the intersection of the two sets of entries of both directories, and then we check that this set is empty using the keyword :code:`no`. To complete our first property specification we just need to universally quantify over all different directories :code:`x` and :code:`y` (recall that :code:`all` denotes the universal quantification of first-order logic). .. code-block:: fact { // Entries cannot be shared between directories all x, y : Dir | x != y implies no (x.entries & y.entries) } .. index:: quantifier; disj The need to quantify over two ore more different variables is very common, so Alloy provides the modifier :code:`disj`, that can be added between the quantifier and the variables, precisely to restrict those variables to be different. This modifier simplifies the formulas, since we no longer need the implication to indirectly restrict the range of the quantification. Using this modifier, our property can be restated as follows. .. code-block:: fact { // Entries cannot be shared between directories all disj x, y : Dir | no (x.entries & y.entries) } As expected there are many different ways to specify the same property. In the case of this property, a simpler formula can be obtained by navigating backwards in the :code:`entries` relation, and specifying instead that for every entry :code:`e` there should be at most one directory in the set :code:`entries.e`, the set of all directories that contain :code:`e` as an entry. This alternative formulation would look as follows. Recall that :code:`lone` can be used to check if a set contains at most one atom. .. code-block:: fact { // Entries cannot be shared between directories all e : Entry | lone entries.e } .. index:: multiplicity constraint; multiplicity arrow Alloy has a special formula syntax to directly restrict the multiplicities of both end points of a binary relation. For example, to state that a relation :code:`r` relates every atom of source signature :code:`A` to at most one atom of target signature :code:`B`, and every atom of :code:`B` to at least one atom of :code:`A`, we could write the formula :code:`r in A some -> lone B`. Not stating a multiplicity next to an end point is the same as having multiplicity :code:`set`. With this special syntax, we could have yet another alternative formulation of our first constraint. .. code-block:: fact { // Entries cannot be shared between directories entries in Dir lone -> Entry } .. index:: relation; injective relation; surjective relation; simple relation; entire relation; function relation; representation relation; abstraction relation; injection relation; surjection relation; bijection .. note:: A bestiary of binary relations. The constraint :code:`entries in Dir lone -> Entry` forces relation :code:`entries` to be *injective*, one where no two atoms of the source signature point to the same target atoms. This is one of the four basic properties of relations we can obtain by varying the multiplicities of the source and target signatures. If we had :code:`entries in Dir some -> Entry` we would have a *surjective* relation, one where every atom of the target is related to some source atom. If :code:`entries in Dir -> lone Entry` relation :code:`entries` would be *simple* (or a *partial-function*), a relation where every source atom is related to at most one target. And if :code:`entries in Dir -> some Entry` relation :code:`entries` would be *entire* (or *total*), since every source atom is related to at least one target. By combining these four properties we get additional well-known relation types. A relation that is both entire and simple is a *function*: every atom of the source is related to exactly one target. A *representation* is a relation that is both entire and injective, and dually, an *abstraction* is a relation that is both simple and surjective. An *injection* is a function that is also a representation, and a *surjection* is a function that is also an abstraction. Finally, by combining all four basic properties we get a *bijection*: a one-to-one mapping between the source and the target signatures. The following table summarises these properties. .. table:: :align: center +---------------------+---------------------+---------------------+---------------------+ | injective | entire | simple | surjective | +---------------------+---------------------+---------------------+---------------------+ | :code:`A lone -> B` | :code:`A -> some B` | :code:`A -> lone B` | :code:`A some -> B` | +---------------------+-------+-------------+-------------+-------+---------------------+ | representation | function | abstraction | +-----------------------------+---------------------------+-----------------------------+ | :code:`A lone -> some B` | :code:`A -> one B` | :code:`A some -> lone B` | +-----------------------------+-------------+-------------+-----------------------------+ | injection | surjection | +-------------------------------------------+-------------------------------------------+ | :code:`A lone -> one B` | :code:`A some -> one B` | +-------------------------------------------+-------------------------------------------+ | bijection | +---------------------------------------------------------------------------------------+ | :code:`A one -> one B` | +---------------------------------------------------------------------------------------+ To enforce that different entries in the same directory have different names we could write the following fact. .. code-block:: fact { // Different entries in the same directory must have different names all d : Dir, disj x, y : d.entries | x.name != y.name } Here you can see another nice feature of Alloy's syntax: it is possible to quantify over any expression and not only over signatures. In this case, :code:`x` and :code:`y` will be instantiated with all the (distinct) atoms belonging to :code:`d.entries`, the set of entries of each directory :code:`d`. An alternative formulation of this property is the following. .. code-block:: fact { // Different entries in the same directory must have different names all d : Dir, n : Name | lone (d.entries & name.n) } Expression :code:`d.entries & name.n` denotes the set of entries in directory :code:`d` that also have name :code:`n`. This set must contain at most one entry for every directory :code:`d` and name :code:`n`. To prevent the third issue we can enforce that each directory is contained in at most one entry as follows. .. code-block:: fact { // A directory cannot be contained in more than one entry all d : Dir | lone object.d } Note that it would be wrong to specify this property as :code:`object in Entry lone -> Dir`, since this would force relation :code:`object` to only relate entries to directories (excluding files). The last issue is a an example of a broader problem: there is nothing in our specification that forces all objects except the root to belong to an entry. To specify such a constraint, we can begin by determining the set of all objects that are contained in any entry using expression :code:`Entry.object`, and then enforce that this set is equal the set of all objects minus the root. .. code-block:: fact { // Every object except the root is contained somewhere Entry.object = Object - Root } After adding these four facts, if we re-execute the :code:`example` command and iterate with :guilabel:`New` we could get the following instance. .. image:: instance12.png :width: 500 px :align: center The problems identified above are now gone, but we still have two issues (the second already present in the previous instance): * Entries not belonging to any directory. * Directories contained in themselves. To address the first issue we could just strengthen the first fact introduced above to demand that every entry belongs to one and exactly one directory. .. code-block:: fact { // Entries must belong to exactly one a directory entries in Dir one -> Entry } Concerning the second issue, to forbid directories from containing themselves as entries, we can use the previously described expression :code:`d.entries.object` to determine the objects contained in a directory :code:`d`. Then we just need to forbid :code:`d` itself from being a member of this set. .. code-block:: fact { // Directories cannot contain themselves all d : Dir | d not in d.entries.object } Re-executing again command :code:`example` and iterating a couple of times with :guilabel:`New` reveals no more issues. Obviously, it is impossible to manually inspect all possible instances, so we will proceed with the verification of our desired assertion, namely that the file system contains no partitions. Assertion verification ====================== .. index:: assert To specify this assertion we need to determine the set of all objects that are reachable from the root. We have already seen how to determine the set of objects that are directly contained in a directory. Namely, :code:`Root.entries.object` is the set of objects directly contained in the :code:`Root` directory. The set of objects reachable from :code:`Root` contains not only these, but also the objects that they contain, which can be determined as .. code-block:: Root.entries.object.entries.object Of course, we also need to include the objects contained in these, and so on, and so on. Essentially, we would like to determine the following set: .. code-block:: Root.entries.object + Root.entries.object.entries.object + Root.entries.object.entries.object.entries.object + ... .. index:: relational operator; transitive closure The problem is how to fill in the :code:`...` in this expression: ultimately the number of times we need to compose :code:`entries.object` depends on the size of our file system, and we would like our specification to be independent of this value. Fortunately, relational logic includes a so-called *transitive closure* operator (:code:`^`) that when applied to a binary relation (or relational expression) determines the binary relation that results from taking the union of all its possible compositions. Essentially, given a relation :code:`r`, :code:`^r` is the same as :code:`r + r.r + r.r.r + ...`. Seeing our instances as labelled graphs, the expression :code:`x.^r` will determine the set of all atoms that can be reached from atom :code:`x` by navigating in one or more steps via arrows labelled with :code:`r`. Transitive closure is the reason why relational logic is strictly more expressive than first-order logic: our desired assertion could not be expressed in first-order logic alone. By using transitive closure applied to relational expression :code:`entries.object` we can determine the set of all objects reachable from root. To ensure that there are no partitions, this set must contain all objects (except the root itself). Our desired assertion can thus be specified as follows. .. code-block:: assert no_partitions { // Every object is reachable from the root Object - Root = Root.^(entries.object) } .. index:: command; check To verify that this assertion is a consequence of all the facts that have been imposed before, we can define a :code:`check` command. .. code-block:: check no_partitions Unfortunately, executing this command reveals a counter-example. .. image:: instance13.png :width: 400 px :align: center The problem is that we have two directories that contain each other. Fortunately, this counter-example is not an issue in real file systems, but exposes a problem in our specification. One of the facts specified above imposed that no directory can contain itself, but this alone is not sufficient: a directory cannot contain itself directly, nor indirectly. To fix that fact, we can again use the transitive closure operator to determine the set of all objects reachable from any directory :code:`d`, and then disallow :code:`d` from being a member of this set. .. code-block:: fact { // Directories cannot contain themselves directly or indirectly all d : Dir | d not in d.^(entries.object) } Re-executing the :code:`check` command no longer yields counter-examples. Although with the bounded analysis performed by the Analyzer we can never be entirely sure that the assertion is valid, we can set a higher scope to increase our confidence that that is indeed the case. .. code-block:: check no_partitions for 6 .. tip:: Be sure your specification is still consistent! You should always be wary of the results of checking your assertions, in particular when they yield no counter-examples. Recall that a :code:`check` command checks that an assertion is implied by the conjunction of all declared facts. If your facts are inconsistent, in the sense that their conjunction is false, or admit only very trivial instances (for example empty ones), your assertion can be trivially true. For example, in this example we changed one of the facts before our final check that yielded no counter-examples. We should have checked that this change did not accidentally make our specification inconsistent. To do so we could execute a :code:`run` command after the final check, and iterate a bit through the returned instances to make sure the specification is still consistent and admits non-trivial file systems. Of course, just pressing :guilabel:`New` is not the ideal method to check if expected file system examples are still possible. In section :ref:`testing` we will see how to define :code:`run` commands that behave like unit tests that directly search for specific instances of a specification. So far we used only a reduced subset of all relational logic operators that are part of Alloy's syntax. We did use the two most important ones, composition (:code:`.`) and transitive closure (:code:`^`), and with these alone (plus the standard set theory operators) it is possible to write most facts and assertions of interest. For a complete list of relational logic operators please see the :ref:`relational-logic` chapter. .. _higher-arity: Using higher-arity relations ============================ .. caution:: This chapter is still under construction .. code-block:: abstract sig Object {} sig File extends Object {} sig Dir extends Object { contents : Name -> Object } one sig Root extends Dir {} sig Name {} fact { // Different entries in the same directory must have different names all d : Dir, n : Name | lone n.(d.contents) } fact { // A directory cannot be contained in more than one directory all o : Dir | lone contents.o } fact { // Directories cannot contain themselves directly or indirectly all d : Dir | d not in d.^{ d : Dir, o : Object | some d.contents.o } } fact { // Every object except the root is contained somewhere Name.(Object.contents) = Object - Root } Exercises ========= #. To practice relational logic, access the following Alloy4Fun models and specify all the listed constraints. Each constraint is specified in a separate predicate, and for each there is a command that can be used to check its correctness. If the constraint is not correctly specified a counter-example will be shown. The counter-example will include an atom that clarifies if it is an example that the incorrect constraint is currently rejecting but should be accepted or one that is currently being accepted but should be rejected. a. `Photo sharing social network `_ #. `Graphs `_ #. `Production line `_ #. `Train station `_ #. `Courses `_ #. Specify the `Git Object Model `_ using Alloy. Focus on the connection between the different kinds of objects and ignore details like authors or committers. Start with a version that abstracts away the hashes that identify the objects and connect them directly instead. In a second version add the explicit hashes and the constraints that characterize them. Try to customize the visualizer theme to simplify to comprehension of instances. In particular, in the second version with explicit hashes, try to define auxiliary relations that can be used in the visualizer to depict the connections between the objects. #. Specify `Red-Black Trees `_ using Alloy. To specify the constraint that "every path from a given node to any of its descendant NIL nodes goes through the same number of black nodes" you can use the cardinality operator (:code:`#`), but be careful with the scope of :code:`Int` (the scope sets the desired bit-width). Try to customize the visualizer theme to simplify to comprehension of instances.