Kostas Dermentzis

@stevana, as another generalisation, I think the type of these threads could be extended. For example forking unbound vs bound threads could make a difference at the result, when testing...

I think asking for a user function to do the cleanup is a good idea. During execution we should be careful to evaluate everything with proper exception handles (similar to...

In the parallel case `executeCommands` is called with the `initModel` as intial state. Inside `executeCommands` there is no precondition check and the final Model (result of transition) is usually just...

I think it's the same problem. What you mention > pass in the model that's the result of executing the prefix can only work for the first suffix. Next suffixes...

Yes I don't think this will work either. Assume in `MemoryReference`, one threads runs `Increment ref` and the other `Write ref 2`. In the one Model the reference would become...

Indeed, I think `History` would also work and is a good idea. Building the general Model seems hard though.

`linearise` stops if there is no postcondition that can hold, so any references created after that will not be visible on the Model. Do you think we can overcome this?

Indeed, I wrote a function which does this and seems to work for my rqlite example. I was wondering though if it's too complicated for a recourse cleaning process. Do...

I agree that it's the users's responsibility to handle exceptions in the semantics. I have done exactly this with brackets at my rqlite tests https://github.com/advancedtelematic/quickcheck-state-machine/blob/rqlite/test/RQlite.hs#L359. About the type of the...

Also, the cleanup works when I ^C the tests. Although maybe I need to always mask async exceptions when I run the cleanup..