# Alloy Authors - Practical Alloy - Structural modeling (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article1.be68295a7e40.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/50842145) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Alloy Authors]] **Full Title**:: Practical Alloy - Structural modeling **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [practicalalloy.github.io](https://practicalalloy.github.io/chapters/structural-modeling/index.html) **Host**:: [[practicalalloy.github.io]] **Highlighted**:: [[2025-04-25]] **Created**:: [[2025-04-26]] ## Highlights - There are two kinds of commands, both accepting an optional name and a formula enclosed in braces: `run` commands instruct the Analyzer to check the satisfiability of the given formula, yielding a satisfying instance if that is the case; `check` commands instruct the Analyzer to check the validity of the given formula, yielding a counter-example instance if that is not the case. ([View Highlight](https://read.readwise.io/read/01jsm9ykj0450nypp25k29ae8q)) ^881519097 - It is very common to require that some subset signatures are disjoint. Alloy has a special syntax to declare those: instead of `in`, the keyword `extends` should be used in the signature declaration. ([View Highlight](https://read.readwise.io/read/01jsmaazcsgkp5g3s367re4sd4)) ^881520523 - Actually, in Alloy properties can be specified with an extension 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. ([View Highlight](https://read.readwise.io/read/01jsnb1kx4tts5fc5fq7g6mmf5)) ^881684208 - A typical atomic formula in relational logic is a cardinality check: keyword `no` checks if a relation is empty; `some` checks if it is non-empty; `lone` checks if it has at most one tuple; and `one` checks if it has exactly one tuple. ([View Highlight](https://read.readwise.io/read/01jsnb6tv3r01a3scy9sv00n0r)) ^881684736 - However, it illustrates an important point about Alloy’s motto that “everything is a relation”. ([View Highlight](https://read.readwise.io/read/01jsnbnck9b820ya61aj76p1gp)) ^881686913 What is a relation? Examples: - Unary Relations (Sets): A relation with only one element per tuple (e.g., `{x, y, z}`). - Binary Relations: A relation that connects two elements (e.g., `{(x, y), (y, z)}`). - Higher-Arity Relations: Relations involving three or more elements (e.g., `{(x, y, z)}`). - The essential operator in relational logic is *composition*, the binary operator written as `.` (also known as *dot-join*). This operator allows us to navigate through fields to obtain related atoms. ([View Highlight](https://read.readwise.io/read/01jsnbfc5ymq18fjge76stpb1w)) ^881686570 - Another interesting usage is when composing a non-singleton set with a relation. For example, `Entry.name` is the set of all names of all entries and `Dir.entries` is the set of all entries that belong to some directory. ([View Highlight](https://read.readwise.io/read/01jsnbxs319kd6gegd7nvxv64m)) ^881687349 - 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, `entries.e` denotes the set of directories that contain entry `e`: this set can be empty, if `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. ([View Highlight](https://read.readwise.io/read/01jsnbza20dmswjved4jggh01r)) ^881687388 - For example, `d.entries.object` denotes the set of all file system objects that are contained in some entry of directory `d`. ([View Highlight](https://read.readwise.io/read/01jsnc1fta1zsx4famj9vy8v5q)) ^881687457 - For example, `entries.object.d` denotes the set of all directories that have some entry that points to directory `d`. ([View Highlight](https://read.readwise.io/read/01jsnc1a75dbf3t0r8e5vmfmr4)) ^881687454 Read as whose `entries.object` is `d`. - The need to quantify over two or more different variables is very common, so Alloy provides the modifier `disj`, that can be added between a quantifier and the variables, precisely to restrict those variables to be different. ([View Highlight](https://read.readwise.io/read/01jsnc3mxvyjmp53hj79qdd357)) ^881687517 - The `->` operator is the Cartesian product, here being applied to two singleton sets (two variables) to form a singleton binary relation (with a single tuple). Checking that this singleton binary relation is a subset of `entries` is just checking the membership of the respective tuple. ([View Highlight](https://read.readwise.io/read/01jsnd406y2sghj6qwq4d3dy96)) ^881695360 Field is a binary relation (set of 2-elements tuples) - The `iden` predefined binary *identity* relation contains all possible tuples of identical atoms. ([View Highlight](https://read.readwise.io/read/01jsnda659ty744ej9j3e215qw)) ^881699413 Set `{(a, a) for any a}` - The unary operator `~` reverses a binary relation, so `~entries` is a relation from entries to the directories containing it. ([View Highlight](https://read.readwise.io/read/01jsndc7eew0b7rjwefnfe5nzk)) ^881699998 - Fortunately, relational logic includes the so-called *transitive closure* operator (`^`) that when applied to a binary relation determines the binary relation that results from taking the union of all its possible compositions. ([View Highlight](https://read.readwise.io/read/01jsndp909vaw8hy37mnc0v7y3)) ^881700487 - In this definition we could also use a `let` expression to name the derived relation `entries.object`. ([View Highlight](https://read.readwise.io/read/01jsnzs0yperng9zmvmxa93486)) ^881763312 - To verify that this assertion is a consequence of all the facts that have been imposed before, we can use a `check` command. ([View Highlight](https://read.readwise.io/read/01jsp03pwns6vfyrb5stta2fmh)) ^881763611 Comment out `run` or use `Execute` menu to choose the command to run.