Cannot get model based test working

Question

As an exercise I wanted to implement a 2-3 finger tree. That should be the perfect opportunity to try out FsCheck's model-based testing. I decided to try the newer experimental version.

So far I only coded one command for the test machine because I already fail at making that work—one the other hand it keeps the post short. The full code is available on GitHub.

open CmdQ
open Fuchu
open FsCheck
open FsCheck.Experimental

type TestType = uint16
type ModelType = ResizeArray<TestType>
type SutType = FingerTree<TestType>

let spec =
    let prepend (what:TestType) =
        { new Operation<SutType, ModelType>() with
            override __.Run model =
                // Also tried returning the same instance.
                let copy = model |> ResizeArray
                copy.Insert(0, what)
                copy

            override __.Check(sut, model) =
                let sutList = sut |> Finger.toList
                let newSut = sut |> Finger.prepend what
                let newSutList = newSut |> Finger.toList
                let modelList = model |> Seq.toList
                let areEqual = newSutList = modelList
                areEqual |@ sprintf "prepend: model = %A, actual = %A (incoming was %A)" modelList newSutList sutList

            override __.ToString() = sprintf "prepend %A" what
        }

    let create (initial:ModelType) =
        { new Setup<SutType, ModelType>() with
            override __.Actual () = initial |> Finger.ofSeq

            override __.Model () = initial //|> ResizeArray // Also tried this.
        }

    let rndNum () : Gen<TestType> = Arb.from<uint16> |> Arb.toGen

    { new Machine<SutType, ModelType>() with
        override __.Setup =
            rndNum()
            |> Gen.listOf
            |> Gen.map ResizeArray
            |> Gen.map create
            |> Arb.fromGen

        override __.Next _ = gen {
            let! cmd = Gen.elements [prepend]
            let! num = rndNum()
            return cmd num
        }
    }

[<Tests>]
let test =
    [spec]
    |> List.map (StateMachine.toProperty >> testProperty "Finger tree")
    |> testList "Model tests"

What I understand is this: Operation<_>.Run is run twice to build up a ResizeArray from one with a single element. Then Operation<_>.Check is run twice with the same numbers to insert into a single element FingerTree<_>.

The first of the two passes. Single-element tree incoming, adding makes it a (correct) two-element tree which compares well against the model after the first command.

The second command is always the one failing. Check is called with the bigger ResizeList (now 3 elements) but the same single-element Tree as in the first command. Adding one more element of course does not get it to size 3 and the test fails.

I would have expected that I need to return the updated model from Check for the commands to come. But you need to return a Property so that's not possible.

Did I completely misunderstand how to approach this? How should a working model-based test be written?

Answer 1

The model-based testing assumes that the "system under test" is modified as a side-effect when Check is called on a particular operation, and initialized for that test run when Setup.Actual() is called. It is intended for dealing with systems that are mutable - like a mutable object - and that style while somewhat bewildering here works out quite nicely with such systems.

Since your finger tree type is immutable, my advice would be to redefine SutType to:

type SutType = Ref<FingerTree<TestType>>

and modify the rest accordingly.