Each problem in this assignment should be modeled in terms of the event idiom. Make the transition between states an explicit type (Event), and define each event's effects in a sig fact instead of a transition predicate.

You will also need to impose a trace to relate all states with events. To order states, please use the util/ordering module.

Your solutions for this assignment, if not stated otherwise, should terminate within 1 minute. It should have run or check commands ready. Only writing pred or assert is not enough.

Problem 1: Stack

Note: For this problem, you should use the built-in construct seq to help you keep track of your Stack elements. The seq documentation with useful functions can be found here.

Model a last-in first-out stack in Alloy with support for Push and Pop operations. Treat each operation that modifies the stack's state as an event. The stack should begin empty, and you should not be able to Pop from an empty stack.

What properties should a stack obey? You should write assertion statements to verify your model's behavior. Write three assertions verifying the behavior of your stack in the following cases:

As we have not yet covered the event idiom in the class, we provide the following as a template. However, feel free to modify the template however you want (although you must still use the event idiom). For example, if you don't need some sigfacts or facts, or if you want to write additional pred, you can add or remove them as you want.

open util/ordering[StackState]

sig Element {}

sig StackState {
    elements: seq Element
}{
    ...
}

abstract sig Event {
    pre, post: StackState
}{
    ... -- constraints that should hold for each Event
}

fact firstState {
    ... -- constraints for the first StackState
}

fact trace {
    ... 
    -- relate all `StackState`s and `Event`s 
    -- (similar to `nextState` in https://piazza.com/class/iy3a9mkbo83kw?cid=196)
}

sig Push extends Event {
    value: Element
}{
    ... -- model pushing by relating `pre`, `post`, and `value`
}

sig Pop extends Event {
    ...
}{
    ... -- model popping
}

-- HOMEWORK ASSERTION 1
assert popThenPush {
    ...
}
check popThenPush

-- HOMEWORK ASSERTION 2
assert sameNumberPushesPops {
    ...
}
check sameNumberPushesPops

-- HOMEWORK ASSERTION 3
assert noPopFromEmpty {
    ...
}
check noPopFromEmpty

OPTIONAL: If you would like a challenge just for fun, you can try to verify the last-in first-out behavior entirely in a single assertion.

Problem 2: River Crossing

Note: For this problem, we recommend using the built-in construct util/ordering to keep your runtime down (your runtime should be less than 2 minutes). You should be able to model this problem using 11 CrossingEvents.

The following problems are similar to a famous river crossing puzzle involving a goat, wolf, and cabbage. The Alloy Documentation includes a solution to that puzzle here. However, the Alloy example uses predicates (as we did in Tic-Tac-Toe) rather than explicit event sigs. To receive full credit on this assignment, you should explicitly model events.

Part 1: Goats and Wolves

Three goats and three wolves are trying to cross a river in a boat that has room for at most two passengers. The boat cannot cross the river without any passengers. If there are ever more wolves than goats on one side of the river, the wolves will eat the goats. How can the goats and wolves cross safely to the other side? Solve the problem by modeling it in Alloy and using the analyzer to find a solution. Remember, it's generally preferable to use as few constraints as possible to adequately constrain your model.

Part 2: Pets and Owners

Three pet owners and their pets are trying to cross a river. Each owner has exactly one pet. Again, their boat has room for at most two passengers and cannot cross the river without passengers. If a pet is in the presence of another person, its own owner must also be present - otherwise, the pet's owner will be jealous and worry that the other person will try to steal their beloved pet! How can the pets and pet owners cross the river without making any of the pet owners jealous? You should solve the problem by modeling it in Alloy and using the analyzer to find a solution.

Part 3: Relationship

Do you notice any similarities between these two problems? Describe the relationship between them, either by showing how a solution to one can be constructed given a solution to the other, or by showing why such a construction is not possible. Your answer should be explained in words in a text file.

Problem 3: Bridge Crossing

Four people want to cross a bridge at night, but the bridge is narrow and at most two people can cross at once. They only have one torch, and due to darkness, the torch must be always carried while crossing the bridge. Person A can walk across the bridge in 1 minute, B in 2 minutes, C in 5 minutes, D in 8 minutes, and when two people cross the bridge together, they must move at the slower person's pace. How can they all get across the bridge in 15 minutes or less? Model the problem in Alloy, and use the analyzer to find a solution.

Handing In

Run cs1950y_handin alloy4 from a directory holding your 4 Alloy files (stack.als, goats_and_wolves.als, pets_and_owners.als, bridge.als), and one text file (relationship.txt). You should receive an email confirming that your handin has worked.

Credit

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