CS 580 Alloy TutorialSession 2: Language and AnalysisGreg Dennis and Rob SeaterSoftware Design Group, MITUsed and modified with permissionby Robert Stehwienalloy language & analysis●language = syntax for structuring specifications in logic–shorthands, puns, sugar●analysis = tool for finding solutions to logical formulas–searches for and visualizes counterexamples“I'm My Own Grandpa” Song●popular radio skit originally written in the 1930's●expanded into hit song by “Lonzo and Oscar” in 1948module examples/tutorial/grandpaabstract sig Person { father: lone Man, mother: lone Woman}sig Man extends Person { wife: lone Woman}sig Woman extends Person { husband: lone Man}fact { no p: Person | p in p.^(mother + father) wife = ~husband}assert noSelfFather { no m: Man | m = m.father}check noSelfFatherfun grandpas(p: Person) : set Person { p.(mother + father).father}pred ownGrandpa(p: Person) { p in grandpas(p)}run ownGrandpa for 4 Person“I'm My Own Grandpa” in Alloylanguage: module headermodule examples/tutorial/grandpa●first non-comment of an Alloy model●saved as examples/tutorial/grandpa.als–relative to Alloy Analyzer's models directorylanguage: signaturessig A {}set of atoms Asig A {}sig B {}disjoint sets A and B (no A & B)sig A, B {}same as abovesig B extends A {}set B is a subset of A (B in A)sig B extends A {}sig C extends A {}B and C are disjoint subsets of A (B in A && C in A && no B & C)sig B, C extends A {}same as aboveabstract sig A {}sig B extends A {}sig C extends A {}A partitioned by disjoint subsets B and C (no B & C && A = (B + C))sig B in A {}B is a subset of A – not necessarily disjoint from any other setsig C in A + B {}C is a subset of the union of A and Bone sig A {}lone sig B {}some sig C {}A is a singleton setB is a singleton or emptyC is a non-empty setgrandpa: signatures●all men and women are persons●no person is both a man and a woman●all persons are either men or womenabstract sig Person { . . .}sig Man extends Person { . . .}sig Woman extends Person { . . .}language: fieldssig A {f: e}f is a binary relation with domain A and range given by expression e f is constrained to be a function (f: A -> one e) or (all a: A | a.f: e)sig A { f1: one e1, f2: lone e2, f3: some e3, f4: set e4}(all a: A | a.fn : m e)sig A {f, g: e}two fields with same constraintssig A {f: e1 m -> n e2}(f: A -> (e1 m -> n e2)) or (all a: A | a.f : e1 m -> n e2)sig Book { names: set Name, addrs: names -> Addr}dependent fields(all b: Book | b.addrs: b.names -> Addr)grandpa: fields●fathers are men and everyone has at most one●mothers are women and everyone has at most one●wives are women and every man has at most one●husbands are men and every woman has at most oneabstract sig Person { father: lone Man, mother: lone Woman}sig Man extends Person { wife: lone Woman}sig Woman extends Person { husband: lone Man}language: factsfact { F }fact f { F }sig S { ... }{ F }sig Host {}sig Link {from, to: Host}fact {all x: Link | x.from != x.to}no links from a host to itselffact noSelfLinks {all x: Link | x.from != x.to}same as abovesig Link {from, to: Host}{from != to}same as above, with implicit 'this.'facts introduce constraints that are assumed to always holdgrandpa: fact●no person is his or her own ancestor●a man's wife has that man as a husband●a woman's husband has that woman as a wifefact { no p: Person | p in p.^(mother + father) wife = ~husband}language: functionsfun f(x1: e1, ..., xn: en) : e { E }sig Name, Addr {}sig Book { addr: Name -> Addr}fun lookup(b: Book, n: Name) : set Addr { b.addr[n]}fact everyNameMapped { all b: Book, n: Name | some lookup(b, n)}functions are named expression with declaration parameters and a declaration expression as a resultinvoked by providing an expression for each parameterlanguage: predicatespred p(x1: e1, ..., xn: en) { F }sig Name, Addr {}sig Book { addr: Name -> Addr}pred contains(b: Book, n: Name, d: Addr) { n->d in b.addr}fact everyNameMapped { all b: Book, n: Name | some d: Addr | contains(b, n, a)}named formula with declaration parametersgrandpa: function and predicate●a person's grandpas are the fathers of one's own mother and fatherfun grandpas(p: Person) : set Person { p.(mother + father).father}pred ownGrandpa(p: Person) { p in grandpas(p)}language: “receiver” syntaxfun f(x: X, y: Y, ...) : Z {...x...}fun X::f(y:Y, ...) : Z {...this...}pred p(x: X, y: Y, ...) {...x...}pred X::p(y:Y, ...) {...this...}f(x, y, ...)x::f(y, ...)p(x, y, ...)x::p(y, ...)fun Person::grandpas() : set Person { this.(mother + father).father}pred Person::ownGrandpa() { this in p::grandpas()}language: assertionsassert a { F }sig Node { children: set Node}one sig Root extends Node {}fact { Node in Root.*children}// invalid assertion:assert someParent { all n: Node | some children.n}// valid assertion:assert someParent { all n: Node – Root | some children.n}constraint intended to followfrom facts of the modellanguage: check commandcheck atop-level sigs bound by 3check a for defaulttop-level sigs bound by default check a for default but listdefault overridden by bounds in listcheck a for listsigs bound in list, invalid if any unboundassert a { F }check a scopeinstructs analyzer to search for counterexample to assertion within scopeabstract sig Person {}sig Man extends Person {}sig Woman extends Person {}sig Grandpa extends Man {}check acheck a for 4check a for 4 but 3 Womancheck a for 4 but 3 Man, 5 Womancheck a for 4 Personcheck a for 4 Person, 3 Womancheck a for 3 Man, 4 Womancheck a for 3 Man, 4 Woman, 2 Grandpa// invalid:check a for 3 Mancheck a for 5 Woman, 2 Grandpaif model has facts M finds solution to M && !Fgrandpa: assertion check●sanity check●command instructs analyzer to search for counterexample to noSelfFather within a scope of at most 3 Persons●noSelfFather assertion follows from factfact { no p: Person | p in p.^(mother + father) wife = ~husband}assert noSelfFather { no m: Man | m = m.father}check noSelfFatherlanguage: run commandpred p(x: X, y: Y, ...) { F }run p scopeinstructs analyzer to search for instance of predicate within scopeif model has facts M, finds solution to M && (some x: X, y: Y, ... | F)fun f(x: X, y: Y, ...) : R { E }run f scopeinstructs analyzer to search for instance of function within scopeif model has facts M, finds solution to M && (some x: X, y: Y, ..., result: R | result = E)grandpa: predicate simulation●command