/*
 * For more details about this example, see 
 * "Automatic Verification of Real-Time Communicating Systems by Constraint Solving", 
 * by Wang Yi, Paul Pettersson and Mats Daniels. In Proceedings of the 7th International
 * Conference on Formal Description Techniques, pages 223-238, North-Holland. 1994.
 */

default(N,6) dnl;         // N = number of trains + 1, N have to be at least 5.
default(ERROR,0)

byte e[N];

/* simulates clock x*/
byte x;

// min_{i=1}^{N-1}(max_x_i) is the maximum value of clock x.
// Usually this maximum=25, but in states Cross{x<=5}, Appr{x<=20} and Start{x<=15}
// the clock is limited by value 5, 15 or 20. 

define(max_x, `byte max_x_$1;')

forloop(j, 1, decr(N), `max_x(j)')


channel       appr, stop, go, leave;
channel       is_empty, notempty, hd, add, rem;

define(train, `process Train_$1{
state Safe, Stop, Cross, Appr, Start;
init Safe;
trans Appr -> Cross{guard x>=10; effect x=0, max_x_$1=5; },
Appr -> Stop{guard x<=10 && e==$1; sync stop?; effect x=0, max_x_$1=25; },
Cross -> Safe{guard x>=3; sync leave!; effect e=$1, x=0, max_x_$1=25; },
Safe -> Appr{sync appr!; effect e=$1, x=0, max_x_$1=20; },
Start -> Cross{guard x>= ifelse(ERROR,0,`7',`5'); effect x=0, max_x_$1=5; },
Stop -> Start{guard e==$1; sync go?; effect x=0, max_x_$1=15; };
}

')

process Clock{
state S1;
init S1;
trans S1 -> S1{guard  
define(guard_max_x, `x<=max_x_$1 &&') forloop(j, 2, decr(N), `guard_max_x(j)')
 x<=max_x_1;
               effect x=x+1; };
}

process Gate{
state S1, S2, S3, S4, S5, S6, Occ, Free, Send;
init Free;
trans Free -> S5{sync notempty?; },
Free -> S4{sync is_empty?; },
Occ -> S6{sync appr?; },
Occ -> S1{sync leave?; },
S6 -> S2{sync stop!; },
Send -> Occ{sync go!; },
S5 -> Send{sync hd!; },
S4 -> S3{sync appr?; },
S3 -> Occ{sync add!; },
S2 -> Occ{sync add!; },
S1 -> Free{sync rem?; };
}

process IntQueue{
byte list[N], len, i;
state Start, Shiftdown;
init Start;
trans Shiftdown -> Shiftdown{guard i < len; effect list[i]=list[i+1], i=i+1; },
Shiftdown -> Start{guard len==i; effect list[i] = 0, i = 0;  },
Start -> Shiftdown{guard len>=1; sync rem!; effect len=len-1, i = 0; },
Start -> Start{guard len==0; sync is_empty!; },
Start -> Start{sync add?; effect list[len]=e, len=len+1; },
Start -> Start{sync hd?; effect e=list[0]; },
Start -> Start{guard len>0; sync notempty!; };
}

forloop(j, 1, decr(N), `train(j)')

system async;