diff --git a/stress-linchk/src/test/scala/dev/tauri/choam/data/ManagedTestExample.scala b/stress-linchk/src/test/scala/dev/tauri/choam/data/ManagedTestExample.scala index 6c7a4dadd..633dfc109 100644 --- a/stress-linchk/src/test/scala/dev/tauri/choam/data/ManagedTestExample.scala +++ b/stress-linchk/src/test/scala/dev/tauri/choam/data/ManagedTestExample.scala @@ -18,25 +18,20 @@ package dev.tauri.choam package data -import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.{ LinChecker, LincheckAssertionError } import org.jetbrains.kotlinx.lincheck.paramgen.IntGen -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.jetbrains.kotlinx.lincheck.annotations.{ Operation, Param } import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import munit.FunSuite @Param(name = "v", gen = classOf[IntGen], conf = "0:127") -class ManagedTestState extends VerifierState { +class ManagedTestState { @volatile private[this] var count: Int = 0 - override def extractState(): AnyRef = { - Integer.valueOf(this.count) - } - @Operation def incr(v: Int): Int = { val curr = this.count @@ -54,8 +49,14 @@ class ManagedTestState extends VerifierState { final class ManagedTestExample extends FunSuite with BaseLinchkSpec { - test("Dummy counter test".ignore) { // expected failure + test("Dummy counter test") { val opts = new ModelCheckingOptions() - LinChecker.check(classOf[ManagedTestState], opts) + try { + LinChecker.check(classOf[ManagedTestState], opts) + fail("expected a lincheck failure") + } catch { + case _: LincheckAssertionError => + () // ok, expected failure + } } } diff --git a/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieModelTest.scala b/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieModelTest.scala index 55c8871b4..2a9092eec 100644 --- a/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieModelTest.scala +++ b/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieModelTest.scala @@ -20,7 +20,6 @@ package data import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.paramgen.StringGen -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.jetbrains.kotlinx.lincheck.annotations.{ Operation, Param } import munit.FunSuite @@ -46,7 +45,7 @@ final object TtrieModelTest { @Param(name = "k", gen = classOf[StringGen]) @Param(name = "v", gen = classOf[StringGen]) - class TestState extends VerifierState { + class TestState { private[this] val emcas: mcas.Mcas = mcas.Mcas.Emcas @@ -54,10 +53,6 @@ final object TtrieModelTest { private[this] val m: Ttrie[String, String] = Ttrie[String, String].unsafeRun(emcas) - override def extractState(): AnyRef = { - m.unsafeSnapshot.unsafeRun(emcas) : scala.collection.immutable.Map[String, String] - } - @Operation def insert(k: String, v: String): Option[String] = { m.put.unsafePerform(k -> v, emcas) diff --git a/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieStressTest.scala b/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieStressTest.scala index ba3a557c0..716432828 100644 --- a/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieStressTest.scala +++ b/stress-linchk/src/test/scala/dev/tauri/choam/data/TtrieStressTest.scala @@ -20,7 +20,6 @@ package data import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.paramgen.StringGen -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.jetbrains.kotlinx.lincheck.annotations.{ Operation, Param } import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions @@ -43,7 +42,7 @@ final class TtrieStressTest extends FunSuite with BaseLinchkSpec { final object TtrieStressTest { @Param(name = "k", gen = classOf[StringGen]) - class TestState extends VerifierState { + class TestState { private[this] val emcas: mcas.Mcas = mcas.Mcas.Emcas @@ -51,10 +50,6 @@ final object TtrieStressTest { private[this] val m: Ttrie[String, String] = Ttrie[String, String].unsafeRun(emcas) - override def extractState(): AnyRef = { - m.unsafeSnapshot.unsafeRun(emcas) : scala.collection.immutable.Map[String, String] - } - @Operation def insert(k: String): Option[String] = { m.put.unsafePerform(k -> "dummy", emcas) diff --git a/stress-linchk/src/test/scala/dev/tauri/choam/skiplist/SkipListModelTest.scala b/stress-linchk/src/test/scala/dev/tauri/choam/skiplist/SkipListModelTest.scala index 2baa1518f..cad994a88 100644 --- a/stress-linchk/src/test/scala/dev/tauri/choam/skiplist/SkipListModelTest.scala +++ b/stress-linchk/src/test/scala/dev/tauri/choam/skiplist/SkipListModelTest.scala @@ -20,7 +20,6 @@ package skiplist import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.paramgen.{ IntGen, StringGen } -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.jetbrains.kotlinx.lincheck.annotations.{ Operation, Param, StateRepresentation } import munit.FunSuite @@ -79,15 +78,11 @@ final object SkipListModelTest { @Param(name = "key", gen = classOf[IntGen]) @Param(name = "value", gen = classOf[StringGen]) - class TestStateSequential extends VerifierState { + class TestStateSequential { private[this] val m = scala.collection.mutable.TreeMap.empty[Int, String] - override def extractState(): Map[Int, String] = { - m.toMap - } - @StateRepresentation def stateRepr(): String = { m.toList.map {