IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata