//////////////////////////////////////////////////////
//		                    
//   ASM Specification of The ITC	 	
//                                   	
//                Specification     
//////////////////////////////////////////////////////

freetype DATA == { abstract }

freetype  IS_SORT == {green, red, exiting, entering}   //Island State

static function Data == { abstract }
static function maxcar == abstract   // max number of cars allowed in the tunnel
static function zero == abstract

static function incr == MAP_TO_FUN {abstract -> abstract} 
static function decr == MAP_TO_FUN {abstract -> abstract} 

dynamic function tc : DATA with tunnelCounter in Data initially zero 
dynamic function ic : DATA with islandCounter in Data initially zero 

dynamic function islandstate: IS_SORT initially red		


////////////////////////////////////////////////////
//			 Island Light Controller   
external function carentering: BOOL
external function carexiting: BOOL
external function islandgranted: BOOL
external function islandrelease: BOOL

//outputs
dynamic function islandrequest: BOOL initially undef  
dynamic function islanduse: BOOL initially undef
dynamic function islandred: BOOL initially undef  
dynamic function islandgreen: BOOL initially undef	

//  Behavioral description for the island light controller  ILC----

transition ILCS == 
block
if ( islandstate = green ) then
	islandgreen := true
	islanduse := true
	islandred := false
	islandrequest := false
	if(islandrelease) then
		islandstate := red
	else
		if(carentering) then
   			ic := decr(ic)
			tc := incr(tc)
			islandstate := entering
		else
			islandstate := green
		endif
	endif
endif

if ( islandstate = red ) then
	islandred := true
	islanduse := false
	islandgreen := false
	if(carentering) then
		islandrequest := true
	else
		islandrequest := false	
	endif
	
	if(carexiting) then
		tc := decr(tc)
		islandstate := exiting
	else
		if(islandgranted ) then
			islandstate := green
		else
			islandstate := red
		endif
	endif

endif
if ( islandstate = entering ) then
	islandgreen := true
	islanduse := true
	islandred := false
	islandrequest := false	
	if(carentering) then
		islandstate := entering
	else
		islandstate := green
	
	endif
endif

endblock
