What should mock be used for

[akegalj]

I am not sure what should be mock , last parammeter to StateMachine be used for and how it is used in a current implementation?

This line is onpar with my understanding https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/Echo.hs#L146

Also I can't deduce why mock would be needed from readme section on hackage:

Sequential property
The sequential property checks if the model is consistent with respect to the semantics. The way this is done is:

generate a list of actions;

starting from the initial model, for each action do the the following:

check that the pre-condition holds;
if so, execute the action using the semantics;
check if the the post-condition holds;
advance the model using the transition function.
If something goes wrong, shrink the initial list of actions and present a minimal counterexample.

Parallel property
The parallel property checks if parallel execution of the semantics can be explained in terms of the sequential model. This is useful for trying to find race conditions -- which normally can be tricky to test for. It works as follows:

generate a list of actions that will act as a sequential prefix for the parallel program (think of this as an initialisation bit that setups up some state);

generate two lists of actions that will act as parallel suffixes;

execute the prefix sequentially;

execute the suffixes in parallel and gather the a trace (or history) of invocations and responses of each action;

try to find a possible sequential interleaving of action invocations and responses that respects the post-conditions.

The last step basically tries to find a linearisation of calls that could have happend on a single thread.

[stevana]

The way mock should be used is that it should return a mocked response to each
command using values from the model, e.g. Read from the README looks up the
value associated to the reference we are trying to read from in the model. If a
command returns References, e.g. Create from the README, then genSym
should be used to create those (Symbolic) References.

Why mock is needed is more complicated.

Most importantly, is that it solves the problem of allowing more than one
Reference in a response. It's a hack however and I wish I could find a better
solution.

Another reason for not removing it is, because I've also played around with the
idea of using mock to create mocked APIs. I've still not worked out the
details of how exactly this should work though. (Because this isn't actually
used by the library yet, it's not important for mock to return the correct
responses, e.g. having mock for Read return ReadValue 0 is completely
fine.)

Does that make sense?

I'll update the README to include more info about mock while I keep thinking
of how to get rid of it or actually use it for something meaningful...

[akegalj]

Most importantly, is that it solves the problem of allowing more than one
Reference in a response. It's a hack however and I wish I could find a better
solution.

I have seen internal implementation and noticed some state counter, so I guess this is what you are saying here

Another reason for not removing it is, because I've also played around with the
idea of using mock to create mocked APIs. I've still not worked out the
details of how exactly this should work though.

Esentially you are saying that mock is not quite operational yet - but there is a plan to use it in some future version (so you are trying to be backward compatible as much as possible)

(Because this isn't actually
used by the library yet, it's not important for mock to return the correct
responses, e.g. having mock for Read return ReadValue 0 is completely
fine.)

ok - this is where you answered it :) . Yes, I figured that out by trying to modify TicketDispenser mock function from something that makes sense https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/TicketDispenser.hs#L161 into something that doesn't:

mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
-- mock (Model Nothing)  TakeTicket = error "mock: TakeTicket"
-- mock (Model (Just n)) TakeTicket = GotTicket <$> pure n
mock _                _      = pure ResetOk

but it produced correct output (test passed) in both cases. That's when I figured my understanding about this feature is still vauge but I see it is still WIP

Does that make sense?

it does - thanks <3

I'll update the README to include more info about mock while I keep thinking
of how to get rid of it or actually use it for something meaningful...

why I was confused about mock is that we can't really correctly map more complex systems (we can - but with huge effort). For example TicketDispenser is a small enough system where we can easily mock (in fact we can almost correctly capture its semantics with mock). In English mock is defined as "not real but appearing or pretending to be exactly like something" - in other words my understanding of mock function is that given model and action it shoud approximately give a response. But lets imagine that we are testing some IO action that might fail like reading a file:

data Action r = ReadFileA

data Response r = ReadFileR (Either SomeError Text)

data Model r = Model Text

I am not sure how I could mock up all errors that can happen. Do I have to mock up all cases

mock :: Model Symbolic -> Action Symbolic -> GenSym (Symbolic Response)
-- non happy path
mock model ReadFileA = 
  -- somehow figure out how all error cases can happen and model all of them.
  -- what if we leave out some error case?
  -- maybe IO error happens depending on some OS internals. Do I have to capture that?
  return $ ReadFileR $ Left $ ...
-- happy path
mock (Model t) ReadFileA = return $ ReadFileR $ Right t

(the above won't compile but I guess you see where I am aiming at)

or would it be sufficient to mock only happy paths (which seems viable):

mock :: Model Symbolic -> Action Symbolic -> GenSym (Symbolic Response)
mock (Model t) ReadFileA = return $ ReadFileR t

?

This is a toy example, but its motivated by my real life example where https://github.com/input-output-hk/cardano-sl/pull/3772/files#diff-3b681d025c5691ef4161a3e2d29ebea3R69 we are modeling some action, wallet creation by CreateWalletR (Either WL.CreateWalletError V1.Wallet) and wallet creation can fail in various ways (multiple wrong paths that can trigger Left). I wonder is mock intended to mock up all those wrong paths?

Or more complex example is testing a black box system like John Hughes testing dropbox https://www.youtube.com/watch?v=H18vxq-VsCk . I am not sure he would be able to find all wrong paths (not even all happy paths) with a black box approach.

I hope you see where my confusion is comming from: mock all paths or only "simple" paths :)

[stevana]

but it produced correct output (test passed) in both cases. That's when I figured my understanding about this feature is still vauge but I see it is still WIP

When I said:

(Because this isn't actually
used by the library yet, it's not important for mock to return the correct
responses, e.g. having mock for Read return ReadValue 0 is completely
fine.)

I should have added that the only important part is that Reference responses are generated by genSyms, because that is what increases the state counter that you mentioned in the beginning which is used for generating commands...

I'll make sure to mention both these things when I update the README!

Regarding how to mock more complex systems: we can't really answer this question until we actually know how to use mock for mocking APIs and how we intend to use those mocked APIs...

Perhaps only happy path is enough? Perhaps there should be fault injection commands which steer the unhappy paths? I don't know yet... But for now, while mock is only used for genSyming references, it doesn't really matter.

If you have any ideas on the topic, I'm all ears, :-).

[akegalj]

Thanks for prompt replays.

I will have to dive deeper into implementation details to capture full understanding of underlying mechanics. There is also mention of few papers in README that I'll have to read to get a full picture (hopefully by end of the year!). Will give my feadback eventually (based on our use case)

[stevana]

Feel free to ask questions or open further issues if there's something you'd like explained better in the documentation! I'm happy to explain things further, especially during working hours :-).

Also, I'm looking forward to hear your feedback!