Writing Tests

Writing Tests #

Here is an example test of 2 threads concurrently incrementing a counter annotated with the necessary annotations to run JMC.

public class CounterTest {
    @JmcCheck
    @JmcCheckConfiguration(strategy = "trust")
    @JmcTimeout(value = 10, unit = ChronoUnit.SECONDS)
    public void testTrustCounter() {
        ParametricCounter counter = new ParametricCounter(2);
        counter.run();
        assert counter.getCounterValue() == 2;
    }
}

The complete test is available here

Each test that runs with JMC requires the following annotations

  1. JmcCheck at the method level to indicate which tests should be run using JMC
  2. JmcCheckConfiguration to define the configuration parameters to run the test. The annotation can be specified either at the class or the method level.
  3. A mandatory parameter in the configuration numIteration or the JmcTimeout annotation to define the boundary of the test. numIteration will bound the number of iterations and JmcTimeout specifies a wall clock timeout.

Refer here for more detailed documentation of all the annotations available.

Annotation free configuration #

Alternatively, the model checker can be configured manually without using any annotations. The above test without using the annotations is as follows,

public void customConfigTrustCounter() {
    try {
        JmcCheckerConfiguration config =
                new JmcCheckerConfiguration.Builder()
                        .strategyType("trust")
                        .numIterations(1000)
                        .build();
        JmcTestTarget target =
                new JmcFunctionalTestTarget(
                        "CounterTest",
                        () -> {
                            ParametricCounter counter = new ParametricCounter(2);
                            counter.run();
                            assert counter.getCounterValue() == 2;
                        });
        JmcModelChecker checker = new JmcModelChecker(config);
        checker.check(target);
    } catch (JmcCheckerException e) {
        System.out.println("Error model checking: " + e.getMessage());
    }
}

The model checker should be instantiated with a JmcCheckerConfiguration and provided a JmcTestTarget. For more details refer to the API docs