// Lecture: Alloy Logic (part d)
// For You To Do #1 - Quantifiers
// John Hatcliff
// Feb 27, 2008
sig Name, Addr {}
sig Book {
addr: Name -> Addr
}
// The bi-implication below was conjectured to hold in the FYTD description
// ((all n: Name | some a : Addr | b.addr[n] = a) // constraint 1
// <=>
// (some a: Addr | all n : Name | b.addr[n] = a))
// The conjectured bi-implication below does not hold.
//
// Consider b.addr = n0->a0 + n1->a1 + n2->a1 for a scope of 3 but 1 book.
// Then constraint 1 holds because every name maps to some address.
// Constraint 2 does not hold because we cannot find an address a such that every
// name maps to a and only a.
//
// Alloy finds an instance to the following predicate (stating the negation of
// the bi-implication) which confirms our argument above.
pred DoNotReorderAllSome(b: Book, disj n0, n1, n2 : Name, disj a0, a1, a2: Addr) {
// construct a scenario
b.addr = n0->a0 + n1->a1 + n2->a1
not ((all n: Name | some a : Addr | b.addr[n] = a) // constraint 1
<=>
(some a: Addr | all n : Name | b.addr[n] = a)) // constraint 2
}
run DoNotReorderAllSome for 3 but 1 Book
// The following code will cause Alloy to generate a counterexample (not necessarily
// the one above illustrating the inequivalence of the two constraints.
assert conjecturedEquivalence {
(all b : Book |
(all n: Name | some a : Addr | b.addr[n] = a) // constraint 1
<=>
(some a: Addr | all n : Name | b.addr[n] = a)) // constraint 2
}
check conjecturedEquivalence for 3 but 1 Book
// Does the second constraint imply the first for an arbitrary expression ?
// The following code will test this implication for the property P stated above.
assert conjecturedImplication {
(all b : Book |
(some a: Addr | all n : Name | b.addr[n] = a)
=>
(all n: Name | some a : Addr | b.addr[n] = a))
}
// We can keep bumping up the scope in the hope of finding a counterexample
check conjecturedImplication for 3 but 1 Book
check conjecturedImplication for 6 but 1 Book
check conjecturedImplication for 9 but 1 Book
// We cannot find a counterexample, but this DOES NOT prove that implication
// holds for all properties P. First, we have only established the implication for
// the particular property b.addr[n] = a. Second we have only confirmed that
// the implication holds on signature sets up to size 9, we cannot conclude
// that it holds for sets of any size. Alloy cannot be used to prove the
// suggested implication.
// The rest of the answers for this FYTD exercise are omitted.