<commit_before>package at.forsyte.apalache.tla.bmcmt.config

import at.forsyte.apalache.infra.{ErrorMessage, ExceptionAdapter, FailureMessage, NormalErrorMessage}
import at.forsyte.apalache.tla.assignments.AssignmentException
import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.bmcmt.types.TypeInferenceError
import at.forsyte.apalache.tla.imp.SanyException
import at.forsyte.apalache.tla.imp.src.SourceStore
import at.forsyte.apalache.tla.lir.{MalformedTlaError, TlaEx}
import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
import at.forsyte.apalache.tla.pp.NotInKeraError
import javax.inject.{Inject, Singleton}

/**
  * The adapter for all exceptions that can be produced when running the model checker.
  *
  * @author <NAME>
  */
@Singleton
class CheckerExceptionAdapter @Inject()(sourceStore: SourceStore,
                                        changeListener: ChangeListener) extends ExceptionAdapter {
  private lazy val ISSUES_LINK: String = "[https://github.com/konnov/apalache/issues]"

  override def toMessage: PartialFunction[Exception, ErrorMessage] = {
    // normal errors
    case err: SanyException =>
      NormalErrorMessage("Error by TLA+ parser: " + err.getMessage)

    case err: AssignmentException =>
      NormalErrorMessage("Error when finding assignments: " + err.getMessage)

    case err: TypeInferenceError =>
      val msg = "%s: type error: %s".format(findLoc(err.origin), err.getMessage)
      NormalErrorMessage(msg)

    // tool failures
    case err: NoRuleException =>
      val msg =
        "%s: no rule to rewrite a TLA+ expression: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: RewriterException =>
      val msg = "%s: rewriter error: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: SmtEncodingException =>
      val msg = "%s: error when rewriting to SMT: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: TypeException =>
      val msg = "%s: type error: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: InvalidTlaExException =>
      val msg = "%s: unexpected TLA+ expression: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: InternalCheckerError =><commit_msg>one more fix in the error message<commit_after>package at.forsyte.apalache.tla.bmcmt.config

import at.forsyte.apalache.infra.{ErrorMessage, ExceptionAdapter, FailureMessage, NormalErrorMessage}
import at.forsyte.apalache.tla.assignments.AssignmentException
import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.bmcmt.types.TypeInferenceError
import at.forsyte.apalache.tla.imp.SanyException
import at.forsyte.apalache.tla.imp.src.SourceStore
import at.forsyte.apalache.tla.lir.{MalformedTlaError, TlaEx}
import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
import at.forsyte.apalache.tla.pp.NotInKeraError
import javax.inject.{Inject, Singleton}

/**
  * The adapter for all exceptions that can be produced when running the model checker.
  *
  * @author <NAME>
  */
@Singleton
class CheckerExceptionAdapter @Inject()(sourceStore: SourceStore,
                                        changeListener: ChangeListener) extends ExceptionAdapter {
  private lazy val ISSUES_LINK: String = "[https://github.com/konnov/apalache/issues]"

  override def toMessage: PartialFunction[Exception, ErrorMessage] = {
    // normal errors
    case err: SanyException =>
      NormalErrorMessage("Error by TLA+ parser: " + err.getMessage)

    case err: AssignmentException =>
      NormalErrorMessage("Assignment error: " + err.getMessage)

    case err: TypeInferenceError =>
      val msg = "%s: type error: %s".format(findLoc(err.origin), err.getMessage)
      NormalErrorMessage(msg)

    // tool failures
    case err: NoRuleException =>
      val msg =
        "%s: no rule to rewrite a TLA+ expression: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: RewriterException =>
      val msg = "%s: rewriter error: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: SmtEncodingException =>
      val msg = "%s: error when rewriting to SMT: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: TypeException =>
      val msg = "%s: type error: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: InvalidTlaExException =>
      val msg = "%s: unexpected TLA+ expression: %s".format(findLoc(err.causeExpr), err.getMessage)
      FailureMessage(msg)

    case err: InternalCheckerError =>
{'fraction_non_alphanumeric': 0.11059518784297172, 'fraction_numerical': 0.0, 'mean_word_length': 3.9416058394160585, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 23, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6894002', 'n_tokens_mistral': 1519, 'n_tokens_neox': 1475, 'n_words': 328}