Index

A

Alloy, [1] Alloy Analyzer enumeration, [1], [2] evaluator, [1] options, [1], [2], [3], [4] visualizer, [1], [2], [3]

assert, [1], [2] atoms

B

Boolean operator see logical operator

C

command check, [1], [2], [3], [4] run, [1], [2], [3], [4], [5] constant iden none, [1] univ

converse see transpose

D

distributed protocol leader election

dot join see composition

E

enum keyword see enumeration signature event, [1], [2] effect, [1] enabled frame condition, [1] guard, [1] visualization

extends keyword see sub-signature

F

fact fairness strong weak fields field declaration, [1] mutable fields first-order logic

first-order operator some for keyword see seting scopes fun keyword see function, Alloy function, Alloy, [1], [2], [3] function, logic

I

in keyword, signature see subset signature initial state, [1] instance, [1], [2] exploration, [1], [2] snapshot

Int signature invariant

L

liveness logical operator conjunction, [1] disjunction, [1] else, [1] equivalence, [1] implication, [1] negation, [1]

M

model checking bounded model checking, [1] complete model checking, [1] model, Alloy see specification model, logic see instance module ordering parameterised predefined

multiplicity constraint, [1] lone keyword, [1] multiplicity arrow no keyword one keyword, [1], [2] set keyword some keyword, [1]

P

path see trace pred keyword see predicate, Alloy

predicate, [1] predicate, Alloy predicate, logic, [1] proposition propositional logic

Q

quantifier disj, [1], [2], [3] existential, [1], [2] higher-order, [1] universal, [1]

R

relation abstraction arity, [1] bijection binary, [1] entire function injection injective representation simple surjection surjective ternary, [1], [2]

relation comprehension, [1], [2], [3] relational logic, [1] relational operator box join Cartesian product, [1] composition, [1] difference, [1] domain restriction, [1] intersection, [1] override range restriction, [1] reflexive transitive closure, [1] transitive closure, [1] transpose union, [1]

S

safety scenario, [1] scopes, [1] exact scopes setting scopes, [1] steps, [1] sig keyword see signature declaration signature abstract enumeration signature, [1], [2] multiplicity mutable signature parent signature signature declaration, [1] sub-signature, [1] subset signature, [1], [2] top-level signature

Skolemization, [1] solver, [1], [2] specification String signature stuttering, [1] symmetry breaking, [1]

T

temporal operator after, [1] always, [1], [2] eventually, [1] historically, [1] once prime sequence, [1] themes customisation, [1], [2], [3], [4], [5] magic layout

total order trace, [1], [2] transition system type system arity error type-system irrelevance error

U

unbounded model checking see complete model checking

V

var keyword mutable fields mutable signature

variable signature see mutable signature