types
	TimeSteps = {Int0 = 0 , Int20 = 20, Int30 = 30, Int270 = 270} ;
	Int = int[0..270] ;
	SmallInt = int[0..3] ;
	AlarmSystem = autocons system
	|[
		var
			open : bool = true ;
			locked : bool = false ;
			armed : bool = false ;
			soundAlarm : bool = false ;
			flashAlarm : bool = false ;
			blockingLevel : SmallInt = 0 ;
			armedOnNow : bool = false ;
			armedOnLater : bool = false ;
			armedOff : bool = false ;
			soundOn : bool = false ;
			soundOffNow : bool = false ;
			soundOffLater : bool = false ;
			flashOn : bool = false ;
			flashOffNow : bool = false ;
			flashOffLater : bool = false  ;
			silent : bool = false # true after alarms turned off
		actions
			ctr Close ( waittime : Int) =
				requires not flashAlarm and not soundAlarm :
					requires open and waittime = 0 and blockingLevel = 0 and locked and silent:
						open := false ;
						blockingLevel := 1 ;
						armedOnNow := true ;
						silent := false			

					end []
					requires open and waittime = 0 and blockingLevel = 0 and not locked and silent:
						silent := false ;			
						open := false 
					end []
					requires open and waittime = 0 and blockingLevel = 0 and locked and not silent:
						open := false ;
						blockingLevel := 1 ;
						armedOnLater := true

					end []
					requires open and waittime = 0 and blockingLevel = 0 and not locked and not silent:
						open := false 
					end

				end ;

			ctr Open ( waittime : Int) =
				requires true :
					requires not open and waittime = 0 and blockingLevel = 0 and not armed :
						open := true
					end []
					requires not open and waittime = 0 and blockingLevel = 0 and armed :
						open := true ;
						armed := false ;
						blockingLevel := 3 ;
						armedOff := true ;
						soundOn := true ;
						flashOn := true
					end 
				end ;

#				requires not open and waittime = 0 and blockingLevel = 0 :
#					open := true ;
#					(requires not armed :
#						skip
#					end []
#					requires armed :
#						armed := false ;
#						blockingLevel := 3 ;
#						armedOff := true ;
#						soundOn := true ;
#						flashOn := true 
#					end)
#				end ;
			ctr Unlock ( waittime : Int) =
				requires true : 
					requires locked and waittime = 0 and blockingLevel = 0 and not flashAlarm and soundAlarm:
						locked := false ;
						silent := false ;
						soundOffLater := false ;
						soundOffNow := true ;
						blockingLevel := 1 
					end []
					requires locked and waittime = 0 and blockingLevel = 0 and flashAlarm and soundAlarm :
						locked := false ;
						flashOffNow := true ;
						blockingLevel := 2 ;
						silent := false ;
						soundOffLater := false ;
						soundOffNow := true

					end []
					requires locked and waittime = 0 and blockingLevel = 0 and not flashAlarm and not soundAlarm:
						locked := false ;
						silent := false ;
						armedOff := true ;
						blockingLevel := 1
					end []
					requires locked and waittime = 0 and blockingLevel = 0 and flashAlarm and not soundAlarm:
						locked := false ;
						flashOffNow := true ;
						flashOffLater := false ;
						blockingLevel := 1 ;
						silent := false
					end
				end;
				
			ctr Lock ( waittime : Int) =
				requires true :
					requires not locked and waittime = 0 and blockingLevel = 0 and open :
						locked := true
					end []
					requires not locked and waittime = 0 and blockingLevel = 0 and not open :
						locked := true ;
						blockingLevel := 1 ;
						armedOnLater := true
					end 
				end ;
			obs ArmedOn (waittime : Int) =
				requires (armedOnNow or armedOnLater):
					requires (waittime = 20 and armedOnLater) :
						armedOnLater := false ;
						blockingLevel := blockingLevel - 1 ;
						armed := true
					end
					[] requires (waittime = 0 and armedOnNow) :
						armedOnNow := false ;
						blockingLevel := blockingLevel - 1 ;
						armed := true
					end
				end ;
			obs ArmedOff (waittime : Int) =
				requires (waittime = 0 and armedOff) :
					armedOff := false ;
					blockingLevel := blockingLevel - 1 ;
					armed := false
				end ;
			obs SoundOn (waittime : Int) =
				requires true :
					requires (waittime = 0 and soundOn and blockingLevel = 1) :
						soundOn := false ;
						blockingLevel := blockingLevel - 1 ;
						soundAlarm := true ;
						soundOffLater := true 
					end []
					requires (waittime = 0 and soundOn and blockingLevel <> 1) :
						soundOn := false ;
						blockingLevel := blockingLevel - 1 ;
						soundAlarm := true
					end 
	
				end ;
			obs SoundOff (waittime : Int) =
				requires (soundOffNow or soundOffLater) :
					requires (waittime = 30 and soundOffLater) :
						soundOffLater := false ;
						flashOffLater := true ;
						soundAlarm := false
					end
					[] requires (waittime = 0 and soundOffNow) :
						soundOffNow := false ;
						blockingLevel := blockingLevel - 1 ;
						soundAlarm := false
					end
				end ;
			obs FlashOn (waittime : Int) =
				requires true :
					requires (waittime = 0 and flashOn and blockingLevel = 1) :
						flashOn := false ;
						blockingLevel := blockingLevel - 1 ;
						flashAlarm := true ;
						soundOffLater := true 
					end []
					requires (waittime = 0 and flashOn and blockingLevel <> 1) :
						flashOn := false ;
						blockingLevel := blockingLevel - 1 ;
						flashAlarm := true
				end 
				end ;
			obs FlashOff (waittime : Int) =
				requires (flashOffNow or flashOffLater) :
					requires (waittime = 270 and flashOffLater) :
						flashOffLater := false ;
#						blockingLevel := blockingLevel - 1 ;
						flashAlarm := false ;
						silent := true
					end
					[] requires (waittime = 0 and flashOffNow) :
						flashOffNow := false ;
						blockingLevel := blockingLevel - 1 ;
						flashAlarm := false
					end
				end
	do
		var A : TimeSteps : Close (A) [] 
		var B : TimeSteps : Open (B) []
		var C : TimeSteps : Lock (C) []
		var D : TimeSteps : Unlock (D) []
		var E : TimeSteps : ArmedOn (E) []        
		var F : TimeSteps : ArmedOff (F) []        
		var G : TimeSteps : SoundOn (G) []        
		var H : TimeSteps : SoundOff (H) []   
    		var I : TimeSteps : FlashOn (I) []        
		var J : TimeSteps : FlashOff (J)    
	od
	]|
system
	AlarmSystem