Spin cycle start label placed incorrectly when first cycle operation is some non-atomic method call

[avpotapov00]

Consider the following example:

**
 * Checks that if spin cycle starts right after method call then spin cycle start event will be placed correctly.
 */
class SpinCycleFirstExecutionIsFirstInMethodCallTest {

    val counter = AtomicInteger(0)
    private val someUselessSharedState = AtomicBoolean(false)

    @Operation
    fun trigger() {
        counter.incrementAndGet()
        counter.decrementAndGet()
    }

    @Operation
    fun causesSpinLock() {
        if (counter.get() != 0) {
            deadSpinCycle()
        }
    }

    private fun deadSpinCycle() {
        do {
            val sharedVariableValue = getSharedVariable()
            someUselessSharedState.compareAndSet(sharedVariableValue, !sharedVariableValue)
        } while (true)
    }

    private fun getSharedVariable(): Boolean = someUselessSharedState.get()

    @Test
    fun test() = ModelCheckingOptions()
        .addCustomScenario {
            parallel {
                thread { actor(SpinCycleFirstExecutionIsFirstInMethodCallTest::trigger) }
                thread { actor(SpinCycleFirstExecutionIsFirstInMethodCallTest::causesSpinLock) }
            }
        }
        .minimizeFailedScenario(false)
        .check(this::class)

}

The output is:

/* The following events repeat infinitely: */ Label is hidden into the getSharedVariable call, it's undesirable.