These exercises are optional and will not be corrected.

Exercise 1: Using the Alloy Analyzer to check an Alloy specification

Consider the Alloy specification for the address book given in the slides.

• Check the assertion noParentReflexivity; what’s the output? Is the assertion valid?
• Run the predicate personWithoutParents; what does the output mean? Is the predicate consistent with the specification? Which is the person without parents?
• Run the function personParents: the Analyzer will find an instance. What does this mean? Inspect the instance. What can you say about the specification now?

Exercise 2: Refining the Alloy specification with new facts

Add the following facts to the specification:

1. Marriage is symmetric (x is married with y iff y is married with x)
2. Marriage is irreflexive (noone is married with him/herself)
3. A person is not one of his/her ancestors
4. A person’s siblings are all and only the offsprings of at least one of her parents
5. Incest, in the form of marriage between siblings or ancestors, is prohibited

fact f1 {
  all p: Person | _______________________________________________
  _______________________________________________________________
}


fact f2 {
  _______________________________________________________________
  _______________________________________________________________
}


fact f3 {
  _______________________________________________________________
  _______________________________________________________________
}


fun siblings[p : Person]: set Person {
  _______________________________________________________________
  _______________________________________________________________
}


fact f5 {
  no p: Person | ________________________________________________
  _______________________________________________________________
}

Exercise 3: Check the consistency of the specification

Now that the specification contains many facts we may ask whether it is consistent. How do we check consistency? Write an assertion to check consistency and the check command to check it. 

_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________

Check the consistency in the Alloy Analyzer. What result do you obtain? Comment its meaning. Now try to generate a number of unconstrained instances of the specification. Write a predicate and a run command that allows you to generate the instances.

_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________
_______________________________________________________________

Run it and inspect the instances. Have them the shape you expected? Is their number the right number? 

Exercise 4: More predicates/facts

The following Alloy signatures are given:

sig Address { }
sig Value {}
sig Computer {
  memory: Address -> Value
}
pred write[__________________________________________] {
  ________________________________________________________________
  ________________________________________________________________
  ________________________________________________________________
  ________________________________________________________________
  ________________________________________________________________
}

1. Write an Alloy predicate for the memory write operation. This operation, given an Address addr and a Value val, modifies the memory of a computer at addr setting it to val. The content of all the other memory cells remains unchanged. 
2. Express the following assertion: In every computer’s memory, every memory address contains exactly one value. 
3. Later, we decide that the previous assertion is too strong for our needs. Precisely, we want that every address is associated to at most one value. Our idea is that addresses not associated to any value represent uninitialized memory cells. Suppose a nontrivial analysis scope for Address (say, 100): are there analysis scopes for Value not allowing the analyzer to find a counterexample to this last assertion?   

Exercise 5: Modeling behavior

Define a signature DeterministicFiniteStateMachine, defining a model for the structure (state and transitions) of deterministic finite state machines having:

• exactly one initial state; 
• one or more final states; 
• possibly some dangerous states; 
• zero, one, or more transitions between states. 

Initial and final states cannot be dangerous, but the initial state can possibly be also final. All states must be the source or the target of at least one transition. State machine's transitions are made of a source state, a target state, and an event firing the transition, where events belong to the signature Event.

Write then a predicate named SafeComputation, which, given a DeterministicFiniteStateMachine m and a sequence of states seq, is true if and only if seq is a computation bringing m from its initial state to one of its final states, without passing for a dangerous state. At that scope you may use the module util/sequence[S] and the following declarations contained in it:

• sig Seq, whose atoms are the sequences of atoms of S 
• sig SeqIdx, whose atoms are the indices of the sequences defined by Seq 
• pred add[s: Seq, e: elem, s': Seq], true if and only if s' is obtained by appending e to s 
• pred isEmpty[s: seq], true if and only if s is the empty sequence 
• fun elems[s: Seq]: set S, returning the set containing all the elements of s 
• fun inds[s: Seq]: set S, returning the set of all the indices of s 
• fun first[s: Seq]: lone S, fun last[s: Seq]: lone S, returning the first/last element of s, or the empty set if and only if s is the empty sequence
• pred rest[s, s': Seq], true if and only if s' is the tail (i.e., the sublist starting after its first element) of s
• fun next[i: SeqIdx]: lone SeqIdx, returning the index (if exists)immediately after the index i
• fun at[s: Seq, i: SeqIdx]: lone S, returning the element of s at position i, or the empty set when s does not contain (i.e., is shorter than) i.