bracketP doesn't work about quickcheck-state-machine HOT 8 CLOSED

Yeah, I recall that I couldn't get clean up to work properly, probably because of the reasons you explained. Thanks for looking into it.

I think both options might be desirable and it would be nice if we had an example of each approach. Perhaps CrudWebserverFile could be started and stopped each run, while the Db version spawned globally?

from quickcheck-state-machine.

It's a good idea to demonstrate both.

Now, it looks like the current specifications for these web servers cannot be parallelized. For instance, a simple counterexample for the File version is: in the prefix, create a file; in both suffixes, delete the file. Are the parallel properties expected to fail here, and if not, what would be a good fix?

from quickcheck-state-machine.

If we make the server implementation use removePathForcibly instead of removeFile then the fact that the file isn't there for second delete action doesn't matter. The post-condition just checks should work fine? Is there anything else that could go wrong?

By the way, this example was inspired by: https://github.com/Quviq/QuickCheckExamples/blob/master/src/crud_eqc.erl .

from quickcheck-state-machine.

There could be a concurrent GetFile and DeleteFile, so if DeleteFile execute first, GetFile will fail.

There are a few points I'd like to ask about in the testing process for parallel programs.

• It seems that linearization should allow traces where, for instance, we try to read a file we just deleted. In that case, we need to relax the precondition to allow reading non existent files, and the postcondition to allow returning errors. But even the Erlang example doesn't seem to do that. Am I missing something?
• Am I right in thinking that the generation process, reusing the sequential program generator, is meant to be heuristic: the generation of the two suffixes simulates two independent single-threaded models; we hope that makes them interesting enough, even though the models will not match the subsequent parallel execution?

from quickcheck-state-machine.

Ah yes, I now remember a discussion with @Danten where he raised a similar point about the Erlang example. I don't think we came to any satisfactory conclusion about how the Erlang version works. Do note that there is a bunch of read2_* things that are supposed to simulate failed reads. But I don't get how we can generate successful reads in the suffixes that we for sure know will succeed, because of the point you raised.

This leads to your second question. Perhaps the model should be shared when we generate the suffixes, and not independent like it is now? I don't think that makes sense though, because we don't know how the threads are scheduled or how long the operations take to execute.

I think instead what we need to do is to generalise histories. This is getting a bit off topic for this issue, so I'll create a new one.

from quickcheck-state-machine.

Thanks for your answer! I'll keep looking at the literature surrounding the topic and see whether anything interesting comes up.

from quickcheck-state-machine.

Started a bit on this in the bugfix/bracket branch.

from quickcheck-state-machine.

This issue regarding bracket was fixed in #166.

Let's continue the discussion about what to do when the semantics of actions fails in #162.

from quickcheck-state-machine.