Getting hold of the abstract state after generating commands

[m-alvarez]

I'm using quickcheck-state-machine to test a pure state machine living in the State monad (say, State s). Unfortunately, due to how the system works, for a certain family of tests, it is essentially impossible for me to give an abstract state without making it just as complex as the actual state, since I need detailed access to s to generate valid commands.

As inelegant as it is, I'm inclined to use the same type s for both abstract and concrete state, but this has the issue that the state machine will then be run twice in exactly the same way (and the cost of this is not entirely negligible). Ideally, I would just generate a list of commands and then inspect the resulting abstract state (or specify invariants directly on it). Is there a way to accomplish this with quickcheck-state-machine?

[stevana]

I'm not sure I understand fully what you want to do.

Do you mean something like:

helper :: (Model Symbolic -> Property)  -- ^ Predicate you want to hold on the model 
                                        -- after commands have been generated.
       -> Property
helper p = forAllCommands sm Nothing $ \cmds ->
  let model' = advanceModel sm initModel cmds
  p model' 

If not, perhaps you can provide a small example?

[m-alvarez]

Yes, this is exactly what I had in mind, but if I understand your code correctly there is still some redundancy since you execute the commands in cmds twice: once while they're being generated and a second time when advanceModel gets executed, correct?

More generally, what we have is a system like this (except significantly more complicated). For example, one would like to test the property that the total amount of money in a ledger is conserved after any sequence of transactions.

The problem I have is that my ledger isn't simply a Map but a blockchain and so generating valid state transitions ahead of time is basically impossible unless my abstract state is already essentially the entire system. Does this make sense?

[stevana]

Yes, this is exactly what I had in mind, but if I understand your code correctly there is still some redundancy since you execute the commands in cmds twice: once while they're being generated and a second time when advanceModel gets executed, correct?

Yes, this will traverse cmds twice. It doesn't execute the commands against the real system though, only goes through the list of commands and applies the transition function.

If you want to avoid this, you could define your own forAllCommands variant that takes a predicate Commands cmd resp -> model Symbolic -> prop and is defined in terms of a variant of generateCommands which uses runStateT rather than evalStateT.

The problem I have is that my ledger isn't simply a Map but a blockchain and so generating valid state transitions ahead of time is basically impossible unless my abstract state is already essentially the entire system. Does this make sense?

Usually the abstract state (or model) is a simplification of the real system, exactly because we want to avoid re-implementing the entire system (the specification must be simpler than the implementation, otherwise what's the point of the specification?).

I've not come across an example where one needs the full state of the system under test to generate valid programs before. I don't understand your problem domain well enough to tell if this really is the case in your example. If it really is, could you explain why that's the case?

[stevana]

Closing, feel free to reopen if you have any further questions.