freetype DATA == { abstract }
static function Data ==  {abstract} 
static function maxcar == abstract
static function zero == abstract
static function Bool == { true, false } 

static function incr == MAP_TO_FUN {abstract -> abstract} 
static function decr == MAP_TO_FUN {abstract -> abstract} 
static function lt ==  MAP_TO_FUN  {abstract*abstract -> Bool}

dynamic function tc : DATA with tunnelCounter in Data initially zero 

external function carentering: BOOL
external function carexiting: BOOL
external function mainlandgranted: BOOL
external function mainlandrelaease: BOOL
//external function lt: BOOL

dynamic function  mainlandgreen: BOOL initially false  
dynamic function  mainlanduse: BOOL initially  false
dynamic function  mainlandrequist: BOOL initially  false  
dynamic function  mainlandred: BOOL initially false 

dynamic function d2: BOOL initially undef
dynamic function d1: BOOL initially undef

static function or2 (in0,in1) == in0 or in1

static function or3 (in0,in1,in2) == in0 or in1 or in2
static function or4 (in0,in1,in2,in3) == in0 or in1 or in2 or in3
  
static function and2 (in0,in1) == in0 and  in1
static function and3 (in0,in1, in2) == in0 and  in1 and in2
   
static function nand2 (in0,in1) == not (in0 and in1)

static function and4 (in0,in1,in2,in3) == in0 and  in1 and in2 and  in3
 
static function inv (in0) == not (in0)

static function mux4(s0, s1, in0, in1, in2, in3) ==
        if s0 and s1 then in3 
        elseif (not (s0) and s1) then in2       
        elseif s0 and not (s1) then in1  
        elseif not (s0) and not(s1) then in0
end

transition MLCI == 
block
	d2 := or2(and2(d2,or2(carexiting,mainlandgranted)),
		and2(d1,or3(d2,mainlandrelaease,inv(lt(tc,maxcar)))))
		
	d1 := or3(and2(and2(d2,inv(d1)),or2(carexiting,mainlandgranted)),
		nor2(carentering,or3(d2,mainlandrelaease,inv(lt(tc,maxcar)))),
		and3(inv(or3(d2,mainlandrelaease,inv(lt(tc,maxcar))),
		d1,and(carentering,and2(d2,inv(d1)))))) 
		
mainlandred := d2
mainlandgreen := inv(d2)
mainlanduse := inv(d2)
mainlandrequist := and3( d2,inv(d1),carentering)
tc = mux4(d2,or2(and2(carentering,and2(d2,inv(d1))),
		and3(carentering,d1,inv(or3(d2,mainlandrelaease,inv(lt(tc,maxcar)))))),
		tc,tc,decr(tc),incr(tc))
endblock
