###keys
gstat clock lane[0] lane[1] lane[2] lane[3] lane[4] lane[5] lane[6] lane[7] v[0] v[1] v[2] v[3] v[4]
###textDisplay
clock::::EXT
clock#0 clock#1
v[0]::::EXT
v[0]#1 v[0]#2
v[1]::::EXT
v[1]#1 v[1]#2
v[2]::::EXT
v[2]#1 v[2]#2
v[3]::::EXT
v[3]#1 v[3]#2
v[4]::::EXT
v[4]#1 v[4]#2
v[5]::::EXT
v[5]#1 v[5]#2
v[6]::::EXT
v[6]#1 v[6]#2
v[7]::::EXT
v[7]#1 v[7]#2
###states
(gstat: nFin clock:(0,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,running,oo,oo) v[2]:(1,running,oo,oo) v[3]:(5,running,0,oo) v[4]:(5,running,oo,oo)) ||
(gstat: nFin clock:(0,true) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,running,oo,oo) v[2]:(1,running,oo,oo) v[3]:(5,approaching,0,oo) v[4]:(5,running,oo,oo)) ||
(gstat: nFin clock:(0,true) (lane[0]: oo) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,running,oo,oo) v[2]:(1,approaching,0,oo) v[3]:(5,approaching,0,oo) v[4]:(5,running,oo,oo)) ||
(gstat: nFin clock:(0,true) (lane[0]: oo) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,running,oo,oo) v[2]:(1,approaching,0,oo) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(0,true) (lane[0]: 1) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,approaching,0,oo) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(0,true) (lane[0]: 1) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,stopped,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(1,false) (lane[0]: 1) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,stopped,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(1,false) (lane[0]: 1) (lane[1]: 2) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,crossing,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(1,false) (lane[0]: 1) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,running,oo,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,crossed,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(1,true) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,approaching,1,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,crossed,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,approaching,1,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,crossed,0,0) v[3]:(5,approaching,0,oo) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,approaching,1,oo)  v[1]:(0,approaching,0,oo) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,approaching,1,oo)  v[1]:(0,stopped,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,stopped,1,0)  v[1]:(0,stopped,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossing,1,0)  v[1]:(0,crossing,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,approaching,0,oo)) ||
(gstat: nFin clock:(2,false) (lane[0]: 1 ; 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossing,1,0)  v[1]:(0,crossing,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,stopped,0,0)) ||
(gstat: nFin clock:(2,false) (lane[0]: 0) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossing,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,stopped,0,0)) ||
(gstat: nFin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,stopped,0,0) v[4]:(5,stopped,0,0)) ||
(gstat: nFin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 3 ; 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossing,0,0) v[4]:(5,crossing,0,0)) ||
(gstat: nFin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: 4) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossing,0,0)) ||
(gstat: nFin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0)) ||
(gstat: fin clock:(2,false) (lane[0]: oo) (lane[1]: oo) (lane[2]: oo) (lane[3]: oo) (lane[4]: oo) (lane[5]: oo) (lane[6]: oo) (lane[7]: oo) v[0]:(0,crossed,1,0)  v[1]:(0,crossed,0,0) v[2]:(1,crossed,0,0) v[3]:(5,crossed,0,0) v[4]:(5,crossed,0,0))