[erlang-questions] PropER generator for list of records with a sequence number

[Jesper Louis Andersen]

On Mon, Dec 10, 2018 at 8:30 AM Frans Schneider <fchschneider@REDACTED>
wrote:

> Hi list,
>
> In PropER, I am looking for a way to generate records with one field
> being a sequence number which is incremented for each instance.
>
>
This is somewhat haphazard, you have been warned!

Some questions/initial guesses:

* If you run 100 proper tests, do you want the cache to be restarted 100
times, or just once? The former does not provide any kind of isolation
between runs, which is usually not what you want to do.
* Use `erlang:unique_integer` to provide a unique integer for each run, and
feed it into the cache?
* It isn't entirely clear what a run means to you, and what property you
are trying to epoch-test.
* If you have any kind of relations between commands toward your cache, you
can look at stateful testing.
* By "not entirely clear" I mean that the lifetime needs of your SUT and
your test generator isn't really known to us.

Some observations:

* Observation: the seqno is "time". Time should often be injected.
* Create your cache so you can start it with a given seqno. Feed this into
the cache by injecting it as a parameter when you start it.
* Your cache run can then assume that seqno.
* If you go for a stateful test, you can then write properties which
verifies the cache handles its seqno correctly, for all possible starting
seqno.
* Write a test where there is only a single key. Focus on the seqno since
that is highly likely to contain an error. Once you have this, extend your
model with multiple keys, but keep it low: 2 to 5 keys should be more than
enough to capture almost all kinds of errors in the system.

In a stateless model, the best you can do is generating random integers as
sequence numbers and verify the cache does the right thing given its
current state. Say it should ignore updates if a sequence number is too
low. Then if we start with a large integer in the sequence, then most runs
will just reject the input, as it should. In a stateful model, you can
track the state of the cache and then generate sequence_numbers with the
property they are monotonically increasing, which will make the system test
the "real code". A stateful model would also fault-inject once in a while
to test the case where the sequence number is too low.

One big advantage of the stateful model is precision: when failure occurs,
it knows the command sequence which made the failure occur, so it can often
point to the culprit by shrinking. A stateless model needs to search more
to find the problem. The disadvantage is that a stateful model requires
more work to implement and get right.

Personally, I'd just go with a stateful model immediately. Add a way to
query your cache for its current contents. Then you can write your update
commands such that they update, then query the cache state. This makes
postconditions/invariants easy to write for the system. Start with a single
command and work from there. As you add commands, you will start to find
the problems in the SUT. I.e., the first goal should be to initialize the
cache and then ask how large it is or something such. This should always be
0. Then stop the cache again. Next model could track if you updated a
single key in the cache or not. So the size is either 0 or 1, depending on
when that call happens. You can slowly extend the model from this simple
initial idea until you cover everything.

IF you want to go with a stateless model, generate a random list of
operations to run against the cache. Run these against the cache and
against a different local model you have. Then run an observation against
both and fail if they don't agree. This provides isolation from run to run
(your 100 test cases might run 10 cache operations each, roughly). However,
many operations will not have effect, and the observations will be weaker
than a stateful model, so you would have to do more runs before you hit a
problem.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20181210/1e60df3a/attachment.htm>