Section 4 · Reading Alloy configuration

The three basic parts of an Alloy configuration file

Estimated time: 1 min

Configuration file anatomy

To read an Alloy configuration, start by recognizing its parts. An Alloy configuration file is made of attributes, expressions, and blocks. These elements describe the settings and behavior that Alloy loads.

Attributes

Attributes are key = value pairs that configure individual settings:

Alloy
url = "http://localhost:9090"

Here, url is the attribute name. The value on the right side of = comes from an expression.

Expressions

Expressions compute the values that attributes use. An expression can be:

  • A constant, such as "localhost:9090"
  • A calculation, such as (1 + 2) * 3
  • A standard library call, such as sys.env("HOME")

Alloy evaluates an expression before assigning its result to an attribute. There is a fourth kind of expression, a reference to another component’s export, that you trace later in this section.

Blocks

Blocks group related attributes and nested blocks between { and }. Most blocks you read define components. A component block has a name and a label:

Alloy
local.file "example" {
  filename = "/tmp/example.txt"
}

Here, local.file is the component name, "example" is the label, and filename is an attribute inside the block.