CSci 420/520: Homework 8

Modeling and Checking in Alloy II

Due Friday, November 4th by 1pm.

Summary

In this assignment, you will be given a specification and asked to complete a Alloy model that satisfies the requirements. You will be provided hints on how to proceed.

Assignment

In this assignment, we model a simple railway safety protocol. We have many trains entering and leaving a train station. These trains follow a certain protocol, and here we want to check whether our protocol works. You are provided a basic stub and instructions to help you write the model. The goal of this assignment is to familarize you with model writing in Alloy.

Here is some background information.

1. We break up the railway tracks into individual segments, where each segment can have at most 1 train. A segment is directional, and only admits traffic from one direction.
2. Each segment has a gate at the end that may prevent a train from continuing on to the next segment. A gate has two states, open and closed. This does not mean a train will always pass through, only that it can.
3. segments are connected by the next relation, which is the set of segments that a train can enter upon leaving a segment. We assume that a train can occupy only one segment.
4. Each segment can conflict with some other segment due to crossings, trains getting so close that they collide, or any other reason. Therefore each segment overlaps a set of other segments. (This relation is symmetric, and generally transitive.)
5. We ignore all timing issues, and only model the transfer of a train from one segment to another. At any given state of the system, some subset of the trains will move to some subset of their next segments.
6. The gates of the segments are governed by the following policies.
   1. If segment A contains a train, then the gates of the segments before A must be closed. This is to prevent other trains from entering A
   2. For any two segments that overlap, there can be at most 1 open gate. Think of two segments, A on the West and B on the East. Both segments meet and merge into a third track C which moves towards North. Either A's gate can be open or B's gate can be open, or none. Having both gates open at the same time may result in a crash.

Instructions

Download the code railway.als and place it into your work directory. Follow the instructions inside the file and complete the model. Note that the second policty doesn't work. If your model is correct, then the first and third policies should check correctly. Write the answers to the questions asked at the end of the specification as comments inside your code.

Grading

At the minimum, all assignments must compile. Questions must be answered in detail, and should be more than a translation of the formal specification.

200 points total.

Email your modified railway.als to meghan@cs.wm.edu.