OoasTools

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