Function model_check_ta 

fn model_check_ta(
    ta: GeneralThresholdAutomaton,
    spec: ELTLSpecification,
    model_checker: Option<ModelCheckerOption>,
    config: TACOConfig,
    abort_on_violation: bool,
) -> ModelCheckerResult