Syntax Quick Reference

Top-level declarations

type Name = { A, B, C };

transition name(p : Type) { guard: e ; modifies: x ; effect: x := e ; }

agent Name(p : Type) {
    attributes { a : T = v ; }
    behavior { P0 = a . P1 + b . done ; }
}

schema Env {
    attributes { x : Int = 0 ; }
    invariants { x >= 0 ; }
}

system S {
    schema: Env ;
    agents { Agent(i) * 3 ; }
    init { x == 0 ; }
    sync { ... ; }
    properties { safety : x >= 0 ; }
}

property invariant Name { ... }
property reachable Name { ... }
property unreachable Name { ... }

pattern Name {
    signature { a(p) . b(q) . done }
    constraints { p > q }
    severity: CRITICAL ;
}

rules RuleSet(x) { x + 0 => x ; }
canonizer Norm for Int { apply(rules: RuleSet, strategy: bottomUp) ; }

Behavior operators

Effect forms

x := e
x += e   x -= e
arr[i] := e
node.f := e
Agent(i).f := e
skip
if (c) then { ... } else { ... }
for (j : Int) in [0..n) { ... }
havoc(x) [ with { c } ]
let name = e