/***********************************************************************************/
/*                                                                                 */
/*                                 TrainWare                                       */
/*                                                                                 */
/*                          Andrew Ireland 29/10/03                                */
/*                                                                                 */
/***********************************************************************************/
/*                                                                                 */
/* A simple railway network involving four stations and four tunnels is modelled.  */
/* The railway network is circular and all the stations are separated by a tunnel. */
/* While each station is modelled by a process, the tunnels are modelled by        */
/* channels. Consequently the movement of trains is modelled by message passing,   */
/* where a train is denoted by a unique number (byte). Although trains only        */
/* travel in one direction, the network is unsafe because trains may travel at     */
/* different rates. Within the model, a crash (unsafe state), corresponds to       */
/* two trains occupying the same tunnel at the same moment in time. Note that a    */
/* two train network, as modelled here, is sufficient to demonstrate that the      */
/* system is unsafe. Note also that the role of the set-up process is to simply    */
/* introduce a train in the network.                                               */
/*                                                                                 */
/***********************************************************************************/


chan TunnelAB = [2] of { byte };
chan TunnelBC = [2] of { byte };
chan TunnelCD = [2] of { byte };
chan TunnelDA = [2] of { byte };

proctype Station(chan in_track, out_track)
{	
        byte train; 

	do
	:: in_track?train; out_track!train
	od
}

proctype Setup(chan track; byte train)
{
	track!train;
}

init {  atomic{ 
        run Setup(TunnelBC, 1); /* introduce train 1 before station C */
        run Setup(TunnelDA, 2); /* introduce train 2 before station A */

        run Station(TunnelDA, TunnelAB);  /* station A */
	run Station(TunnelAB, TunnelBC);  /* station B */
	run Station(TunnelBC, TunnelCD);  /* station C */
        run Station(TunnelCD, TunnelDA)}  /* station D */
}