Package org.mpi_sws.jmc.annotations

Annotation Interface JmcCheckConfiguration

@Target({METHOD,TYPE}) @Retention(RUNTIME) public @interface JmcCheckConfiguration
Configuration annotation for JMC checks.

The annotation allows users to specify parameters for the tests and is mandatory

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    boolean
    debug
    Enables debug logs and additional information based on the strategy used.
    int
    numIterations
    The number of iterations to run for the JMC check.
    String
    reportPath
    The path where the JMC report will be generated.
    long
    seed
    The seed for the random number generator used in the JMC check.
    String
    strategy
    The strategy to use for the JMC check.

  • Element Details

    • strategy

      String strategy
      The strategy to use for the JMC check.

      Available strategies include:

      • random - Randomly explores the state space.
      • trust - Uses Trust to exhaustively enumerate all executions.
      Returns:
      the strategy name
      Default:
      "random"

    • numIterations

      int numIterations
      The number of iterations to run for the JMC check.

      Either this parameter or a JmcTimeout annotation should be specified for each test

      Returns:
      the number of iterations
      Default:
      0

    • debug

      boolean debug
      Enables debug logs and additional information based on the strategy used.
      Returns:
      true if debug mode is enabled, false otherwise
      Default:
      false

    • reportPath

      String reportPath
      The path where the JMC report will be generated.

      By default, the report is generated in "build/test-results/jmc-report".

      Returns:
      the report path
      Default:
      "build/test-results/jmc-report"

    • seed

      long seed
      The seed for the random number generator used in the JMC check.

      By default, the seed is set to 0, which means a new random seed will be created at runtime.

      Returns:
      the seed value
      Default:
      0L