-
Notifications
You must be signed in to change notification settings - Fork 0
/
DistributedIncrementCounterTest.kt
55 lines (42 loc) · 1.47 KB
/
DistributedIncrementCounterTest.kt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
package info.potapov
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions
import org.jetbrains.kotlinx.lincheck.verifier.VerifierState
import org.junit.jupiter.api.Test
/**
* Test that checks linearizable behavior for a counter with an increment of 1
*/
internal class DistributedIncrementCounterTest {
private val counter = DistributedCounter(4)
@Operation
fun increment() = counter.increment(1)
val count: Int @Operation get() = counter.count
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.iterations(10)
.invocationsPerIteration(100_000)
.threads(3)
.actorsPerThread(4)
.sequentialSpecification(CounterVerifierState::class.java)
.check(this::class.java)
@Test
fun stressTest() = StressOptions()
.iterations(100)
.invocationsPerIteration(100_000)
.actorsBefore(2)
.actorsAfter(2)
.threads(3)
.actorsPerThread(3)
.sequentialSpecification(CounterVerifierState::class.java)
.check(this::class.java)
class CounterVerifierState : VerifierState() {
private var counter = 0
fun increment() {
counter++
}
val count: Int get() = counter
override fun extractState() = counter
}
}