Practical Alloy

https://practicalalloy.github.io/
Admin
Practical Alloy is a hands-on guide to formal software design, introducing structural and behavioral...
Tokens:119,761
Snippets:1,080
Trust Score:9.7
Update:6 days ago
Show doc for...
Tokens:
Raw
### Run example command with scope 4

Source: https://practicalalloy.github.io/chapters/structural-modeling/index.html

Runs the 'example' command with a scope of 4, changing the default scope for analysis.

```alloy
run example {} for 4

```

--------------------------------

### Run empty command to get any satisfying instance

Source: https://practicalalloy.github.io/chapters/behavioral-modeling/index.html

Defines an empty run command named 'example' to ask for any instance that satisfies all declared facts)Skip any provided context. Return ONLY valid JSON. Ensure all required escapes are applied.

```alloy
run example {}
```

--------------------------------

### Alloy: composition example - non-empty directories

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `entries.Entry` step by step, showing the resulting set of directories that contain entries.

```alloy
entries.Entry
= {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0),(Entry1),(Entry2),(Entry3)}
= {(Root),(Dir0)}

```

--------------------------------

### Kodkod relations and bounds for file system example

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/model-finding/index.html

Shows the relations and their lower- and upper-bounds that the Analyzer generates for the file system example under the scope of 2, as passed to Kodkod.

```text
Root    = {(Root0)} {(Root0)}
Dir$    = {}        {(Object0)}
File    = {}        {(Object0)}
Entry   = {}        {(Entry0),(Entry1)}
Name    = {}        {(Name0),(Name1)}

entries = {}        {(Root0,Entry0),(Root0,Entry1),(Object0,Entry0),(Object0,Entry1)}
object  = {}        {(Entry0,Root0),(Entry1,Root0),(Entry0,Object0),(Entry1,Object0)}
name    = {}        {(Entry0,Name0),(Entry1,Name1),(Entry0,Name1),(Entry0,Name1)}

```

--------------------------------

### Alloy: composition example - entries inside root

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates the composition `Root.entries` step by step, showing the resulting set of entries.

```alloy
Root.entries
= {(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
= {(Entry0),(Entry1),(Entry2)}

```

--------------------------------

### Alloy: composition example - names of entries inside root

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `Root.entries.name` step by step, showing the resulting set of names.

```alloy
Root.entries.name
= {(Entry0),(Entry1),(Entry2)}.name
= {(Entry0),(Entry1),(Entry2)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
= {(Name0),(Name2),(Name1)}

```

--------------------------------

### Example value of singleton signature 'Root'

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Shows the value of the singleton signature 'Root' in the example instance, a unary relation with a single atom.

```alloy
Root = {(Root)}

```

--------------------------------

### Complete instance values for all signatures and fields

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Lists the values of all signatures and fields in the example instance, including Object, Dir, Root, File, Entry, Name, entries, object, and name.

```alloy
Object   = {(Root),(Dir0),(Dir1),(File)}
Dir      = {(Root),(Dir0),(Dir1)}
Root     = {(Root)}
File     = {(File)}
Entry    = {(Entry0),(Entry1),(Entry2),(Entry3)}
Name     = {(Name0),(Name1),(Name2)}

entries  = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
object   = {(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}
name     = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}

```

--------------------------------

### Alloy: cartesian product example - all possible associations between files and names

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `File->Name` step by step, showing the resulting set of pairs.

```alloy
File->Name
= {(File)} -> {(Name0),(Name1),(Name3)}
= {(File,Name0),(File,Name1),(File,Name3)}

```

--------------------------------

### Run Command with Predicate Constraint

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Adapts the `example` run command to enforce `no_self_containment` as a predicate, since it is no longer a fact.

```alloy
run example { no_self_containment }

```

--------------------------------

### Alloy: intersection example - directories inside root

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `Root.entries.object & Dir` step by step, showing the resulting set of directories.

```alloy
Root.entries.object & Dir
= Root.{(Root,File),(Root,Dir0),(Dir0,Dir1)} & Dir
= {(File),(Dir0)} & {(Root),(Dir0),(Dir1)}
= {(Dir0)}

```

--------------------------------

### Alloy: composition example - binary relation between directories and contained objects

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `entries.object` step by step, showing the resulting binary relation.

```alloy
entries.object
= {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}
= {(Root,File),(Root,Dir0),(Dir0,Dir1)}

```

--------------------------------

### Alloy: set difference example - all directories except root

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `Dir - Root` step by step, showing the resulting set of directories.

```alloy
Dir - Root
= {(Root),(Dir0),(Dir1)} - {(Root)}
= {(Dir0),(Dir1)}

```

--------------------------------

### Example values of field 'name' as a binary relation

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Shows the value of the field 'name' in the example instance, a binary relation with four pairs.

```alloy
name = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}

```

--------------------------------

### Example value of signature 'Dir' as a unary relation

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Shows the value of the signature 'Dir' in the example instance, a unary relation with three atoms.

```alloy
Dir = {(Root),(Dir0),(Dir1)}

```

--------------------------------

### Run command: everything_happens

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/meta/index.html

Guarantees that every mutable element is eventually populated. For the file sharing example, this produces a trace with 5 states.

```alloy
run everything_happens {
  all v : var$ | eventually some v.value
}

```

--------------------------------

### Set scope for command with for and but

Source: https://practicalalloy.github.io/chapters/structural-modeling/index.html

Executes the example command with a default scope of 4 for top-level signatures, but up to 2 entries and exactly 3 names.

```alloy
run example {} for 4 but 2 Entry, exactly 3 Name

```

--------------------------------

### Values of predefined relations none, univ, and iden

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Shows the values of the predefined relations 'none', 'univ', and 'iden' in the example instance.

```alloy
none = {}
univ = {(Root),(Dir0),(Dir1),(File),(Entry0),(Entry1),(Entry2),(Entry3),(Name0),(Name1),(Name2)}
iden = {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}

```

--------------------------------

### Alloy model with util/ordering and exact scope

Source: https://practicalalloy.github.io/_sources/chapters/structural-topics/topics/ordering/index.rst.txt

This Alloy model uses util/ordering to totally order an abstract signature Nat, with Even and Odd subtypes. The fact requires alternating successors and that first is Even and last is Odd. Running the example command with the default scope of 3 for Nat yields no instance because the ordering module forces an exact scope, making the constraints unsatisfiable; changing the scope to 4 produces an instance.

```alloy
open util/ordering[Nat]

abstract sig Nat {}
sig Even, Odd extends Nat {}

fact {
  all n : Even | n.next in Odd
  all n : Odd | n.next in Even
  first in Even
  last in Odd
}

run example {}
```

--------------------------------

### Static declarations for file sharing model

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/meta/index.html

Defines the signatures Token, Attribute, File, Text, Binary, and Link for the file sharing example. File has attributes and shared fields, Text and Binary extend File, and Link extends File with a link field.

```alloy
sig Token {}

sig Attribute {}

sig File {
  attributes : set Attribute,
  var shared : set Token
}

sig Text, Binary extends File {}

sig Link extends File {
  link : one File
}

```

--------------------------------

### run all_initiate: correct command with sufficient message scope

Source: https://practicalalloy.github.io/chapters/protocol-design/index.html

Runs the same scenario as bad_all_initiate but with exactly 6 Message, which is sufficient to find a trace. Note that Elected is now a binary relation.

```Alloy
run all_initiate {
  all n : Node | eventually initiate[n]
  eventually Node = Elected.Node
} for exactly 3 Node, exactly 6 Message

```

--------------------------------

### run example_unique_generator: generate unique network configuration

Source: https://practicalalloy.github.io/chapters/protocol-design/index.html

Runs the generator with the unique predicate for 3 Node and 10 Message. This guarantees that New Config returns a different network configuration (different ring or order of node identifiers).

```Alloy
run example_unique_generator {
  generator
  unique
} for 3 Node, 10 Message

```

--------------------------------

### Check commands for induction conditions

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/inductive-invariants/index.html

These check commands verify the initiation and preservation conditions with a scope of 1 and 2 steps respectively.

```Alloy
check init_inv_shared_are_accessible for 10 but 1 steps
check pres_inv_shared_are_accessible for 10 but 2 steps
```

--------------------------------

### Check command: shared_are_accessible

Source: https://practicalalloy.github.io/chapters/behavioral-modeling/index.html

Example of a check command with an implicit scope on top-level signatures, here checking configurations with up to 3 files and up to 3 tokens.

```alloy
check shared_are_accessible

```

--------------------------------

### Activate meta-capabilities with run some_sig

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/meta/index.html

This run command activates Alloy's meta-capabilities by referencing the meta-signature sig$. It is trivially true in non-empty models and introduces meta-signatures into the instance.

```alloy
run some_sig {
  some sig$
} for 2

```

--------------------------------

### Alloy: domain restriction example - identity relation on objects

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/relational-logic/index.html

Evaluates `Object <: iden` step by step, showing the resulting identity relation restricted to objects.

```alloy
Object <: iden
= {(Root),(Dir0),(Dir1),(File)} <: {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}
= {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File)}

```

--------------------------------

### no_shared_dirs fact for ternary contents field

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/nary-relations/index.html

Adapts the no_shared_dirs fact to the ternary field. Uses contents.d to get a binary relation of directories and names, and restricts to at most one with lone.

```Alloy
fact no_shared_dirs {
  // A directory cannot be contained in more than one entry
  all d : Dir | lone contents.d
}

```

--------------------------------

### Simplified initial fact with only no File

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/mutable-toplevel-signatures/index.html

Simplified version of the `init` fact that removes the redundant `no shared` constraint, since an empty `File` implies an empty `shared` relation.

```alloy
fact init {
  // Initially there are no files uploaded nor shared
  no File
}

```

--------------------------------

### run command with parameterized predicate and Skolemization

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Defines a predicate 'empty_dir' with a parameter 'd : Dir' and runs it. The Analyzer performs Skolemization, adding a subset '$empty_dir_d' to instances to represent the quantified variable.

```alloy
pred empty_dir [d : Dir] {
  no d.entries
}

run empty_dir for 3

```

--------------------------------

### Run command with scope for Dir only

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Assigns a specific scope to Dir but not to File. Since File is the only extension without a specific scope, it gets the remaining scope from Object (3 - 3 = 0), so the command yields no instance.

```alloy
run dirs_3 { some File } for 3 but 3 Dir

```

--------------------------------

### unique_names fact for ternary contents field

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/nary-relations/index.html

Adapts the unique_names fact to a ternary contents field. Uses n.(d.contents) to get objects assigned name n in directory d and restricts to at most one with lone. Parentheses are required because composition associates to the left.

```Alloy
fact unique_names {
  // Different entries in the same directory must have different names
  all d : Dir, n : Name | lone n.(d.contents)
}

```

--------------------------------

### Run command with overall scope 3

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Declares a run command with an overall scope of 3. Because the scope applies to top-level signatures, the Object signature gets 3 atoms, but one is consumed by the Root singleton, so only 2 atoms are available for files or non-root directories.

```alloy
run scope_3 {} for 3

```

--------------------------------

### Run command with exact scopes

Source: https://practicalalloy.github.io/chapters/protocol-design/index.html

Run command to generate configurations with exactly 3 nodes and 3 identifiers.

```Alloy
run example3 {} for exactly 3 Node, exactly 3 Id

```

--------------------------------

### Declare a sequence field with seq in Alloy

Source: https://practicalalloy.github.io/chapters/behavioral-topics/topics/sequences/index.html

Declares a mutable sequence field 'trashed' of type seq uploaded in a singleton signature Trash. The sequence is used to store files in the trash bin, sorted from oldest to newest. The example also declares Token and File signatures, and a var sig uploaded in File.

```alloy
sig Token {}

sig File {
  var shared : set Token
}
var sig uploaded in File {}

one sig Trash {
  var trashed : seq uploaded
}

```

--------------------------------

### Define empty_dirs function to highlight empty directories

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/visualization/index.html

Parameterless function returning a set of Dir. The visualizer evaluates it after solving and shows it as a subset labeled '$empty_dirs'. Use it to highlight empty directories without affecting analysis performance.

```alloy
fun empty_dirs : set Dir {
  Dir - entries.Entry
}

```

--------------------------------

### Run command with generator axiom for exactly 3 nodes

Source: https://practicalalloy.github.io/chapters/protocol-design/index.html

A run command named 'example3_generator' that invokes the generator predicate with a scope of exactly 3 Node and 6 Message. The Message scope is twice the Node scope to allow one message of each type per node.

```alloy
run example3_generator {
  generator
} for exactly 3 Node, 6 Message

```

--------------------------------

### Run command with scope 2 (all_entries_dir)

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/model-finding/index.html

Runs a command named all_entries_dir that searches for instances where all entries point to directories, using a scope of 2.

```alloy
run all_entries_dir {
  Entry.object in Dir
} for 2

```

--------------------------------

### check command with empty constraint

Source: https://practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Shows a check command labeled 'no_partitions' but with an empty constraint, which is equivalent to true and never finds counter-examples. Warns against confusing command labels with predicate names.

```alloy
check no_partitions {}

```

--------------------------------

### Pointwise delete and download predicates

Source: https://practicalalloy.github.io/_sources/chapters/behavioral-topics/topics/pointwise-effects/index.rst.txt

Pointwise specifications for 'delete' and 'download'. 'delete' updates 'trashed' and clears 'f.shared'. 'download' updates 'shared.t' and uses a universal quantifier over other tokens. Both include frame conditions for 'uploaded' and 'trashed'.

```alloy
pred delete [f : File] {
  f in uploaded - trashed                  // guard
  trashed' = trashed + f                   // effect on trashed
  no f.shared'                             // effect on f.shared
  all g : File - f | g.shared' = g.shared  // no effect on other shared files
  uploaded' = uploaded                     // no effect on uploaded
}

pred download [t : Token] {
  some shared.t                             // guard
  no shared'.t                              // effect on shared.t
  all u : Token - t | shared'.u = shared.u  // effect on other shared tokens
  uploaded' = uploaded                      // no effect on uploaded
  trashed' = trashed                        // no effect on trashed
}
```
Tokens:
Raw