Stateful generators and combinators

[alfert]

I would like to see more combinators to create more complex data, in particular a reducer to create data depending on the already generated elements.

Background:

The reducers could be a nice solution for generating command sequences to support symbolic state machines for property testing of stateful systems. Here we start with an initial state and generate commands depending on the current state and producing a new state. A reduce or unfold function could be a solution for that problem.

If this goes along your development direction of StreamData, I can work on PRs for that.

[josevalim]

@alfert this sounds very exciting but I am having some difficulty in seeing some of the use cases. Could you please expand on that area? Thank you!

[alfert]

@josevalim sure: property testing of stateful systems in Quickcheck, Proper, and others work with a state machine as the abstraction of the system under test (SUT) and a command generator, which generates a list of commands against the SUT. Pre- and postconditions on the state machine define valid command sequences, state transition of the state machine and connect SUT values with their state machine counter parts. There are two phases in stateful system testing: the first phase generate valid command sequences depending on the preconditions of the state machine, the second phase uses the generated command sequences and executes it against the SUT checking the postcondition of the state machine is the same as the results of the SUT. A failing property results in a shrinked command list to get the minimal sequence of commands that exhibit the error.

Use cases for this approach are property based testing of all kinds of stateful (sub) systems, such as GenServers, processes, but also data structures (see "breaking erlang maps" below). Another interesting approach is to run a long sequence of commands against a system, e.g. a sequence of 3.000 or more commands. These are tests which you would never write as a unit test and the property testing approach guarantees that each command execution sequence is different.

Some documentation and examples are here:

• https://medium.com/@jlouis666/breaking-erlang-maps-2-362730a91400
• http://propertesting.com/book_stateful_properties.html
• http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_generic_servers.html
• http://www.quviq.com/getting-better-statistics-from-state-machine-tests/
• https://fscheck.github.io/FsCheck/StatefulTesting.html

[josevalim]

Thanks @alfert. I thought you were hinting at something else when you said about relying on reduce. :) Do you have a proposal about the API? Maybe something you already leverage in propcheck?

[alfert]

@josevalim Depends on what kind of API you are thinking about.

For the property testing, I think about following either QuickCheck or PropEr closely - this is work in progress and will be the foundational API. To make the state machine definition easier, I would like to define a macro based DSL which shall be nicer and more idiomatic than QuickCheck's new state machine DSL (relying on function name postfixes and a parse transform).

Regarding the use of StreamData, I am in the state of an early implementation but hit a wall when realizing that the combinators have no state (i.e. map, bind and filter). Reduce is for me the essential combinator, where you can deal with state (or time - as in Elm's foldp). But thinking about the infinite streams in StreamState, an unfold might be even more helpful. The basic approach in pseudo code is:

def command_generator(initial_state, command_list) do
  unfold(initial_state, fn state -> 
   cmd = command_list 
   |> Enum.filter(& StateMachine.precondition(state, &1))
   |> one_of()
   new_state = StateMachine.transition(state, cmd)
  {new_state, cmd}
  end) 
end

Until now, I avoided a deep dive into the inner workings of the LazyTree. But if an unfold like in Streams can be defined on top of LazyTree, I assume a proper command generator where each new element depends on the elements generated before should be do-able.

The implementation in propcheck is mostly a layer on top of PropEr, so I cannot take any implementation with me, since the generation mechanism and the internal data structure are completely different compared to StreamData. PropEr is a complex Erlang library and its internals are not for the faint-hearted.

[josevalim]

This is ultimately @whatyouhide's call to make but maybe we could provide an unfold/reduce operation and leave the rest of the stateful generators up to libraries so we have a bit of experimentation before sticking with a final implementation.

I will also copy @fishcakez since I know he has some thoughts on the matter too.

[whatyouhide]

I think that we might be underestimating the changes that stateful generators would bring (or I didn't understand the scope of this discussion). Stateful generators were avoided from the start (after I tried really hard to make them work) because essentially

bind(gen1, fn term ->
  gen2
end)

invalidates the state of gen2 everytime we generate a new term from gen1. The only semi-solution I can see is to have a single generator that generates the next command and which is passed a list of previous commands (so that it can generate a valid command based on the previous ones). This would be a stateless generator.

Can you tell me if I'm on the right track and if what I'm proposing makes sense? Otherwise, how can we avoid the bind problem?

@josevalim how would unfold work?

[alfert]

I am currently working on a recursive translation of PropEr's command sequence generator. You more or less encouraged me to look more closely into their implementation, since they don't have such combinators. But I will progress slowly, since I can do this in my spare time only and weekend is over. I will come back to you, with either success or failure. So, do not invest too much time on this topic just to serve me.

[fishcakez]

I was able to get a statem generator working with an older version of this code, so it should still be possible. I haven't looked at the proper code but I used a body recursive call I think and shrinking worked okay. Unfortunately the laptop is in storage and I didn't take advantage of the distributed part of a DVCS.

I think that using a different DSL is a great idea, I was working on using native Elixir features to replace the awkward virtual state and to create a reproducible method that did not use seeds but generated test case files. Hopefully @alfert can make some progress as I doubt I will return to it any time soon.

[tmbb]

I have a question regarding stateful testing in general. As long as you're not messing with the scheduler, it's just a question of generating valid command sequences (according to the rules you give it) and executing them in order, right? Can't the stream_data generatos do it already? Or is there something I'm not seeing?

[fishcakez]

Yes, you can do it with the generator already, it doesn't require a change to stream_data On 20 Oct 2017 12:01, "tmbb" <[email protected]> wrote: I bave a question regarding stateful testing in general. As long as you're not messing with the scheduler, it's just a question of generating valid command sequences (according to the rules you give it) and executing them in order, right? Can't the stream_data generatos do it already? Or is there something I'm not seeing? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#51 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AB6JTWYcuHTotzQ-AjHmbap2dSeRA6_fks5suO4lgaJpZM4P5t3p> .

[alfert]

Back, after a long time....

I tried to translate the recursive command generators of proper, but I alway ran against the wall since list construction is not allowed by call (only atoms, tuples and StreamData structs). Interestingly the approach of @fishcakez in https://github.com/fishcakez/stream_code works, but to be honest I do not understand really what the difference is that makes it work.

I modified @fishcakez's approach such that it does not generate macro code but symbolic calls to come closer to the usual state-machine definition. Works nicely. But when I introduced failing properties to see how shrinking works, the generated list of commands did not shrink but only tried various elements in the list's head.

My next approach was to modify the list_of generator to allow for an accumulator and data generator working together with the accumulator, similar to Stream.unfold in its arguments. This works and I will publish a PR for that soon introducing an unfold function. It requires only a small modification of call_n_times and reuses everything else from list_of. With that in place, list_of itself can be expressed as the following

    def list_of(data, options \\ []) do
       unfold(nil, fn _ -> {nil, data} end, options)
    end 

[keathley]

I wanted to see if there was any progress that had been made on this issue and if I might be able to help contribute in any way. This is something that our team is very interested in since eqc is currently prohibitively expensive and Proper's licensing makes it a non-starter for our organization.

[alfert]

As a funny co-incidence of @keathley' new issue #94, I finally had a good idea to implement the PropEr API for stateful testing including shrinking on top of stream_data. You can find this in repo https://github.com/alfert/counter. I needed to copy some of the private functions of stream_data to make it work. I put it into a separate repo to research various strategies including some tests with demo systems and a comparison to PropEr's approach. We can later merge it into stream_data.