<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">On Mon, Dec 10, 2018 at 8:30 AM Frans Schneider <<a href="mailto:fchschneider@gmail.com">fchschneider@gmail.com</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi list,<br>
<br>
In PropER, I am looking for a way to generate records with one field <br>
being a sequence number which is incremented for each instance.<br>
<br></blockquote><div><br></div><div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">This is somewhat haphazard, you have been warned!</div><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">Some questions/initial guesses:</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* 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.<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* Use `erlang:unique_integer` to provide a unique integer for each run, and feed it into the cache?</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* It isn't entirely clear what a run means to you, and what property you are trying to epoch-test.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* If you have any kind of relations between commands toward your cache, you can look at stateful testing.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* By "not entirely clear" I mean that the lifetime needs of your SUT and your test generator isn't really known to us.<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">Some observations:<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* Observation: the seqno is "time". Time should often be injected.<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* 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.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* Your cache run can then assume that seqno.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* 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.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* 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.<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">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.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">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.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">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.<br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">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.<br></div><br></div></div>