இதை தகவல் செய்: Analysis of the model checkers' input languages for modeling traffic light systems