analyzing relational logicDaniel Jackson, MITWG 2.3 · NewcastleApril 2000

language assumptions

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

analysis desired

simulation
find a state that satisfies invariant J

… and additionally condition C
• 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

% bugscaught

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

TRANSLATEPROBLEM

TRANSLATESOLUTION

MAPPING

BOOLEANFORMULA

BOOLEANASSIGNMENT

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