Your solutions for this assignment should terminate within 10 seconds.

Problem 1: Address Book

In this exercise, you'll get some practice writing expressions and constraints for a simple multi-level address book, similar to the one seen in Chapter 2 of the Jackson book. By "multi-level" we mean that entries can reference groups and aliases rather than just addresses directly.

Consider a set Addr of addresses, and a set Name consisting of two disjoint subsets Alias and Group. The mapping from Names to addresses is represented by a relation address. A Name can map directly to an Addr or to another Name. Aliases map to at most one target, but Groups can map to a set of targets.

First of all, make the above definitions precise by writing a predicate basicDefinitions.

There are some constraints that you'd expect any address book to satisfy. Write the following:

• (a) There are no naming cycles; a Name can never contain a reference to itself, not even indirectly.
• (b) All names eventually denote at least one address.

Then we make these two along with basicDefinitions a fact (the template has already done this for you).

Sometimes you might want to explore to see more interesting instances. Add the following simulation constraints to do so:

• (c) The address book has at least two levels (for example, an instance with a Name pointing to another Name which then points to an Addr is considered two levels)
• (d) Some groups are non-empty.

Finally, write expressions for each of the following, without using comprehension/predicate calculus (recall that comprehensions are expressions like {x : A | ...}). Note that these do not all necessarily need to produce an instance, they are just for you to check specific conditions of your model:

• (e) the set of names that are members of groups (all of the Names that a Group transitively points to are considered members of that Group);
• (f) the set of groups that are empty;
• (g) the mapping from aliases to the addresses they refer to, directly or indirectly;
• (h) the mapping from names to only the addresses to which they directly refer.

Following is a template file that you must follow:

abstract sig Name {
	address: set Addr + Name
}
sig Alias, Group extends Name {}
sig Addr {}

// DO NOT MODIFY THE ABOVE

pred basicDefinitions { ... }

// (a)
pred noCycle { ... }

// (b)
pred reachAddresses { ... }

fact {
	basicDefinitions
	noCycle
	reachAddresses
}

// (c)
pred twoOrMore { ... }
run twoOrMore

// (d)
pred groupNonEmpty { ... }
run groupNonEmpty

// (e)
fun groupMembers: Name { ... }
run groupMembers

// (f)
fun emptyGroups: Group { ... }
run emptyGroups

// (g)
fun mappingAlias: (Alias -> Addr) { ... }
run mappingAlias

// (h)
fun mappingName: (Name -> Addr) { ... }
run mappingName

As you fill them in, execute the run command; the tool will generate sample instances. Then, when you have an interesting instance, enter a candidate expression into the evaluator, and the tool will show you its value for that particular instance. You may find that you need to add more simulation constraints to obtain an instance that nicely illustrates the meaning of an expression.

Problem 2: Handshakes

There are five people at a party. There was some handshaking, though not every pair of people shook hands (of course nobody shook their own hand, and a pair of people shook hands no more than once). At the end of the party, everyone said they had shaken a different number of hands than everyone else.

• (a) Is this possible? Model the problem in Alloy such that your model either finds an instance or shows that no instance exists.
• (b) Now suppose that exactly one person at the party lied about how many hands they had shaken. How many hands did this person shake? Solve this problem by adjusting your model and using the analyzer to find a solution.
• (c) Is there another solution, in which the liar shook a different number of hands than the answer you found in part (b)? Check whether this is possible with an assert in Alloy.

Problem 3: State Machines

A state machine is a directed graph that models how a system moves from state to state as it executes. It has one or more initial (or starting) states, and edges connecting each state to its successor(s). Construct an Alloy model of a state machine, then write predicates that constrain Alloy to produce instances of the following types of machine:

• (a) a deterministic machine, in which there is one starting state and each state has at most one successor
• (b) a nondeterministic machine, in which there are multiple starting states, or where some states have more than one successor, or both
• (c) a machine with unreachable states
• (d) a machine without unreachable states
• (e) a connected machine in which every state is reachable from every other state
• (f) a machine with a deadlock: a reachable state that has no successors
• (g) a machine with a livelock: the possibility of an infinite execution in which a state that is always reachable is never reached.

While you are free to design sigs or have additional facts, funs, etc. however you like, you should have the following at minimum.

// (a)
pred deterministic { ... }
run deterministic

// (b)
pred nondeterministic { ... }
run nondeterministic

// (c)
pred unreachable { ... }
run unreachable

// (d)
pred reachable { ... }
run reachable

// (e)
pred connected { ... }
run connected

// (f)
pred deadlock { ... }
run deadlock

// (g)
pred livelock { ... }
run livelock

Handing In

For this assignment, you should have 3 Alloy files (address_book.als, handshakes.als, state_machine.als). To hand in your homework run cs1950y_handin alloy3 from a directory containing an Alloy file for each of the problems.

Credit

Exercises borrowed or adapted from Appendix A of Daniel Jackson's Software Abstractions.