fun runWithLincheck()

in trace-debugger/src/main/org/jetbrains/lincheck/trace/debugger/TraceDebuggerInjections.kt [35:80]


    fun runWithLincheck() {
        firstRun = false

        val (testClass, testMethod) = TraceAgentParameters.getClassAndMethod()

        val isStaticMethod = Modifier.isStatic(testMethod.modifiers)
        val instanceClass = if (isStaticMethod) TraceDebuggerStaticMethodWrapper::class.java else testClass

        val scenario = scenario {
            parallel {
                thread {
                    // TODO: current implementation does not support `testMethod`
                    //  that accepts arguments (e.g. java main function)
                    if (isStaticMethod) {
                        actor(
                            TraceDebuggerStaticMethodWrapper::callStaticMethod,
                            testClass, testMethod
                        )
                    } else {
                        actor(testMethod.kotlinFunction!!)
                    }
                }
            }
        }

        val lincheckOptions = ModelCheckingOptions()
            .iterations(0)
            .invocationsPerIteration(1)
            .addCustomScenario(scenario)
            .addGuarantee(forClasses(TraceDebuggerInjections::class).allMethods().ignore())
            .verifier(FailingVerifier::class.java)
            .logLevel(LoggingLevel.OFF)
            .invocationTimeout(5 * 60 * 1000) // 5 mins

        val failure = lincheckOptions.checkImpl(instanceClass)

        val result = failure!!.results.threadsResults[0][0]
        if (result is ExceptionResult) throw result.throwable

        if (!TraceAgentParameters.traceDumpFilePath.isNullOrEmpty() && failure.trace != null) {
            val dumpFile = File(TraceAgentParameters.traceDumpFilePath!!)
            dumpFile.parentFile?.mkdirs()
            dumpFile.createNewFile()
            dumpFile.writeText(failure.toString())
        }
    }