freetype DATA == { abstract }
static function Data ==  {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} 

dynamic function tc : DATA with tunnelCounter in Data initially zero 

external function carentering: BOOL
external function carexiting: BOOL
external function islandgranted: BOOL
external function islandrelaease: BOOL

dynamic function  islandgreen: BOOL initially false  
dynamic function  islanduse: BOOL initially  false
dynamic function  islandrequist: BOOL initially  false  
dynamic function  islandred: 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 nor2 (in0,in1) == not (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 mux2(s0, in0, in1) ==
        if s0 then in1 
        else in0  
end

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 ILCI == 
block
	d2 := or2(and2(and2(d1,inv(carexiting)),nand2(d2,islandgranted)),
		and2(inv(d1),or2(carentering,and2(islandrelaease,inv(d2)))))

	d1 := or2(and2(islandrelaease,inv(d2)),and2(d1,or3(carexiting,inv(d2),inv(islandgranted))))		
		
islandred := d1
islandgreen := inv(d1)
islanduse := inv(d1)
islandrequist := and3(d1,d2,carentering)

tc := mux2(and2(and2(carentering,inv(islandrelaease)),nor2(d1,d2)),mux2(and3(d1,d2,carexiting),tc,decr(tc)),incr(tc))
endblock
// ic := mux4(and2(nor2(d1,d2),and2(carentering,
// inv(islandrelaease))),
// and3(carexiting,d1,d2),ic,incr(ic),decr(ic),ic)
