TrainCrossroads

Bx Examples Repository

Title: TrainCrossroads

Version: 0.1

Type: Sketch

Overview

An accessible illustration of a BX that is not history-ignorant.

A train runs on a figure-of-eight track with a crossroads in the middle. In order to determine the state of the train, it is not in general sufficient to specify its position; only also needs to specify the history of its previous positions. In particular, the train may be “at the crossroads” in two different states (or even four, if you're allowed to pick it up and put it back on the track facing the opposite direction).

Models

The source model space consists of the position of (the centre of the locomotive of) the train together with the direction in which it is facing; the direction is tangent to the track at that position, and (let's say) facing anticlockwise round the left-hand loop of the figure-of-eight and clockwise round the right-hand loop.

The view model space consists solely of the position.

Consistency

Models are consistent when their positions agree.

Consistency Restoration

The state of the view is completely determined by the source. For most views (positions), the source (direction) is also determined; but when the position is the centre of the crossroads, there are two possible directions. One might specify that the train should take the shortest route along the track to the required position, and disambiguate at the extremities (say, move forwards when there is a tie).

Properties

Correct and hippocratic. But not history-ignorant: with the shortest-route consistency restoration as above, a series of short moves may take the train to the crossroads facing the opposite direction to where the composition of those moves would.

Discussion

This example was used in the introductory lecture at the Summer School on BX and Shonan Meeting Seminar 091 on BX.

References

Author(s)

Jeremy Gibbons

Reviewer(s)

Comments

Artefacts

hamleys-wooden-figure-of-8-train-track-set-78012-0-1417083604000.jpg
Unless otherwise stated, the content of this page is licensed under GNU Free Documentation License.