Abstract: The paper describes the design of a coloured Petri net model for a rather complex model train system. The purpose of this system is to teach graduate CS students net modelling and analysis techniques, and the systematic concersion of non-trivial net models into fully operational real systems. The track layout of this system currently includes three main cyclic tracks, each subdivided into several sections, three switchyards of several sidings, and also interconnecting tracks via which trains may change main tracks and directions.
The idea is to equip each of several trains - currently up to ten - with its own travel plan. It specifies a sequence of tracks through which the train must be routed in the given order. Execution of these plans must be dynamically coordinated based on locally made decisions about the allocation of track sections to requesting trains so that essential safety and liveness properties are met.
The paper first introduces the basic net components necessary to model train movement along track sections and across branching and merging switches, then describes the composition of a complete track model from these components, including the controls necessary to enforce an orderly behaviour, and then outlines the composition of the complete system model. It also addresses some of the as yet unsolved problems of deadlock prevention in the system.