A Train Crossing

Open the following model in Uppaal

This is a simplified model of a train crossing with an automaton describing a train, an automaton describing the barrier, and an automaton for the controller. The file overgang.q contains a query that expresses that the barrier is closed whenever the train is at the crossing.

Problem 1

Show that the mentioned safety property does not hold in the model, and generate a diagnostic trace which demonstrates this. Adjust the model in such a way that the property holds.

Problem 2

The automaton for the controller is not input enabled. Is this a problem? If so, adjust the automaton so that it becomes enabled (and the correctness property still holds).

Problem 3

Adjust the model such that there a two trains, which can safely pass the crossing.

Problem 4

If the only requirement for the system would be that the barrier is closed whenever the train is at the crossing, then it would be very easy to build: just keep the barrier closed all the time. What additional requirements should we impose? Check that these requirements hold for the model.