/*
		          Airware

                   Andrew Ireland 25/01/01                             

A simple Promela model of airspace involving four sectors, i.e.
A, B, C and D. Two aircraft are modelled by the processes AircraftX 
and AircraftY. The locations of the aircraft are modelled by the 
variables locationX and locationY respectively. Note that the
decision as to where an aircraft travels within the airspace
is determined by the aircraft. Within this model a midair
collision (unsafe state) corresponds to two aircraft occupying 
the same sector at the same moment in time. Note that a two aircraft 
system is sufficient to demonstrate that the system is unsafe.

*/

mtype = {A, B, C, D};

mtype locationX = A;
mtype locationY = D;


proctype AircraftX()
{	

   do
      :: (locationX == A) -> if
                             :: locationX = B;
                             :: locationX = C;
                             :: locationX = D;
                             fi;
      :: (locationX == B) -> if
                             :: locationX = A;
                             :: locationX = C;
                             :: locationX = D;
                             fi;
      :: (locationX == C) -> if
                             :: locationX = B;
                             :: locationX = A;
                             :: locationX = D;
                             fi;
      :: (locationX == D) -> if
                             :: locationX = B;
                             :: locationX = C;
                             :: locationX = A;
                             fi;
   od
}

proctype AircraftY()
{	

   do
      :: (locationY == A) -> if
                             :: locationY = B;
                             :: locationY = C;
                             :: locationY = D;
                             fi;
      :: (locationY == B) -> if
                             :: locationY = A;
                             :: locationY = C;
                             :: locationY = D;
                             fi;
      :: (locationY == C) -> if
                             :: locationY = B;
                             :: locationY = A;
                             :: locationY = D;
                             fi;
      :: (locationY == D) -> if
                             :: locationY = B;
                             :: locationY = C;
                             :: locationY = A;
                             fi;
   od
}

init { atomic{ run AircraftX(); run AircraftY() }}