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)