Package org.mpi_sws.jmc.annotations

Annotation Interface JmcTimeout

@Target({METHOD,TYPE}) @Retention(RUNTIME) public @interface JmcTimeout
This annotation is used to specify a timeout for a test method or class when using the JMC model checker. It can be applied to methods or classes.

The timeout value is specified in the specified time unit, and if the test exceeds this duration, it will be considered failed.

Either this or the JmcCheckConfiguration.numIterations() should be specified mandatorily for each test

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    long
    value
    The timeout value for the annotated test method or class.

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    ChronoUnit
    unit
    The time unit for the timeout value.

  • Element Details

    • value

      long value
      The timeout value for the annotated test method or class.

      This value is used to determine how long the test should run before it is considered failed due to timeout.

      Returns:
      the timeout value

    • unit

      ChronoUnit unit
      The time unit for the timeout value.

      This specifies the unit of time for the timeout value, such as seconds, milliseconds, etc.

      Returns:
      the time unit for the timeout
      Default:
      SECONDS