//////////////////////////////////////////////////////
//		                    
//   ASM Specification of The MLC	 	
//                                   	
//                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 mainlandstate: IS_SORT initially red		


////////////////////////////////////////////////////
//			 Island Light Controller   
external function carentering: BOOL
external function carexiting: BOOL
external function mainlandgranted: BOOL
external function mainlandrelease: BOOL

//outputs
dynamic function mainlandred: BOOL initially undef  
dynamic function mainlandgreen: BOOL initially undef	
dynamic function mainlandrequest: BOOL initially undef  
dynamic function mainlanduse: BOOL initially undef

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

 transition MLC_SPEC == 
block
if (mainlandstate = red) then
	mainlandred := true
	mainlandgreen := false
	mainlandrequest := carentering
	mainlanduse := false
	if(carexiting) then
		tc := decr(tc)
		mainlandstate := exiting
	else 
		if (mainlandgranted) then
			mainlandstate := green
		endif
	endif
endif

if ( mainlandstate = exiting ) then
	mainlandred := true
	mainlandgreen := false	
	mainlanduse := false
	mainlandrequest := false
	if(carexiting) then
		mainlandstate := exiting
	else
	 	mainlandstate := red
	endif
endif	

if ( mainlandstate = green ) then
	mainlandred := false
	mainlandgreen := true
	mainlanduse := true
	mainlandrequest := false
	if( tc < maxcar) then
		if(mainlandrelease) then
			mainlandstate := red
		else 
			if(carentering) then
				tc := incr(tc)
				mainlandstate := entering
			endif
		endif	
	else
		mainlandstate := red
	endif
endif

if ( mainlandstate = entering ) then
	mainlandred := false
	mainlandgreen := true
	mainlanduse := true
	mainlandrequest := false
	if(carentering) then
		mainlandstate := entering
	else
	 	mainlandstate := green
	endif
endif
endblock
