Your solutions for this assignment should terminate within 4 minutes. If they exceed the time limit, you will get a partial credit. Please also note how long your solutions take to run as a comment if they do exceed the time limit.

Problem 1: Topsort (revisited)

The problem has two parts and has a template code which you have to follow. Please read the entire problem before beginning writing your code.

Part 1

Blue needs a way to resolve dependencies in the build system for her new programming language cluelang. To create an ordering among dependencies, Blue decides to implement topological sort. Here is Blue’s pseudocode:

L ← Empty list that will contain the sorted elements
S ← Set of all nodes with no incoming edges
while S is non-empty do
    remove a node n from S
    add n to tail of L
    for each node m with an edge e from n to m do
        remove edge e from the graph
        insert m into S
return L (a topologically sorted order)

Use Alloy to find the bug in the Blue’s algorithm. To do this, first model the algorithm itself. Then write an assertion that would hold for a correct implementation of topological sort. check this assertion to find a counterexample that demonstrates the bug in Blue’s pseudocode. Additionally, run the model to show that it has an instance.

Part 2

Now, adjust your model to fix the bug you found in Part 1. Use the same assert statement from Part 1 to show that your model is now correct. Additionally, run the model to show that it has an instance.

For both parts, you must use the sigs in the template code below. Feel free to adjust the numbers in the run and check to fit your specification (see additional constraints at the end of Problem 1). Also, feel free to add additional fact or pred or fun. ... is a placeholder and you can replace it with whatever you want (or just remove it entirely if you don’t need anything there)

open util/ordering[State]

sig Vertex { }
sig State {
    L: seq Vertex, -- List of sorted elements
    S: set Vertex, -- Set of nodes with no incoming edges
    Graph: set Vertex -> Vertex
}{
    no iden & ^Graph -- Graphs are acyclic
}

abstract sig Event {
    pre, post: State,
    v: Vertex
}

fact transitions {
    all s: State - last | let s' = s.next |  one e: Event | e.pre = s and e.post = s'
}

sig IterationEventBuggy extends Event {
    ...
}{
    ... -- Model an "iteration" of Blue's algorithm here
}

sig IterationEventCorrect extends Event {
    ...
}{
    ... -- Model an "iteration" of the correct algorithm here
}

assert correctness {
    ... -- Holds for correct algorithms
}

-- Blue's algorithm:
check correctness for 8 but 7 Vertex, 0 IterationEventCorrect, 8 Int -- This should have a counterexample
run {} for 8 but 7 Vertex, 0 IterationEventCorrect, 8 Int -- This should have an instance (though might be incorrect)

-- Correct algorithm:
check correctness for 8 but 7 Vertex, 0 IterationEventBuggy, 8 Int -- This should have no counterexample
run {} for 8 but 7 Vertex, 0 IterationEventBuggy, 8 Int -- This should have an instance

Note: the number to run / check (for ...) should not be less than 8 when you submit, but you can change it however you want when implementing

Note 2: One problem that might come up is that there are too many Vertex, and the algorithm does not have enough State (recall that when we use util/ordering[State], the number of State will be fixed). A workaround is to give the number of Vertex to be less than the number to run / check by one. See the template code for an example.

Problem 2: Correspondence

Recall the two River Crossing problems from Alloy 2. Now, formalize the correspondence between the two problems.

Note: For this problem, please use our models for the two problems, which can be found in /course/cs195y/src/alloy5. If you have any questions about the models, please come to hours or email the TA list to be sure you fully understand them before you proceed with this problem.

To do this, you will need a third module, which uses the two modules we provided as follows:

open GoatsWolves as gw
open PetsOwners as po

First, write a relation from states of one problem to states of the other. That is, a relation of the form

{gw/State0 -> po/State0, gw/State1 -> po/State1, gw/State2 -> po/State2,...}

Next, write a predicate that expresses the correspondence between states of one problem and states of the other.

Finally, write an assertion that if there is a solution to Pets and Owners and the correspondence predicate holds for each state, then the corresponding states of Goats and Wolves will also be a solution.

check your assertion to show that your correspondence is correct.

Handing In

Run cs195y_handin alloy5 from a directory holding your 2 Alloy files (topsort.als, and correspondence.als). You should receive an email confirming that your handin has worked.