Review

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java

@@ -116,9 +116,9 @@ private void checkStateEquivalenceImpl(Class<?> testClass) {
             Object i2 = createTestInstance(testClass);
             if (i1.hashCode() != i2.hashCode() || !i1.equals(i2)) {
                 throw new IllegalStateException(
-                    "equals() and hashCode() methods for a test instance are not defined or defined incorrectly.\n" +
-                    "To define equals() and hashCode() methods the test class should extend `VerifierState` class and override `extractState()` function.\n" +
-                    "This check may be suppressed by setting the option `requireStateEquivalenceImplementationCheck = false`."
+                    "equals() and hashCode() methods for this test are not defined or defined incorrectly.\n" +
+                    "It is more convenient to make the test class extend `VerifierState` class and override `extractState()` function to define equals() and hashCode() methods.\n" +
+                    "This check may be suppressed by setting the requireStateEquivalenceImplementationCheck option to false."
                 );
             }
         }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java

@@ -120,7 +120,9 @@ public OPT verifier(Class<? extends Verifier> verifier) {
     }
 
     /**
-     * Require correctness check of test instance state equivalency relation defined by the user
+     * Require correctness check of test instance state equivalency relation defined by the user.
+     * It checks whether two new instances of a test class are equal.
+     * If the check fails [{@link IllegalStateException}] is thrown.
      */
     public OPT requireStateEquivalenceImplCheck(boolean require) {
         this.requireStateEquivalenceImplementationCheck = require;

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchCTest.java

@@ -101,7 +101,9 @@
     Class<? extends Verifier> verifier() default LinearizabilityVerifier.class;
 
     /**
-     * Require correctness check of test instance state equivalency relation defined by the user
+     * Require correctness check of test instance state equivalency relation defined by the user.
+     * It checks whether two new instances of a test class are equal.
+     * If the check fails [{@link IllegalStateException}] is thrown.
      */
     boolean requireStateEquivalenceImplCheck() default true;
 

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java

@@ -101,7 +101,9 @@
     Class<? extends Verifier> verifier() default LinearizabilityVerifier.class;
 
     /**
-     * Require correctness check of test instance state equivalency relation defined by the user
+     * Require correctness check of test instance state equivalency relation defined by the user.
+     * It checks whether two new instances of a test class are equal.
+     * If the check fails [{@link IllegalStateException}] is thrown.
      */
     boolean requireStateEquivalenceImplCheck() default true;
 

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ResultAsParameterTest.java

@@ -28,11 +28,15 @@
 import org.jetbrains.kotlinx.lincheck.annotations.Param;
 import org.jetbrains.kotlinx.lincheck.paramgen.IntGen;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
 import org.junit.Test;
 
+import java.util.ArrayList;
+import java.util.List;
+
 @OpGroupConfig(name = "push_remove", nonParallel = true)
-@StressCTest(requireStateEquivalenceImplCheck = false)
-public class ResultAsParameterTest {
+@StressCTest
+public class ResultAsParameterTest extends VerifierState {
     private Stack stack = new Stack();
     private Node lastPushNode = null;
 
@@ -58,6 +62,14 @@ public synchronized boolean remove() {
     public void test() {
         LinChecker.check(ResultAsParameterTest.class);
     }
+
+    @Override
+    protected Object extractState() {
+        List<Integer> elements = new ArrayList<>();
+        int e;
+        while ((e = stack.pop()) != -1) elements.add(e);
+        return elements;
+    }
 }
 
 class Stack {

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/StateEquivalenceImplCheckTest.kt

@@ -0,0 +1,21 @@
+package org.jetbrains.kotlinx.lincheck.test
+
+import org.jetbrains.kotlinx.lincheck.LinChecker
+import org.jetbrains.kotlinx.lincheck.annotations.Operation
+import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest
+import org.junit.Test
+import java.lang.IllegalStateException
+import java.util.concurrent.atomic.AtomicInteger
+
+@StressCTest
+class StateEquivalenceImplCheckTest {
+    private var i = AtomicInteger(0)
+
+    @Operation
+    fun incAndGet() = i.incrementAndGet()
+
+    // Check that IllegalStateException is thrown if `requireStateEquivalenceImplCheck` option is true by default
+    // and hashCode/equals methods are not implemented
+    @Test(expected = IllegalStateException::class)
+    fun test() = LinChecker.check(StateEquivalenceImplCheckTest::class.java)
+}

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchCTestAnnTest.java

@@ -26,14 +26,15 @@
 import org.jetbrains.kotlinx.lincheck.annotations.Operation;
 import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
 import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier;
 import org.junit.Test;
 
 import java.util.concurrent.atomic.AtomicInteger;
 
 @StressCTest(threads = 3, actorsPerThread = 3, iterations = 10, invocationsPerIteration = 5,
-        generator = RandomExecutionGenerator.class, verifier = LinearizabilityVerifier.class, requireStateEquivalenceImplCheck = false)
-public class RandomSwitchCTestAnnTest {
+        generator = RandomExecutionGenerator.class, verifier = LinearizabilityVerifier.class)
+public class RandomSwitchCTestAnnTest extends VerifierState {
     private AtomicInteger i = new AtomicInteger();
 
     @Operation()
@@ -45,4 +46,9 @@ public int incAndGet() {
     public void test() {
         LinChecker.check(RandomSwitchCTestAnnTest.class);
     }
+
+    @Override
+    protected Object extractState() {
+        return i.get();
+    }
 }

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressCTestAnnTest.java

@@ -22,18 +22,20 @@
  * #L%
  */
 
+import org.jetbrains.annotations.NotNull;
 import org.jetbrains.kotlinx.lincheck.LinChecker;
 import org.jetbrains.kotlinx.lincheck.annotations.Operation;
 import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
 import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier;
 import org.junit.Test;
 
 import java.util.concurrent.atomic.AtomicInteger;
 
 @StressCTest(threads = 3, actorsPerThread = 3, iterations = 10, invocationsPerIteration = 5,
-        generator = RandomExecutionGenerator.class, verifier = LinearizabilityVerifier.class, requireStateEquivalenceImplCheck = false)
-public class StressCTestAnnTest {
+        generator = RandomExecutionGenerator.class, verifier = LinearizabilityVerifier.class)
+public class StressCTestAnnTest extends VerifierState {
     private AtomicInteger i = new AtomicInteger();
 
     @Operation()
@@ -45,4 +47,9 @@ public int incAndGet() {
     public void test() {
         LinChecker.check(StressCTestAnnTest.class);
     }
+
+    @Override
+    protected Object extractState() {
+        return i.get();
+    }
 }

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/EpsilonVerifierTest.kt

@@ -26,15 +26,18 @@ import org.jetbrains.kotlinx.lincheck.LinChecker
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest
 import org.jetbrains.kotlinx.lincheck.verifier.EpsilonVerifier
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState
 import org.junit.Test
 
-@StressCTest(verifier = EpsilonVerifier::class, requireStateEquivalenceImplCheck = false)
-class EpsilonVerifierTest {
+@StressCTest(verifier = EpsilonVerifier::class)
+class EpsilonVerifierTest : VerifierState() {
     private var i = 0
 
     @Operation
     fun incAndGet() = i++ // non-atomic!
 
     @Test
     fun test() = LinChecker.check(EpsilonVerifierTest::class.java)
+
+    override fun extractState() = i
 }

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/quantitative/KStackTest.kt

@@ -116,7 +116,7 @@ class KStackRelaxedPopIncorrectTest {
     }
 }
 
-@StressCTest(verifier = QuantitativelyRelaxedLinearizabilityVerifier::class, threads = 2, actorsPerThread = 2, invocationsPerIteration = 1)
+@StressCTest(verifier = QuantitativelyRelaxedLinearizabilityVerifier::class)
 @QuantitativeRelaxationVerifierConf(factor = K, pathCostFunc = MAX, costCounter = KStackRelaxedPushAndPopTest.CostCounter::class)
 class KStackRelaxedPushAndPopTest {
     private val s = KStackSimulation<Int>(k = K)