@Test
    public void modelCheckingTest()
    {
        ModelCheckingOptions options = new ModelCheckingOptions();
        // The size of the test can be changed with 'options.iterations' or `options.invocationsPerIteration`.
        // The first one defines the number of different scenarios generated,
        // while the second one determines how deeply each scenario is tested.
        new LinChecker(this.getClass(), options).check();
    }
This test checks that the concurrent set is linearizable with bounded model checking.
Unlike stress testing, this approach can also provide a trace of an incorrect execution.
However, it uses sequential consistency model, so it can not find any low-level bugs (e.g., missing 'volatile'),
and thus, it it recommended to have both test modes.
jctools-core/src/test/java/org/jctools/maps/linearizability_test/LincheckSetTest.java