A Model Checker for Interval Temporal Logics over Finite Structures