Stevan A

The Cleanroom people have some neat tools, e.g. [JUMBL](https://sourceforge.net/p/jumbl/code/ci/master/tree/), for analysing Markov chains. For more information see: - http://jumbl.sourceforge.net/ - https://sourceforge.net/projects/jumbl/files/jumbl_user.pdf/download - https://www.researchgate.net/publication/265184529_Computations_for_Markov_Chain_Usage_Models

Some important progress was made in the blog post ["An in-depth look at quickcheck-state-machine"](http://www.well-typed.com/blog/2019/01/qsm-in-depth/), see especially the "Labelling" section. Some of those ideas are now part of the `Test.StateMachine.Labelling` module...

There's also `features/3` and `call_features/{1,2}` in the eqc statem [API](http://quviq.com/documentation/eqc/index.html), not sure if they are part of the labelled examples machinery though.

Another [talk](https://www.youtube.com/watch?v=NcJOiQlzlXQ) by John Hughes that explains `labelledExamples` is called *Building on developers' intuitions to create effective property-based tests*.

Looks nice! How do you handle overlapping/concurrent actions? Currently it looks like `Write` and `Increment` both start and finish exactly at the same time, this shouldn't happen. Because as we...

> It is possible that this order is different from the execution order. Yeah, that's possible. Can you think of a way to improve this situation? Because linearisability relies there...

> We can't find the order they happen by the result Why do you want to find the order by (from?) the result? We know _when_ `semantics` of a command...

> That's not enough though to find the order, since these times give us only a interval in which an action was commited. My understanding of the linearisability [paper](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf) is...

> We seem to agree that the exact order is unknown. Yeah, good. :-) > You mean enough information about what? About the execution, to find out if it is...

I can see what you mean about being able to visualise a possibly better counterexample if you inspect the results (and hence possibly learn a bit more about the order)....