Alloy Syntax Guide

sig Person {}           -- A set of Person atoms
sig File {}             -- A set of File atoms
sig Empty {}            -- Can be empty (zero atoms)

one sig Root {}           -- Exactly one atom
lone sig Config {}        -- Zero or one atom
some sig Node {}          -- At least one atom
abstract sig Entity {}    -- No direct atoms (only via extensions)

abstract sig Animal {}
sig Cat extends Animal {}
sig Dog extends Animal {}

sig Person {}
sig Employee in Person {}
sig Manager in Employee {}

sig Person {}
sig Student, Faculty in Person {}
-- Student and Faculty can overlap (a Person can be both)

-- To make them disjoint, add a fact:
fact { no Student & Faculty }
-- Or use disj in quantifiers:
-- all disj s: Student, f: Faculty | ...

sig Person {
    name: one String,        -- Exactly one name (required)
    spouse: lone Person,     -- Zero or one spouse (optional)
    children: set Person,    -- Zero or more children
    parents: some Person     -- One or more parents (at least one)
}

sig File {
    parent: one Folder,      -- File -> Folder
    owner: one User          -- File -> User
}

sig Person {
    -- For each Person, maps Organizations to Roles
    membership: Organization -> Role
}

sig Object {
    -- Access control: Subject -> Permission mapping
    access: Subject -> Permission
}

sig Node {
    edges: set Node
}

-- Self-loops allowed by default; prevent with fact:
fact NoSelfLoops {
    no n: Node | n in n.edges
}

-- Symmetric relation (bidirectional edges):
fact Symmetric {
    all n1, n2: Node | n1 in n2.edges implies n2 in n1.edges
}

sig Person {
    father: lone Person,
    mother: lone Person
}

p.father          -- p's father (a Person or empty)
p.father.father   -- p's paternal grandfather
p.(father + mother)  -- p's father or mother

Cat + Dog                    -- All cats and dogs
p.father + p.mother          -- p's parents
read + write                 -- Union of permissions

Employee & Manager           -- People who are both
trusted & external           -- Trusted external entities

Person - Employee            -- Non-employees
all - allowed                -- Forbidden items

sig File {
    parent: one Folder
}

~parent                      -- Folder -> File (children)
f.~parent                    -- Files in folder f

sig Folder {
    parent: lone Folder
}

f.^parent                    -- All ancestors of f
^parent                      -- The ancestor relation
n in n.^parent               -- n is its own ancestor (cycle!)

f.*parent                    -- f and all its ancestors
*parent                      -- The "ancestor or self" relation

User -> File                 -- All user-file pairs
alice -> secret              -- Specific pair
Person -> Person -> Action   -- Ternary relation

Employee <: salary           -- salary restricted to Employees
trusted <: access            -- access for trusted entities only

knows :> Employee            -- knowing relationships to Employees
access :> ReadOnly           -- access limited to read-only perms

defaults ++ customSettings   -- custom overrides defaults
oldState ++ (key -> newValue)  -- Update specific mapping

#Person                      -- Number of persons
#(p.friends)                 -- Number of p's friends
#File > 0                    -- At least one file exists

all p: Person | p.age >= 0
all f: File | one f.parent
all x, y: Node | x.edge = y implies y.edge = x

some p: Person | p.age > 100
some f: File | no f.parent
some x, y: Node | x != y and x in y.edge

no p: Person | p.age < 0
no f: Folder | f in f.^parent
no disj x, y: Node | x.edge = y.edge

one p: Person | p.name = "Alice"
one f: File | f.size = max[File.size]

lone p: Person | p.role = CEO
lone f: File | no f.parent

all disj x, y: Person | x.id != y.id
some disj a, b, c: Node | a->b + b->c in edge

-- Conjunction
all p: Person | p.age >= 0 and p.age <= 150

-- Disjunction
all f: File | f.public or some f.owner

-- Implication
all p: Person | p.employed implies some p.salary

-- Biconditional
all x: Node | x.root iff no x.parent

-- Negation
all p: Person | not p in p.^parent

fact NoSelfEmployment {
    no p: Person | p in p.manages
}

fact AcyclicHierarchy {
    all p: Person | p not in p.^manages
}

-- Anonymous fact (no name)
fact {
    all f: File | some f.owner
}

pred isManager[p: Person] {
    some p.manages
}

pred canAccess[u: User, f: File] {
    f in u.owns or f in u.sharedWith
}

pred wellFormed {
    all f: File | some f.parent
    no f: Folder | f in f.^parent
}

fun parents[p: Person]: set Person {
    p.father + p.mother
}

fun ancestors[p: Person]: set Person {
    p.^(father + mother)
}

fun commonFriends[p1, p2: Person]: set Person {
    p1.friends & p2.friends
}

-- Functions can return relations
fun familyRelation: Person -> Person {
    father + mother + ~father + ~mother
}

assert NoOrphans {
    all f: File | some f.parent or f in RootFolder
}

assert TransitiveClosure {
    all p: Person | p.ancestor = p.^parent
}

assert PermissionConsistency {
    all u: User, f: File |
        canRead[u, f] implies canAccess[u, f]
}

{ p: Person | p.age > 21 }           -- Adults
{ f: File | no f.owner }             -- Unowned files
{ x: Node | x in x.^next }           -- Nodes in cycles

{ p: Person, f: File | f in p.owns } -- Ownership pairs
{ x, y: Node | x->y in edges }       -- Edge pairs

fun adults: set Person {
    { p: Person | p.age >= 18 }
}

pred allFilesOwned {
    no { f: File | no f.owner }
}

pred complexCondition[p: Person] {
    let parents = p.father + p.mother,
        siblings = parents.~(father + mother) - p |
    some siblings and #parents = 2
}

fun reachable[start: Node]: set Node {
    let direct = start.edges,
        indirect = direct.^edges |
    direct + indirect
}

run {}                           -- Any valid instance
run { some File }                -- Instance with files
run wellFormed                   -- Instance where predicate holds
run { #Person = 3 }              -- Exactly 3 persons

check NoOrphans                  -- Find counterexample
check PermissionConsistency      -- Verify property
check { all f: File | some f.owner }  -- Inline assertion

run {} for 5                     -- 0 to 5 of each signature
run {} for 3 File, 2 Folder      -- 0-3 Files, 0-2 Folders
run {} for exactly 3 Person      -- Exactly 3 (not 0 to 3)
run {} for 5 but 2 Int           -- 5 default, but 2-bit integers (-2 to 1)

check NoOrphans for 10           -- Check with 0-10 atoms per signature
check NoOrphans for 3 but 5 File -- 0-3 default, 0-5 files

run {} for 3 expect 1            -- Expect satisfiable
check NoOrphans expect 0         -- Expect no counterexample

module filesystem

sig File { ... }
sig Folder { ... }

module main

open filesystem                  -- Import all from filesystem
open util/ordering[Time]         -- Parameterized utility module
open util/relation               -- Relation utilities

module internal

private sig Helper {}            -- Not visible when opened
sig Public {}                    -- Visible

module graph[Node]

sig Edge {
    src, dst: one Node
}

pred connected[n1, n2: Node] {
    n2 in n1.^(~src.dst)
}

open graph[Computer]             -- Instantiate with Computer

open util/ordering[State]        -- Total ordering on State
open util/relation               -- Relation predicates
open util/ternary                -- Ternary relation utilities
open util/boolean                -- Boolean operations
open util/integer                -- Integer operations
open util/sequence[Elem]         -- Sequences

sig Buffer {
    var contents: set Data,      -- Changes over time
    capacity: one Int            -- Static (no var)
}

pred addData[b: Buffer, d: Data] {
    d not in b.contents          -- Precondition
    b.contents' = b.contents + d -- Postcondition
}

-- Future-time operators
always P                         -- P holds in every future state
eventually P                     -- P holds in some future state
after P                          -- P holds in the next state
P until Q                        -- P holds until Q becomes true
P releases Q                     -- Q holds until P becomes true (or forever)

-- Past-time operators
historically P                   -- P held in all past states
once P                           -- P held at some past state
before P                         -- P held in the previous state
P since Q                        -- P has held since Q was true

-- Specification: initial state + transitions
fact Traces {
    init
    always trans
}

pred init {
    no Buffer.contents
}

pred trans {
    some b: Buffer, d: Data | addData[b, d]
    or stutter
}

pred stutter {
    contents' = contents
}

-- Liveness: something eventually happens
assert EventuallyFull {
    always (some b: Buffer | eventually #b.contents = b.capacity)
}

module mutex

abstract sig Process {
    var state: one State
}

abstract sig State {}
one sig Idle, Waiting, Critical extends State {}

one sig P1, P2 extends Process {}

pred init {
    all p: Process | p.state = Idle
}

pred requestAccess[p: Process] {
    p.state = Idle
    p.state' = Waiting
    all other: Process - p | other.state' = other.state
}

pred enterCritical[p: Process] {
    p.state = Waiting
    no other: Process - p | other.state = Critical
    p.state' = Critical
    all other: Process - p | other.state' = other.state
}

pred exitCritical[p: Process] {
    p.state = Critical
    p.state' = Idle
    all other: Process - p | other.state' = other.state
}

pred stutter {
    all p: Process | p.state' = p.state
}

pred trans {
    (some p: Process | requestAccess[p] or enterCritical[p] or exitCritical[p])
    or stutter
}

fact Traces {
    init
    always trans
}

-- Safety: mutual exclusion
assert MutualExclusion {
    always (lone p: Process | p.state = Critical)
}

-- Liveness: no starvation (if waiting, eventually critical)
-- Note: This will fail without fairness constraints - one process can
-- repeatedly enter/exit while another waits forever
assert NoStarvation {
    all p: Process | always (p.state = Waiting implies eventually p.state = Critical)
}

check MutualExclusion for 5 steps
check NoStarvation for 10 steps

univ                             -- All atoms
Person in univ                   -- Always true
univ - Person                    -- All non-Person atoms

none                             -- Empty set
no x implies x = none            -- Equivalence

iden                             -- Identity: x->x for all x
r & iden                         -- Self-loops in r
r - iden                         -- Remove self-loops

-- Arithmetic
plus[x, y]                       -- x + y
minus[x, y]                      -- x - y
mul[x, y]                        -- x * y
div[x, y]                        -- x / y
rem[x, y]                        -- x % y

-- Comparison
x < y, x > y, x <= y, x >= y

-- Aggregation
sum[s]                           -- Sum of integer set
max[s], min[s]                   -- Maximum/minimum

-- Integer set
Int                              -- All integers in scope

abstract sig State {}
one sig S1, S2, S3 extends State {}

sig Machine {
    var current: one State
}

pred transition[m: Machine, from, to: State] {
    m.current = from
    m.current' = to
}

sig Node {
    edges: set Node
}

fun reachable[n: Node]: set Node {
    n.*edges
}

pred connected {
    all n1, n2: Node | n2 in reachable[n1]
}

pred acyclic {
    no n: Node | n in n.^edges
}

sig Container {
    contains: set Item
}

sig Item {
    inside: lone Container
}

fact Consistency {
    all c: Container, i: Item |
        i in c.contains iff i.inside = c
}

fact SingleOwner {
    all i: Item | lone i.inside
}

sig Subject {}
sig Object {}
sig Permission {}

sig AccessMatrix {
    access: Subject -> Object -> Permission
}

pred canAccess[s: Subject, o: Object, p: Permission] {
    some am: AccessMatrix | p in am.access[s][o]
}

open util/ordering[Time]

sig Time {}

sig Event {
    when: one Time
}

pred before[e1, e2: Event] {
    lt[e1.when, e2.when]
}

fact EventOrder {
    all e1, e2: Event | e1 != e2 implies
        (before[e1, e2] or before[e2, e1])
}

module kvstore

sig Key {}
sig Value {}

sig Store {
    var data: Key -> lone Value
}

one sig TheStore extends Store {}

pred init {
    no TheStore.data
}

pred put[k: Key, v: Value] {
    TheStore.data' = TheStore.data ++ (k -> v)
}

pred get[k: Key, v: Value] {
    v = TheStore.data[k]
    TheStore.data' = TheStore.data  -- Frame condition
}

pred delete[k: Key] {
    TheStore.data' = TheStore.data - (k -> Value)
}

pred trans {
    (some k: Key, v: Value | put[k, v])
    or (some k: Key | delete[k])
    or (TheStore.data' = TheStore.data)  -- Stutter
}

fact Traces {
    init
    always trans
}

-- Each key maps to at most one value
assert Functional {
    always all k: Key | lone TheStore.data[k]
}

-- If we put k->v and don't delete or overwrite, it stays
assert PutPersists {
    all k: Key, v: Value |
        always (put[k, v] and after always (not delete[k] and not (some v': Value - v | put[k, v'])))
            implies after always TheStore.data[k] = v
}

-- Delete removes the key
assert DeleteRemoves {
    all k: Key |
        always (delete[k] implies after no TheStore.data[k])
}

check Functional for 3 but 5 steps
check PutPersists for 3 but 8 steps
check DeleteRemoves for 3 but 5 steps

run { eventually some TheStore.data } for 3 but 5 steps