State Machine Testing

[jeffh]

It would be great to be able to test programs using a state machine:

• Test writer defines a state machine of conceptual app state + transitions. Transitions define
  • What are the preconditions to follow this state.
  • What the transition means for the state machine (returns a new state)
  • What the transition means to run on the subject under test (aka - the real app).
  • What assertions can be made after the transition
• SwiftCheck generates a sequence of transitions that satisfies the state machine
• SwiftCheck then applies the transitions to the subject under test, executing assertions after each transition.

QuickCheck for Erlang implements this in the statem module. Although other developers have attached their own custom solution on top of existing QuickCheck implementations. One that comes to mind is test.check where a company has built their own for a specific use-case and jepsen's knossos.

Thoughts?

[CodaFi]

Yes, yes, let's definitely do this for the next version. This pattern is so useful, I already have a degenerate form of it going in Concurrent and Aquifer. If you can make a representation that makes full use of types like those do you get an incredibly rigid net that tightens over a much wider class of bugs than individual property tests.

[CodaFi]

So, what do we need to do to start making this happen?

[jeffh]

The easiest pass is to compose fromElementsIn and suchThat (Fox does this). It's practical for testing a basic class-level API. But suchThat is inefficient in practice for larger applications.

A better solution is to define generation recursively through flatMap that selects one of the known transitions that's possible give the sequence of current transitions.

But the shrinking is tricky part. I'm not has familiar as haskell-qc variants, but the shrunken result still needs to still needs to satisfy the state machine.

I don't have much time in the immediate future, but a few weeks out I'll probably gather some more spare time.

[CodaFi]

Yeah, I took a look at the way that proper, rapidcheck, and Fox do it. They each take different approaches, each with their own tradeoffs mostly because of their respective implementing languages. I spent the most time with the Erlang versions and came up with this rough translation. It's got a horrible space complexity and the protocol is a bit bloated in my opinion.

public protocol StateM {
    typealias State
    typealias Command

    static var initialState : State { get }

    static var command : Gen<Command> { get }

    static func precondition(_ : State, _ : Command) -> Bool
    static func postcondition(_ : State, _ : Command) -> Bool

    static func nextState(_ : State, _ : Command) -> State
}

extension StateM {
    static func precondition(_ : State, _ : Command) -> Bool {
        return true
    }

    static func postcondition(_ : State, _ : Command) -> Bool {
        return true
    }

    static func commands(initial : State = Self.initialState) -> Gen<[Command]> {
        return Gen.sized { n in
            return Self.commands(n, state: initial, count: 1)
        }
    }

    private static func commands(size : Int, state : State, count : UInt) -> Gen<[Command]> {
        return Gen<[Command]>.frequency([
            (1, Gen.pure([])),
            (size, Self.command.suchThat({ Self.precondition(state, $0) }).flatMap { (cmd) -> Gen<[Command]> in 
                let next = Self.nextState(state, cmd)
                return commands(size.predecessor(), state: next, count: count.successor()).map { 
                    return [cmd] + $0
                }
            })
        ])
    }
}