dtmc

// Sensor states
const int protocol_start		= -1;
const int start 			= 0;
const int updateClock			= 1;
const int maxStateValue			= updateClock;
const int cycleLength 			= 10;

const int refractoryPeriod;
const double mu;
const double epsilon ;

const maxOsc = 3;

global flash:[0..maxOsc] ;



init 
	(flash = 0) &
	(s1State = protocol_start) & 
	(s2State = protocol_start) & 
	(s3State = protocol_start) 
endinit


formula pert1 = (s1LocalClock*epsilon*flash - floor(s1LocalClock * epsilon *flash)) >= 0.5 ? ceil(s1LocalClock*epsilon*flash) : floor(s1LocalClock*epsilon*flash);
formula pert2 = (s2LocalClock*epsilon*flash - floor(s2LocalClock * epsilon *flash)) >= 0.5 ? ceil(s2LocalClock*epsilon*flash) : floor(s2LocalClock*epsilon*flash);
formula pert3 = (s3LocalClock*epsilon*flash - floor(s3LocalClock * epsilon *flash)) >= 0.5 ? ceil(s3LocalClock*epsilon*flash) : floor(s3LocalClock*epsilon*flash);

module flash_updater
	flash_state :[0..maxStateValue] ;
	[] (flash_state = start) -> (flash' = 0) & (flash_state' = updateClock);
	[updateClock] (flash_state = updateClock) -> (flash_state' = start);
endmodule


module sensor1	
	s1State : [-1..maxStateValue] ;
 	s1LocalClock : [1..cycleLength] ;
	[protocol_start] (s1State = protocol_start) -> (s1State' = start);

	// START

	[] 	  (s1State = start) 
		& (s1LocalClock = cycleLength) 
		& (flash_state = updateClock)
	    	& (flash < maxOsc)
	-> 
							(1-mu): (s1State' = updateClock) & (flash' = flash+1) 
							+(mu) : (s1State' = updateClock) ;
	[]   	  (s1State = start) 
	  	& (s1LocalClock + pert1+1 > cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s1LocalClock != cycleLength)
		& (s2LocalClock = cycleLength | s3LocalClock = cycleLength)
		& (s2State = updateClock | s2LocalClock <= s1LocalClock)
		& (s3State = updateClock | s3LocalClock <= s1LocalClock)
	-> 
		(1-mu): (s1State' = updateClock) & (flash' = flash+1) 
		+(mu) : (s1State' = updateClock) ;

	[]   	  (s1State = start) 
	  	& (s1LocalClock + pert1+1  <= cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s1LocalClock != cycleLength)
		& (s2LocalClock = cycleLength | s3LocalClock = cycleLength)
		& (s2State = updateClock | s2LocalClock <= s1LocalClock)
		& (s3State = updateClock | s3LocalClock <= s1LocalClock)
	->
		(s1State' = updateClock)
	;
	[]   	  (s1State = start) 
		& (s1LocalClock != cycleLength) 
		& (s2LocalClock != cycleLength)
		& (s3LocalClock != cycleLength)
		& (flash_state=updateClock)  
		-> 
							
		(s1State' = updateClock) ;

// UPDATE CLOCK & SYNC
	[updateClock] (s1State = updateClock) & (s1LocalClock = cycleLength) 						
		-> 
							(s1State' = start) & (s1LocalClock' = 1)
							;

	[updateClock] 	  (s1State = updateClock) & (s1LocalClock < cycleLength) 
		    	& (s1LocalClock <= refractoryPeriod)							
		-> 
		  	  (s1State' = start) 
			& (s1LocalClock' = s1LocalClock + 1) 
			;
	[updateClock]    (s1State = updateClock) & (s1LocalClock < cycleLength)  
		       	& (s1LocalClock > refractoryPeriod)	
			& (s1LocalClock + pert1 + 1 <= cycleLength)	
		-> 
			  (s1State' = start) 
			& (s1LocalClock' = s1LocalClock + pert1 +1 ) 
							;
	[updateClock]	  (s1State = updateClock) 
			& (s1LocalClock < cycleLength) 
			& (s1LocalClock > refractoryPeriod)	
			& (s1LocalClock + pert1 + 1 > cycleLength)	
		-> 
	   		  (s1State' = start) & (s1LocalClock' = 1) 				
			;

endmodule

module sensor2	
	s2State : [-1..maxStateValue] ;
 	s2LocalClock : [1..cycleLength] ;
	[protocol_start] (s2State = protocol_start) -> (s2State' = start);

	// START
	[]	  (s2State = start) 
		& (s2LocalClock = cycleLength) 
		& (flash_state = updateClock)
		& (flash < maxOsc)	
	-> 
		(1-mu): (s2State' = updateClock) & (flash' = flash+1) 
		+(mu) : (s2State' = updateClock) ;

	[]   	  (s2State = start) 
	  	& (s2LocalClock + pert2 +1> cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s2LocalClock != cycleLength)
		& (s1LocalClock = cycleLength | s3LocalClock = cycleLength)
		& (s1State = updateClock | s1LocalClock <= s2LocalClock)
		& (s3State = updateClock | s3LocalClock <= s2LocalClock)
	-> 
		(1-mu): (s2State' = updateClock) & (flash' = flash+1) 
		+(mu) : (s2State' = updateClock) ;

	[]   	  (s2State = start) 
	  	& (s2LocalClock + pert2 +1 <= cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s2LocalClock != cycleLength)
		& (s1LocalClock = cycleLength | s3LocalClock = cycleLength)
		& (s1State = updateClock | s1LocalClock <= s2LocalClock)
		& (s3State = updateClock | s3LocalClock <= s2LocalClock)
	-> 
		(s2State' = updateClock)
	;
	[] 	  (s2State = start) 
		& (s1LocalClock != cycleLength) 
		& (s2LocalClock != cycleLength)
		& (s3LocalClock != cycleLength)
		& (flash_state=updateClock)  
	-> 
	 	  (s2State' = updateClock) ;

	// UPDATE CLOCK & SYNC
	[updateClock] (s2State = updateClock) & (s2LocalClock = cycleLength) 						-> 
							(s2State' = start) & (s2LocalClock' = 1);
	
	[updateClock] 	  (s2State = updateClock) & (s2LocalClock < cycleLength) 
		    	& (s2LocalClock <= refractoryPeriod)							
		-> 
		  	  (s2State' = start) 
			& (s2LocalClock' = s2LocalClock + 1) 
			;
	[updateClock]    (s2State = updateClock) & (s2LocalClock < cycleLength)  
		       	& (s2LocalClock > refractoryPeriod)	
			& (s2LocalClock + pert2 +1 <= cycleLength)
		-> 
			  (s2State' = start) 
			& (s2LocalClock' = s2LocalClock + pert2 +1)
							;
	[updateClock]	  (s2State = updateClock) 
			& (s2LocalClock < cycleLength) 
			& (s2LocalClock > refractoryPeriod)	
			& (s2LocalClock +pert2 + 1 > cycleLength)	
		-> 
	   		  (s2State' = start) & (s2LocalClock' = 1) 				
			;

endmodule

module sensor3	
	s3State : [-1..maxStateValue] ;
 	s3LocalClock : [1..cycleLength] ;
	[protocol_start] (s3State = protocol_start) -> (s3State' = start);

	// START
	[] 	  (s3State = start) 
		& (s3LocalClock = cycleLength) 
		& (flash_state = updateClock)
		& (flash < maxOsc)	
	-> 
							(1-mu): (s3State' = updateClock) & (flash' = flash+1) 
							+(mu) : (s3State' = updateClock) ;

	[]   	  (s3State = start) 
	  	& (s3LocalClock + pert3 +1  > cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s3LocalClock != cycleLength)
		& (s1LocalClock = cycleLength | s2LocalClock = cycleLength)
		& (s1State = updateClock | s1LocalClock <= s3LocalClock)
		& (s2State = updateClock | s2LocalClock <= s3LocalClock)
	-> 
		(1-mu): (s3State' = updateClock) & (flash' = flash+1) 
		+(mu) : (s3State' = updateClock) ;

	[]   	  (s3State = start) 
	  	& (s3LocalClock + pert3  +1 <= cycleLength)
		& (flash_state = updateClock)
		& (flash > 0)
		& (flash < maxOsc)
		& (s3LocalClock != cycleLength)
		& (s1LocalClock = cycleLength | s2LocalClock = cycleLength)
		& (s1State = updateClock | s1LocalClock <= s3LocalClock)
		& (s2State = updateClock | s2LocalClock <= s3LocalClock)
	-> 
		  (s3State' = updateClock) ;	

	[] (s3State = start)  
		& (s1LocalClock != cycleLength) 
		& (s2LocalClock != cycleLength)
		& (s3LocalClock != cycleLength)
		& (flash_state=updateClock)  
-> 
							(s3State' = updateClock) ;

// UPDATE CLOCK & SYNC
	[updateClock] (s3State = updateClock) & (s3LocalClock = cycleLength) 						-> 
							(s3State' = start) & (s3LocalClock' = 1);
	
	[updateClock] 	  (s3State = updateClock) & (s3LocalClock < cycleLength) 
		    	& (s3LocalClock <= refractoryPeriod)							
		-> 
		  	  (s3State' = start) 
			& (s3LocalClock' = s3LocalClock + 1) 
			;
	[updateClock]    (s3State = updateClock) & (s3LocalClock < cycleLength)  
		       	& (s3LocalClock > refractoryPeriod)	
			& (s3LocalClock + pert3 + 1 <= cycleLength)	
		-> 
			  (s3State' = start) 
			& (s3LocalClock' = s3LocalClock + pert3 + 1) 
							;
	[updateClock]	  (s3State = updateClock) 
			& (s3LocalClock < cycleLength) 
			& (s3LocalClock > refractoryPeriod)	
			& (s3LocalClock +  pert3 + 1 > cycleLength)
		-> 
	   		  (s3State' = start) & (s3LocalClock' = 1) 				
			;
endmodule

