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

[Frans Schneider]

Thanks guys for the suggestions.
I guess I'll have to add some extra code for starting and stopping the 
cache and generating the cache changes that PropER can use. I don't want 
to make changes to the application's code base to facilitate testing 
because that would give to much clutter.
I'll also go for the stateful approach as suggested.
PropER is great, but it takes some time to get used to it...

Frans


On 12/10/18 12:18 PM, Jesper Louis Andersen wrote:
> On Mon, Dec 10, 2018 at 8:30 AM Frans Schneider <fchschneider@REDACTED 
> <mailto: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.
>