A model-based testing framework inspired by quick-check-state-machine.

First, we create a (hopefully simple) model capable of representing the persistance layer of the system under test.

```
newtype Model
= Model (List Int)
```

We need to be able to initialize the system with arbitrary models. Because we already have instances of `Arbitrary Int`

and `Arbitrary a ⇒ Arbitrary (List a)`

, we can use the derive newtype strategy to create arbitrary models that contain integer lists of arbitrary sizes.

`derive newtype instance arbitraryModel ∷ Arbitrary Model`

Now that the model is defined, we need to represent the form of commands that can be generated. Here, because we are simulating a FIFO queue we use the three commands push, pop, and length.

```
data Command
= Push Int
| Pop
| GetLength
```

The last data class we need to define is the result of a command, which we'll call `Response`

. Note that, while responses map 1-to-1 to commands, this is not necessary for the underlying algorithm to work.

```
data Response
= Pushed
| Popped (Maybe Int)
| GotLength Int
derive instance eqResponse ∷ Eq Response
```

This is our generator of commands that will used to create test cases. In this case, we generate commands with an even probability. Note that, unlike other stateful PBT libraries, this library does *not* use a separate function to impose preconditions. If there are preconditions, you need to include them in the generator of commands that is passed to `testModel`

.

```
instance arbitraryCommand ∷ Arbitrary Command where
arbitrary = do
i ← arbitrary
oneOf $ NonEmpty (pure $ Push i) [ pure Pop, pure GetLength ]
```

Then, we define a mock of the system under test.

```
mock ∷ Model → Command → (Tuple Model Response)
mock (Model m) (Push i) = (Tuple (Model (i : m)) Pushed)
mock (Model m) Pop =
let
s = unsnoc m
in
maybe (Tuple (Model Nil) (Popped Nothing))
(\x → Tuple (Model x.init) (Popped $ Just x.last))
s
mock mm@(Model m) GetLength = Tuple mm (GotLength $ length m)
```

We then need to define a postcondition. The postcondition here is simple - we just verify that the mocked response is equal to the real response. This won't always work, ie if a server generates UUIDs. In that case, we'll need some other comparison, but for here, simple equality comparison works.

```
postcondition ∷ Command → Response → Response → (Outcome String String)
postcondition _ r0 r1 = if r0 == r1 then (pure "passed") else (pure "failed")
```

This functino is used to initialize the system under test with a given model. This is used, for example, if you need to initialze a DB in the system under test.

```
initializer ∷ Model → Aff Unit
initializer (Model l) = do
let
arr = toUnfoldable l ∷ Array Int
einit (fromFoldable l)
```

This is the system under test. It uses a file called ./test/Queue.purs that, under the hood, uses JavaScript via the FFI to represent a FIFO queue.

```
sut ∷ Command → Aff Response
sut (Push i) = do
epush i
pure Pushed
sut Pop = Popped <$> epop
sut GetLength = GotLength <$> elng
```

We use a simple shrinker to shrink commands.

```
shrinker ∷ ∀ a. List a → List (List a)
shrinker c = mapWithIndex (\i _ → fromMaybe Nil (deleteAt i c)) c
```

This is the main function that does the PBT and validates the results.

```
isSuccess ∷ ∀ a b. Outcome a b → Boolean
isSuccess (Outcome (Left _)) = false
isSuccess (Outcome (Right _)) = true
main ∷ Effect Unit
main = launchAff_ $ runSpec [consoleReporter] do
describe "checkStateMachine" do
it "works" do
res ← liftEffect $ testModel {
seed: 0,
nres: 100,
setup: esetup,
teardown: eteardown,
modelInitializer: initializer,
initialModelGenerator: arbitrary,
commandListGenerator: arbitrary,
commandShrinker: shrinker,
mock, sut, postcondition }
100 `shouldEqual` (length $ filter (\r → isSuccess r.outcome) res)
```

Check out the test for a full working example.