22
33package kotlinx.coroutines.lincheck
44
5- import kotlinx.coroutines.testing.*
65import kotlinx.coroutines.*
76import kotlinx.coroutines.channels.*
87import kotlinx.coroutines.channels.Channel.Factory.CONFLATED
98import kotlinx.coroutines.channels.Channel.Factory.RENDEZVOUS
109import kotlinx.coroutines.channels.Channel.Factory.UNLIMITED
1110import kotlinx.coroutines.selects.*
12- import org.jetbrains.kotlinx.lincheck.*
13- import org.jetbrains.kotlinx.lincheck.annotations.*
14- import org.jetbrains.kotlinx.lincheck.annotations.Operation
15- import org.jetbrains.kotlinx.lincheck.paramgen.*
16- import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
11+ import org.jetbrains.lincheck.datastructures.*
1712
1813class RendezvousChannelLincheckTest : ChannelLincheckTestBaseWithOnSend (
1914 c = Channel (RENDEZVOUS ),
@@ -80,7 +75,7 @@ abstract class ChannelLincheckTestBaseWithOnSend(
8075 sequentialSpecification : Class <* >,
8176 obstructionFree : Boolean = true
8277) : ChannelLincheckTestBase(c, sequentialSpecification, obstructionFree) {
83- @Operation(allowExtraSuspension = true , blocking = true )
78+ @Operation(blocking = true )
8479 suspend fun sendViaSelect (@Param(name = " value" ) value : Int ): Any = try {
8580 select<Unit > { c.onSend(value) {} }
8681 } catch (e: NumberedCancellationException ) {
@@ -98,7 +93,7 @@ abstract class ChannelLincheckTestBase(
9893 private val obstructionFree : Boolean = true
9994) : AbstractLincheckTest() {
10095
101- @Operation(allowExtraSuspension = true , blocking = true )
96+ @Operation(blocking = true )
10297 suspend fun send (@Param(name = " value" ) value : Int ): Any = try {
10398 c.send(value)
10499 } catch (e: NumberedCancellationException ) {
@@ -114,14 +109,14 @@ abstract class ChannelLincheckTestBase(
114109 else false
115110 }
116111
117- @Operation(allowExtraSuspension = true , blocking = true )
112+ @Operation(blocking = true )
118113 suspend fun receive (): Any = try {
119114 c.receive()
120115 } catch (e: NumberedCancellationException ) {
121116 e.testResult
122117 }
123118
124- @Operation(allowExtraSuspension = true , blocking = true )
119+ @Operation(blocking = true )
125120 suspend fun receiveCatching (): Any = c.receiveCatching()
126121 .onSuccess { return it }
127122 .onClosed { e -> return (e as NumberedCancellationException ).testResult }
@@ -132,17 +127,17 @@ abstract class ChannelLincheckTestBase(
132127 .onSuccess { return it }
133128 .onFailure { return if (it is NumberedCancellationException ) it.testResult else null }
134129
135- @Operation(allowExtraSuspension = true , blocking = true )
130+ @Operation(blocking = true )
136131 suspend fun receiveViaSelect (): Any = try {
137132 select<Int > { c.onReceive { it } }
138133 } catch (e: NumberedCancellationException ) {
139134 e.testResult
140135 }
141136
142- @Operation(causesBlocking = true , blocking = true )
137+ @Operation(blocking = true )
143138 fun close (@Param(name = " closeToken" ) token : Int ): Boolean = c.close(NumberedCancellationException (token))
144139
145- @Operation(causesBlocking = true , blocking = true )
140+ @Operation(blocking = true )
146141 fun cancel (@Param(name = " closeToken" ) token : Int ) = c.cancel(NumberedCancellationException (token))
147142
148143 // @Operation TODO non-linearizable in BufferedChannel
@@ -154,9 +149,6 @@ abstract class ChannelLincheckTestBase(
154149 // @Operation TODO non-linearizable in BufferedChannel
155150 open fun isEmpty () = c.isEmpty
156151
157- @StateRepresentation
158- fun state () = (c as ? BufferedChannel <* >)?.toStringDebug() ? : c.toString()
159-
160152 @Validate
161153 fun validate () {
162154 (c as ? BufferedChannel <* >)?.checkSegmentStructureInvariants()
0 commit comments