Preconditions not satisfied after shrinking in commands API #839
Description
I ran into an example, where the Command API delivers a Command Sequence after shrinking, in which not all preconditions are satisfied, although I thought this is impossible. In the example I define the operations Op1, Op2 and Op3.
Op1 can always be executed, Op2 can only be executed when Op1 has already been executed and Op3 can be executed when Op2 has been executed previously. The definition of the SUT is irrelevant for this demonstration.
Op3 is defined to always fails, so Op1 -> Op2 -> Op3 is a counter example. However, after shrinking Op2 -> Op3 is returned. The example is implemented as follows:
import org.scalacheck.commands.Commands
import org.scalacheck.{Gen, Prop, Properties}
import scala.util.Try
object Property extends Properties("Test") {
property("test") = Spec.property()
}
object Spec extends Commands {
case class TestState(op1wasExecuted: Boolean, op2wasExecuted: Boolean)
override type State = TestState
override type Sut = Unit
def canCreateNewSut(newState: State, initSuts: Traversable[State], runningSuts: Traversable[Sut]): Boolean = initSuts.isEmpty && runningSuts.isEmpty
override def newSut(state: TestState): Sut = ()
override def destroySut(sut: Sut): Unit = ()
override def initialPreCondition(state: TestState): Boolean = !state.op1wasExecuted && !state.op2wasExecuted
override def genInitialState: Gen[TestState] = Gen.const(TestState(op1wasExecuted = false, op2wasExecuted = false))
override def genCommand(state: TestState): Gen[Spec.Command] = {
if (state.op1wasExecuted) {
if (state.op2wasExecuted) Gen.oneOf(new Op1(), new Op2(), new Op3())
else Gen.oneOf(new Op1(), new Op2())
}
else Gen.const(new Op1())
}
}
class Op1() extends Spec.UnitCommand {
override def postCondition(state: Spec.TestState, success: Boolean): Prop = true
override def run(sut: Unit): Unit = ()
override def nextState(state: Spec.TestState): Spec.TestState = state.copy(op1wasExecuted = true)
override def preCondition(state: Spec.TestState): Boolean = true
}
class Op2() extends Spec.Command {
override type Result = Unit
override def run(sut: Unit): Unit = ()
override def nextState(state: Spec.TestState): Spec.TestState = state.copy(op2wasExecuted = true)
override def preCondition(state: Spec.TestState): Boolean = state.op1wasExecuted // Op2 shall only be executed if Op1 was executed previously
override def postCondition(state: Spec.TestState, result: Try[Unit]): Prop = true
}
class Op3() extends Spec.UnitCommand {
override def postCondition(state: Spec.TestState, success: Boolean): Prop = false // Op3 always fails
override def run(sut: Unit): Unit = ()
override def nextState(state: Spec.TestState): Spec.TestState = state
override def preCondition(state: Spec.TestState): Boolean = state.op2wasExecuted
}ScalaCheck gives the following output:
failing seed for Test.test is GX7B3gW_SkspZZgtOWeO5D099Lmjexjkr1pTpXBJxjG=
[info] ! Test.test: Falsified after 3 passed tests.
[info] > Labels of failing property:
[info] Initial State:
[info] TestState(false,false)
[info] Sequential Commands:
[info] 1. minimal.Op2@538d1e94
[info] 2. minimal.Op3@4152fa94
[info] > ARG_0: Actions(TestState(false,false),List(minimal.Op2@538d1e94, minimal.Op3@4152fa94),List())
[info] > ARG_0_ORIGINAL: Actions(TestState(false,false),List(minimal.Op1@25b18388, minimal.Op2@538d1e94, minimal.Op3@4152fa94),List())
The original counter example is Op1 -> Op2 -> Op3, which is the minimal sequence to run into the error.
However, after shrinking the counter example is Op2 -> Op3, which is impossible, as the precondition of Op2 is not satisfied initially. I would expect this behaviour if initialPreCondition was omitted, however it is defined that op1wasExecuted is false initially. Therefore, a counter example without Op1 does not make sense to me.
Have I misunderstood something about the way ScalaCheck works, or is this unintentional behaviour?
A workaround for this example would be to change the precondition of Op3 to state.op1wasExecuted && state.op2wasExecuted.