CPSDebug: Automatic failure explanation in CPS models