Exception message when no operations defined impoved

src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt

@@ -10,6 +10,7 @@
 package org.jetbrains.kotlinx.lincheck
 
 import org.jetbrains.kotlinx.lincheck.annotations.*
+import org.jetbrains.kotlinx.lincheck.annotations.Operation
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
 import org.jetbrains.kotlinx.lincheck.transformation.withLincheckJavaAgent
@@ -74,6 +75,7 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
                 return failure
             }
         }
+        checkAtLeastOneMethodIsMarkedAsOperation(testClass)
         var verifier = createVerifier()
         repeat(iterations) { i ->
             // For performance reasons, verifier re-uses LTS from previous iterations.
@@ -160,6 +162,10 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
             RandomProvider::class.java
         ).newInstance(this, testStructure, randomProvider)
 
+    private fun checkAtLeastOneMethodIsMarkedAsOperation(testClass: Class<*>) {
+        check (testClass.methods.any { it.isAnnotationPresent(Operation::class.java) }) { NO_OPERATION_ERROR_MESSAGE }
+    }
+
     // This companion object is used for backwards compatibility.
     companion object {
         /**
@@ -197,4 +203,6 @@ fun <O : Options<O, *>> O.check(testClass: Class<*>) = LinChecker.check(testClas
  */
 fun <O : Options<O, *>> O.check(testClass: KClass<*>) = this.check(testClass.java)
 
-internal fun <O : Options<O, *>> O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl()
+internal fun <O : Options<O, *>> O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl()
+
+internal const val NO_OPERATION_ERROR_MESSAGE = "You must specify at least one operation to test. Please refer to the user guide: https://kotlinlang.org/docs/introduction.html"

src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/NoOperationsDefinedTest.kt

@@ -0,0 +1,31 @@
+/*
+ * Lincheck
+ *
+ * Copyright (C) 2019 - 2023 JetBrains s.r.o.
+ *
+ * This Source Code Form is subject to the terms of the
+ * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed
+ * with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+package org.jetbrains.kotlinx.lincheck_test.representation
+
+import org.jetbrains.kotlinx.lincheck.NO_OPERATION_ERROR_MESSAGE
+import org.jetbrains.kotlinx.lincheck.check
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
+import org.junit.Assert.assertEquals
+import org.junit.Assert.assertThrows
+import org.junit.Test
+
+/**
+ * This class is used to test the exception message when no operations are defined in a tested class.
+ */
+class NoOperationsDefinedTest {
+
+    @Test
+    fun test() {
+        val exception = assertThrows(IllegalStateException::class.java) { ModelCheckingOptions().check(this::class) }
+        assertEquals(NO_OPERATION_ERROR_MESSAGE, exception.message)
+    }
+
+}