Annotations #

JmcCheck #

The primary annotation to mark a test to be run using JMC. Does not contain any parameters

JmcCheckConfiguration #

Required for each test, either at the method level or the class level. The parameters available are

• numIteration - To specify the number of iterations for JMC checker to run.
• strategy - A string to configure the built-in strategy to use. Available values are random and trust. Refer to Strategies for strategy specific annotations.
• debug - A boolean to enable debug logs and additional reporting of the model checking process.
• reportPath - The path to store the model checking reports. Defaults to build/test-results/jmc-report
• seed - The random seed used by the strategy.

JmcTimeout #

Defines the duration to run the model checker. Either this or the numIteration parameter of JmcCheckConfiguration is mandatory.

JmcReplay #

When the model checker reports a bug, the trace is recorded. Mark the test with this annotation temporarily to replay the exact trace that led to the bug.

JmcExpectAssertionFailure #

Inform JMC that the test is expected to fail with an assertions error. Any other error will lead the test to fail.

JmcExpecteExecutions #

Apart from assertions in the code, use this annotation to inform JMC of the number of executions that are expected to run before stopping. Useful only with the trust strategy where the number of executions explored is optimal.

JmcIgnoreInstrumentation #

Use with the code to mark specific classes. The classes are then ignored by JMC when instrumenting and adding additional event logging necessary for JMC’s working. Mandatory when using custom strategies.