Your solutions for this assignment must terminate within 30 seconds. 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

Milo needs a way to resolve dependencies in the build system for his new programming language milolang. To create an ordering among dependencies, Milo decides to implement topological sort. Here is Milo'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 any bug in Milo'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 Milo's pseudocode. Finally, run the model to show that the algorithm does not trivially fail (that is, 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 new model is now correct. Similarly, 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 facts or preds or funs. ... is a placeholder and you should fill in (or just remove it entirely if we allow you to do so). However, do not edit the template otherwise, as our autograder will not be able to function properly.

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: Vertex -> Vertex
}{
	... -- Graph is acyclic
}

abstract sig Event {
	pre, post: State,
	v: Vertex -- the choosen vertex for an iteration
}

fact trace {
	... -- Order `State`s
}

sig IterationEventBuggy extends Event {
	... -- You may remove this
}{
	... -- Model an "iteration" of Milo's algorithm here
}

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

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

-- Milo'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 or check by one. See the template code for an example.

Problem 2: Correspondence

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

Note: For this problem, please use our models for the two problems, which
can be found on the website here and here. Please copy the code from these
pages into files called GoatsWolves.als and PetsOwners.als respectively.
The passwords for the files can be found at /gpfs/main/course/cs1950y/pub
in the alloy5_pwd file on the department file system.

If you have any questions about the models, please come to hours or ask on
piazza 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 cs1950y_handin alloy5 from a directory holding your 2 Alloy files (named topsort.als and correspondence.als). You should receive an email confirming that your handin has worked. Both problems are due on 3/16 at 11:59pm.