*****************************************************************

*Macros for CTL-

*****************************************************************




prop AG(P) = max(Z.P & [-]Z);
prop EF(P) = min(X.P|<->X);
prop AF(P) = min(X.P|(<->T&[-]X));
prop EG(P) = max(X.P&([-]F|<->X));







**********************************************************************
*  Train crossing
*
*  This is the train crossing in page 12 of Stirling's book
**********************************************************************
**********************************************************************
*  The definition of the "Road"
**********************************************************************
agent Road = car.up.'ccross.'down.Road;

**********************************************************************
*  The definition of the "Rail"
**********************************************************************
agent Rail = train.green.'tcross.'red.Rail;

**********************************************************************
*  The definition of the "Signal"
**********************************************************************
agent Signal = 'green.red.Signal + 'up.down.Signal;

**********************************************************************
*  The crossing 
**********************************************************************
agent Crossing = (Road | Rail | Signal)\{green,red,up,down};

**********************************************************************
* A safety property
**********************************************************************
prop Safety = AG(['ccross]F | ['tcross]F);

**********************************************************************
* No deadlocks
**********************************************************************
prop Nodeadlocks = AG(<->T);

**********************************************************************
* Liveness properties: are they ok?
**********************************************************************
prop Livecar = AG([car] AF(<'ccross>T & [-'ccross]F));
prop Livetrain = AG([train] AF(<'tcross>T & [-'tcross]F));