Index

Symbols

! (not), [1] != (inequality) !in (not in) # (cardinality) & (intersection), [1] && (and), [1] ' (prime), [1] * (reflexive transitive closure) + (union), [1] ++ (override) - (difference), [1] -> (Cartesian product), [1] . (dot-join), [1] :> (range restriction) ; (sequence) < (less than)

<: (domain restriction) << (left shift) <= (less than or equal) <=> (iff), [1] = (equality), [1] =< (less than or equal) => (implies), [1] > (greater than) >= (greater than or equal) >> (right shift w/ zero extension) >>> (right shift w/ sign extension) [] (box-join) ^ (transitive closure), [1], [2] || (or), [1] ~ (converse), [1] ← button, [1] → button, [1], [2]

A

abstract keyword action see event after keyword, [1] all keyword, [1] Allow warnings menu option Alloy extensions versions Alloy Analyzer

Alloy* Alloy4Fun AlloyMax always keyword, [1], [2] and keyword, [1] Apply button as keyword assert keyword, [1] assertion definition atom, [1]

B

before keyword, [1]

box-join operator but keyword, [1]

C

cardinality operator Cartesian product operator, [1] check keyword, [1], [2] Close button Close Evaluator button, [1] command, [1] definition, [1] execution

composition operator see dot-join operator comprehension, [1], [2] computation tree logic configuration, [1], [2] converse operator, [1] CTL see computation tree logic

D

deadlock difference operator, [1] disj keyword, [1], [2]

domain restriction operator dot-join operator, [1] DynAlloy

E

Edge Color Palette option Electrum else keyword, [1] enum keyword equality operator, [1] in signature declaration Evaluator button, [1], [2] event, [1], [2] effect, [1], [2] enabled, [1] frame condition, [1], [2], [3], [4] guard, [1], [2] specification with predicate stuttering visualization

eventually keyword, [1] exactly keyword, [1] Execute All menu option Execute button Execute menu expect keyword, [1] Export To menu option extends keyword

F

fact definition fact keyword fairness, [1], [2], [3] strong, [1] unconditional weak, [1] field, [1] declaration, [1], [2] meta mutable, [1] file sharing app example file system example first-order logic

for keyword, [1] fun keyword fun/add keyword fun/div keyword fun/max keyword fun/min keyword fun/mul keyword fun/next keyword fun/rem keyword fun/sub keyword function Alloy vs logic nomenclature definition recursive

G

generator axiom

greater than operator greater than or equal operator

H

Hide skolem sigs/relations option

Hide unconnected nodes option historically keyword, [1], [2]

I

iden keyword, [1], [2] iff keyword, [1] implies keyword, [1] in keyword as subset or equal operator, [1] in signature declaration, [1], [2] inequality operator instance, [1] evaluator exploration, [1], [2], [3] visualization, [1], [2], [3], [4], [5], [6] vs trace

int keyword Int signature, [1] intersection operator, [1] invariant, [1] inductive

K

Kodkod

L

leader election protocol example left shift operator less than operator less than or equal operator let keyword in macro definition linear temporal logic

linear temporal logic with past liveness, [1], [2] Load theme menu option lone keyword as multiplicity, [1], [2], [3] as quantifier LTL see linear temporal logic

M

macro definition vs predicate Magic Layout button meta-model evaluation visualization model Alloy vs logic nomenclature see instance model checking bounded, [1] complete, [1], [2]

model finding module definition import parametric predefined module keyword multiple inheritance multiplicity arrow operator

N

New button in visualizer, [1], [2] New Config button New Fork button, [1] New Init button New Trace button no keyword as multiplicity, [1] as quantifier

Node Color Palette option none keyword not in keyword, [1] not keyword, [1] NuSMV nuXmv

O

once keyword, [1] one keyword as multiplicity, [1], [2], [3], [4], [5] as quantifier open keyword Open Sample Models... menu option operators arithmetic Boolean, [1] relational, [1], [2], [3] temporal, [1], [2], [3]

Options menu, [1], [2], [3], [4] or keyword, [1] overloading override operator

P

PLTL see linear temporal logic with past pred keyword predicate Alloy vs logic nomenclature definition

Prevent overflows menu option prime operator, [1] private keyword Projection menu propositional logic

Q

QAlloy quantifier higher-order, [1] over mutable set

R

range restriction operator Record the Kodkod input/output menu option recursion Recursion depth menu option reflexive transitive closure operator relation abstraction arity, [1], [2] bijection binary, [1], [2] composition entire function higher-arity identity injective, [1] predefined representation simple surjective ternary, [1] unary

relational linear temporal logic relational logic, [1] navigational style pointfree style, [1], [2] pointwise style, [1], [2] releases keyword, [1] Reset theme menu option right shift w/ sign extension operator right shift w/ zero extension operator RLTL see relational linear temporal logic run keyword, [1]

S

safety, [1], [2] SAT solving, [1] Save theme menu option scope, [1] default definition, [1], [2], [3], [4] for Int signature for seq seq keyword sequence declaration sequence operator set keyword Show as arcs option Show as attribute option Show as labels option, [1] Show button Show Latest Instance menu option Show Metamodel menu option Show New Configuration menu option Show New Fork menu option Show New Initial State menu option Show New Solution menu option Show New Trace menu option Show Next State menu option Show option Show Previous State menu option sig keyword

signature abstract declaration, [1], [2], [3] enumeration extension, [1], [2], [3] fact meta multiplicity mutable, [1], [2] parent, [1] predefined singleton subset, [1], [2], [3], [4] top-level, [1], [2] since keyword Skolem depth menu option Skolemization, [1], [2] Solver menu option, [1], [2] some keyword as multiplicity, [1], [2], [3] as quantifier, [1] steps keyword, [1], [2] String signature stuttering, [1], [2], [3] sum keyword as operator as quantifier symmetry breaking, [1], [2]

T

Table button temporal logic, [1], [2] expressiveness semantics temporal logic of actions theme Theme button TLA see temporal logic of actions trace, [1], [2] evaluator, [1] exploration scenario visualization, [1], [2] vs instance

transition system initial state, [1], [2] specification with temporal formula transitions transitive closure operator, [1], [2] transpose operator see converse operator Tree button triggered keyword Txt button type-system ambiguity error arity error bounding type irrelevance warning relevance type

U

union operator, [1] univ keyword, [1] until keyword util/graph module util/integer module

util/natural module util/ordering module, [1] util/relation module util/sequniv module util/ternary module

V

var keyword, [1], [2]

Verbosity menu option Viz button