Klaus Alfert

@flyingmutant very good points, thread safety was not on my checkmark. That happens if you are for a long time in the Erlang/Elixir world :-) I really like the idea...

@flyingmutant Next round, but there is more to be done. What I did: - statistics are printed automatically for a property, if events are send - event collection is done...

Thanks, to do the printing after calling Check is indeed a good idea. The use case for such reporting is important when you define your own generators. How do you...

Since we are close to Hypothesis and do not have the FP restrictions (and abilities), I would suggest to model it generally after Hypothesis. In my simple implementation, I added...

What I like in @josevalim's last example is the combination of executing the command, checking the postcondition via `assert` and returning a probably modified state. We do not need to...

> Apologies but I don't see how this is not possible with the proposal so far. In the proposal, the goal was to embed the working command call and next...

> From my understanding - and please keep in mind that I understand very little about stateful models - this implies we first generate the commands and apply them only...

> @josevalim Do you think checking for preconditions is a property of the model or of the SUT? Checking the precondition is required during the generation phase to generate useful...

Ah, I see your point. It is different: during generation you simulate the calls to the system, but you use next_state to record the expected state. In next_state you cannot...

I just finished a first version of an EQC like grouping with lots of debug output in Repo https://github.com/alfert/counter: * stateful property testing implementation https://github.com/alfert/counter/blob/master/lib/statem.ex * the system under test...