/*****************************************************************************/
/*                                                                           */
/*                             nonABStrainware                               */
/*                                                                           */
/*                          Andrew Ireland 22/10/06                          */
/*                                                                           */
/*                                F29NM1                                     */
/*                                                                           */
/*****************************************************************************/
/*                                                                               
A simple railway network involving three defective signals and two block  
sections of track is modelled. While the defective signals are
modelled as processes, the block sections of track are modelled by
channels. The movement of trains is modelled by message passing, where 
a train is denoted by a 1 (bit). Although trains only travel in one
direction, the network is unsafe because the defective signals allow
multiple trains to enter the same block section of track at the same
time, i.e. within the model, a crash (unsafe state), corresponds to       
two trains occupying the same block section of track at the same
time. 
*/
#define train 1
	ltl p1 { [](len(BlockSecAB) < 2)) } 

chan BlockSecAB = [2] of { bit };
chan BlockSecBC = [2] of { bit };

proctype SignalA(chan out_track)
{
        do
        :: out_track!1
        od
}

proctype SignalB(chan in_track, out_track)
{
        do
        :: in_track?train;
           out_track!train
        od
}

proctype SignalC(chan in_track)
{
        do
        :: in_track?train;
        od
}

init {  atomic{
        run SignalA(BlockSecAB);
        run SignalB(BlockSecAB, BlockSecBC);
        run SignalC(BlockSecBC) }
}