CSSE 373 Formal Methods in Specification and Design

HW3

Purpose: practice writing expression using the Alloy logic

This is a team homework assignment. All work must be done by the team members together. All team members should understand all work submitted. If you have concerns about your own understanding or that of your teammates, please let me know. I want everyone to learn all they can in this course!

Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.
Do exercise A.1.4 in Appendix A of the text. Some extra guidance:
- In Alloy 4, type scopes don’t limit the number of Int instances. To be able to create smaller counterexamples, use the following template model rather than that provided in the text:
```
// Problem A.1.4
module homework/hw3_1

sig Thing {}

assert union {
  all s: set Thing, p, q: Thing->Thing |
    s.(p+q) = s.p + s.q
}
check union for 4
```
- For parts (a)–(c), if the identity doesn’t hold, give your counterexample by giving the three relations s, p, and q. (You can read these from the picture in the visualizer if you reduce the scope enough.)
- Copy and paste your final Alloy model into your answers document.
Do problem A.1.5 in Appendix A of the text. Again, some extra guidance:
- Use the following template model rather than that provided in the text:
```
// Problem A.1.5
module homework/hw3_2

sig Node {}

pred isTree[r: Node -> Node] {
  ...
}

run isTree for 4
```
- To write your constraints, consider what properties you need to express. How many root nodes does a tree have? Which nodes can you reach starting with the root? How many parents do non-root nodes have? I found it helpful to write these properties down as comments in my Alloy model before trying to write them as Alloy constraints.
- Copy and paste your final Alloy model into your answers document.
Do problem A.1.10. Clearly label (using a comment) each invariant and simulation constraint that you add.
- To save you some typing, here’s the template model from the text:
```
// Problem A.1.10
module homework/hw3_3

abstract sig Name {
  address: set Addr + Name
}

sig Alias, Group extends Name {}
sig Addr {}

// invariants
fact {
  // Put your answers to a and b here, plus the 
  // additional invariant noted below.
}

// simulation constraints
pred show[] {
  // Put your answers to c and d here.
  
  // You may want to add additional constraints to make 
  // the generated instances more interesting.
}

run show for 3 but 6 Name
```
- Read constraint (b) as “All names (in the domain of the address relation) eventually map to an address.”
- Add an additional invariant, “Aliases must directly map to at most one address or name.”
- For parts (e)–(g) copy and paste the Alloy expressions from the Alloy evaluator into your answers document.
- You do not have to do part (h).
- Also, copy and paste your final Alloy model into your answers document.
Be sure to document your models and include your names in the comments.
How much time did you spend on this assignment?
Turn in your work by committing a pdf file containing your answers to the appropriate HW folder in your homework team subversion repository for this course.