Stevan A

> In the one Model the reference would become 1, while in the other 2 and there is no proper way to combine them. True, that's really ugly. How about...

> Building the general Model seems hard though. Why so? The history contains all commands and their responses, using the initial model and the transition functions should let us build...

I'm not saying we should use `linearise` directly, only use it as inspiration for how we can traverse the history and rebuild a model.

`interleavings` can perhaps be reused directly though!

Any of the possible interleavings should be good enough to rebuild the model, I think.

> Maybe the cleanup, user-defined function should be History -> IO () and provide the user with the utility function History -> Model Concrete (this function will also need the...

> if the execution failed on the n-th command of the list, there is no reason to test a prefix smaller than n. You mean greater than n? > However...

Perhaps it would make sense to move your trick into the library? That way we can also use `Map (Reference ...)`-like models...

I thought a bit more about this, and I'm beginning to wonder if post-conditions shouldn't have the type `model Symbolic -> act Symbolic resp -> resp -> Bool`? Or perhaps...

I played around a bit more with this in #209, [see](https://github.com/advancedtelematic/quickcheck-state-machine/pull/209/commits/d069ad92eb9a49ee70506c850418d4f1e6ce16e6): ```haskell data Concrete a where Concrete :: Typeable a => a -> Unique -> Concrete a instance Eq (Concrete...