#import "PAT.Lib.Queue";

//number of trains
#define N 4;

channel appr 0;
channel go 0;
channel leave 0;
channel stop 0;

parameter Wait11;
parameter Wait10;
parameter Wait4;
parameter Wait1;

var<Queue> queue; 

//Train model with 'within'
Train(i) = appr!i -> ((stop?i  -> StopS(i) within[Wait10]) timeout[Wait10] Cross(i));

Cross(i) = Wait[Wait4]; (leave!i -> Train(i)) within[Wait11];

StopS(i) = go?i -> Start(i);

Start(i) = Wait[Wait10]; (leave!i -> Train(i)) within[Wait10];
 
Gate = if (queue.Count() ==0) {
		    atomic{appr?i ->  tau{queue.Enqueue(i)} -> Skip}; Occ
	   } else {  
	        (go!queue.First() -> Occ) within[Wait10]
    };
 
Occ = (atomic{leave?[i == queue.First()]i -> tau{queue.Dequeue()} -> Skip}; Gate)
     []
     (atomic{appr?i -> tau{queue.Enqueue(i)} -> stop!queue.Last() -> Skip}; Occ);
     
System = (||| x:{0..N-1}@Train(x)) ||| Gate;


#assert System deadlockfree;

//Whenever a train approaches the bridge, it will eventually cross.
#assert System |= [](appr.1 -> <>leave.1);


//verifying bounded responsiveness by refinement checking
Bounded = appr.0 -> Started [] go.0 -> Bounded [] leave.0 -> Bounded [] stop.0 -> Bounded
            [] appr.1 -> Bounded [] go.1 -> Bounded [] leave.1 -> Bounded [] stop.1 -> Bounded
            [] appr.2 -> Bounded [] go.2 -> Bounded [] leave.2 -> Bounded [] stop.2 -> Bounded
            [] appr.3 -> Bounded [] go.3 -> Bounded [] leave.3 -> Bounded [] stop.3 -> Bounded;
Started = Working deadline[30]; Bounded;
Working = appr.0 -> Working [] go.0 -> Working [] leave.0 -> Skip [] stop.0 -> Working
            [] appr.1 -> Working [] go.1 -> Working [] leave.1 -> Working [] stop.1 -> Working
            [] appr.2 -> Working [] go.2 -> Working [] leave.2 -> Working [] stop.2 -> Working
            [] appr.3 -> Working [] go.3 -> Working [] leave.3 -> Working [] stop.3 -> Working;
//overflow: There can never be N elements in the queue (thus the array will not overflow).
#define overflow (queue.Count()> N);
#assert System reaches overflow;

#synthesize System with
	Wait11 = 11,
	Wait10 = 10,
	Wait4 = 4,
	Wait1 = 1
;

#synthesize System reachesall;