analyzing relational logic Daniel Jackson, MIT WG 2.3 · Newcastle April 2000

language assumptions
language
• first-order logic
• set & relation operators
• uninterpreted types

analysis desired
simulation
find a state that satisfies invariant J

• find an execution of operation O
resulting in a state satisfying P
from a state satisfying P
that changes the component x
that is not an execution of operation Ov
checking
• does invariant J imply invariant Jv?
• does operation O preserve invariant J ?
• does operation Oc refine Oa under abstraction A?

analyses not possible
refinement
• does Oc refines Oa for some abstraction?
• are all executions of O also executions of O1;O2?
spec by minimization
• make smallest change to connections that satisfies C
precondition checks
• does O have an execution from every state satisfying C?
temporal checks
• do reachable states satisfy J ?

semantics: formulas
M : formula ? env ? boolean
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
M [a in b] e = X[a]e ? X[b]e
M [! F] e = ? M[F]e
M [F && G] e = M[F]e ? M[G]e
M [all v: t | F] e = ? {M[F] (e ? v ? x) | x ? e(t)}

semantics: expressions
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
X [a + b] e = X[a]e ? X[b]e
X [a . b] e = {y | ?x. x ? X[a]e ? (x,y) ? X[b]e}
X [~a] e = {(x,y) | (y,x) ? X[a]e}
X [+a] e = the smallest r such that r ; r ? x ? X[a]e ? x
X [{v: t | F}] e = {x ? e(t) | M[F] (e ? v ? x)}
X [v] e = e(v)
X [a[v]] e = e(a)(v)

models
models are well-formed environments for which formula holds
M : formula ? env ? boolean

Models (F) = {e | M[f]e}
environment e is well formed iff
• tight: only bind variables declared along with formula
• type correct: if expression a has type T, X[a]e ? X[T]e
e is within scope k iff
• for all basic types T, #X[T]e = k
• write Modelsk (F) for models within scope k

small scope hypothesis

% bugs caught

scope

90

4

most bugs can be caught by considering only small instances

example
problem
a, b : S

p : S -> T
! (a  b).p in (a.p  b.p)
a model in a scope of 2
S = {S0, S1}

T = {T0, T1}
p = {(S0, T0), (S1, T0)}
a = {S0}
b = {S1}

S0

S1

T0

T1

a

b

what Alcoa does
alcoa : formula, scope ? env
• does not always succeed (ie, may return nothing)
properties
• termination: always, with deterministic solvers
• soundness: alcoa (F, k) ? Modelsk (F)
• relative completeness: Modelsk (F) ? {} ? alcoa (F, k) succeeds
non-properties
• minimality: alcoa (F, k) not the smallest model of F in k
• completeness: Models (F) ? {} ? alcoa (F, k) succeeds
so counterexamples are real, but cant prove theorems

scope monotonicity
Alcoa is scope monotonic
• alcoa (F, k) succeeds ? alcoa (F, k+1) succeeds
• if scope of 7 fails, no need to try 6, 5,
because models are scope monotonic
• Modelsk (F) ? Modelsk+1 (F)
• property of Alloy, not kernel

every analysis is model finding
does operation O preserve invariant J ?
alcoa (O && J && !J , 3)
show me how O1 and O2 differ
alcoa ((O1 && !O2) || (O2 && !O1) , 3)
show me an execution of O that changes x
alcoa (O && !x = x , 3)

alcoa architecture
TRANSLATE PROBLEM

TRANSLATE SOLUTION

MAPPING

BOOLEAN FORMULA

BOOLEAN ASSIGNMENT

SAT
SOLVER

DESIGN
PROBLEM

DESIGN
ANALYSIS

alcoa

overview of method
from alloy formula F and scope k generate
boolean formula BF

mapping ? : BoolAssignment ? Environment
such that
? maps every solution of BF

?n ? Modelsk (F) ? n ? Models (BF)

SAT solvers
in theory
• 3-SAT is NP-complete
in practice
• solvers work well for 򒮨 variables and ,000 clauses
• usually give small models
kinds of solver
• local search (eg, WalkSAT)
• Davis-Putnam (eg, RelSAT, SATO)
• non-clausal (eg, Prover)

example
problem
a, b : S

p : S -> T
! (a  b).p in (a.p  b.p)
translation in scope of 2
• formula becomes
• ((a0??b0 ? p00) ? (a1??b1 ? p10) ? ((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10))) ?
• a model is
a0 , ?a1 , ?b0 , b1 , p00 , ?p01 , p10 , ?p11

mapping function ?
• set to vector of bool var
a [a0 a1]

b [b0 b1]
• relation to matrix
p [p00 p01 , p10 p11]
final result
S = {S0, S1}

T = {T0, T1}
p = {(S0, T0), (S1, T0)}
a = {S0}
b = {S1}

compositional translation
translating relation r: S -> T
XT [r]ij boolean var, true when r contains (Si, Tj)
translating expression e: T
XT [a]i boolean formula, true when a contains Ti
translating formulas
MT [F] boolean formula, true for models of F
sample rules
MT [F && G] = MT[F] ? MT[F]

XT [a - b]i = XT [a]i ? ?XT [b]i
XT [a . b]i = ?j. XT [a]j ? XT [b]ji

example
a [a0 a1]
b [b0 b1]
p [p00 p01 , p10 p11]
a  b [a0??b0 a1??b1]
(a  b).p [(a0??b0 ? p00) ? (a1??b1 ? p10) ]
a.p [(a0 ? p00) ? (a1 ? p10) (a0 ? p01) ? (a1 ? p11)]
b.p [(b0 ? p00) ? (b1 ? p10) (b0 ? p01) ? (b1 ? p11)]
a.p  b.p [((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10)) ]

! (a  b).p in (a.p  b.p) ? (((a0??b0 ? p00) ? (a1??b1 ? p10) ? ((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10)))) ?

quantifiers
example
!((all x | x in x.p) -> (all x | x in x.p.p))
put in negation normal form
(all x | x in x.p) && (some x | ! x in x.p.p)
skolemize
(all x | x in x.p) && ! (xc in xc.p.p)
how to translate remaining universal quantifiers?

environments & trees
semantics
M : formula ? env ? boolean

X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
translation
MT : formula ? boolFormula tree

XT : expr ? boolValue tree
? tree = (var ? (index ? ? tree) + ?
boolValue = booleanFormulaMatrix + (index ? boolValue)
env becomes (tree, boolean encoding of relations)

examples

compositional rules
MT [a in b] = merge (MT[a], MT[b], ?u,v. ?i (ui ? vj) ) MT [all x | F] = fold (MT[F], ?)
merging
• subexpressions may have different variables
• so interpose layers as necessary, then merge
• maintain consistent ordering from root to leaf

x

0

1

y

0

1

y

0

1

0

1

1

x

y

x in y

symmetry
observation
• types are uninterpreted
• permuting elements of a type preserves modelhood
example
a = {S0} , b = {S1}, p = {(S0, T0), (S1, T0)}

a = {S1} , b = {S0}, p = {(S0, T0), (S1, T0)}
both models of !(a  b).p in (a.p  b.p)
exploitation
• environments form equivalence classes
• avoid considering all elements of a class

?

?

environments

symmetry in boolean formula
preserved!
• express symmetry ? as permutation on boolean vars
• then ? is a symmetry of the boolean formula too
• want to rule out one of A, ?A
Crawfords idea
• order boolean vars into sequence V
• view assignments as binary numbers & pick smaller
• for each ?, add constraint V ? ?V
example
• A = 0123, ?A = 0123, ? = (02)
• V ? ?V is 0123 < 2103 = 0 < 2

symmetry constraint for a relation
suppose we translated relation p: S -> T to the matrix
0 1 2

3 4 5
6 7 8
symmetry (S0 S1) exchanges top two rows
3 4 5

0 1 2
6 7 8
constraint obtained is
0 1 2 3 4 5 6 7 8 < 3 4 5 0 1 2 6 7 8

= 0 1 2 < 3 4 5
= ?0?3 ? (0?3 ? ?1?4) ? (0?3 ? 1?4 ? ?2?5)

generalizing symmetry
extend to
• multiple relations and sets
• multiple types
but
• diminishing returns
• pick ordering of vars carefully
• homogeneous relations tricky

results
observations
• solver time dominates
• RelSAT dominates other solvers
• symmetry gives 100x speedup for proofs
• bugs in boolean code not translation
so end-to-end check
where are we?
• interactive analysis up to 200 bits
• small but real specs (longest so far is 400 lines)
• 30loc list-processing procedures

challenges
symmetry
• why do a few symmetries seem to work so well?
• what symmetries should be used?
progress bar
• will symmetry spoil our heuristics?
visualization of models
• key for novice use
language extensions
• numbers (easy?)
• sequences (hard?)

PPT Slide
allex

PPT Slide
allox

PPT Slide
allix