=== The Counterexample ===

-------- Assumptions --------

lt(tc#2,maxcar_) = 0

-------- Initial state --------
mainlandstate_A = red_
d1_B = 0
d2_B = 1

-------- Clock cycle 1 --------

  -- The symbolic input --

carexiting = 0
mainlandgranted = 1
tc = tc#1

  -- The symbolic state --

mainlandstate_A = green_
d1_B = 1
d2_B = 0

-------- Clock cycle 2 --------

  -- The symbolic input --

carentering = 0
mainlandrelease = 0
tc = tc#2

  -- The symbolic state --

mainlandstate_A = red_
d1_B = 1
d2_B = 1

-------- Clock cycle 3 --------

  -- The symbolic input --

carexiting = 0
mainlandgranted = 1
tc = tc#3

  -- The symbolic state --

mainlandstate_A = green_
d1_B = 0
d2_B = 1

-------- Clock cycle 4 --------

  -- The symbolic input --

carentering = 0
carexiting = 0
tc = tc#4

  -- Symbolic Output --

mainlandrequest_A = 0
mainlandrequest_B = 0
mainlandgreen_A = 1
mainlandred_A = 0
mainlanduse_A = 1
mainlandred_B = 1
mainlandgreen_B = 0
mainlanduse_B = 0
tc_B0 = tc#4
tc_A0 = tc#4