Even though the behaviour of the EULYNX specification of the level crossing is conceptually quite simple, the state space associated to the mCRL2 model is enormous. This Thursday I will present the reasons for the state space explosion and the measures we took to drastically reduce it. Moreover, I will present the verification efforts, which includes some interesting results.