Package org.mpi_sws.jmc.annotations

Annotation Interface JmcExpectExecutions

@Target({METHOD,TYPE}) @Retention(RUNTIME) public @interface JmcExpectExecutions
This annotation is used to mark a test method or class to expect a certain number of executions in the JMC model checker. It can be applied to methods or classes.

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    int
    value
    The expected number of executions for the annotated test method or class.

  • Element Details

    • value

      int value
      The expected number of executions for the annotated test method or class.

      This value is used to verify that the JMC model checker produces the expected number of executions during the test run.

      Returns:
      the expected number of executions