Canonical way of generating matrices

[wilf-phasecraft]

Hi there,

I'm new to PBT and Supposition.jl, so apologies if this is a bit of a simple question. Is there a canonical way of generating matrices for testing? I have found the Data.Vectors generator, but can't see anything analogous for generating a Matrix, and can't really see a simple way of generating a random (non-square) matrix through @composed.

I found this previous short discussion about Array generators, but I'm not looking to generate arrays with an arbitrary number of dimensions, just a 2D array where the two dimensions have arbitrary size.

[Seelengrab]

Hi! No worries, even simple questions can have surprisingly complex answers :) I hope this isn't overwhelming; there's quite a bit of depth to be explored here!

So, in principle generating any 2D array is simple: just generate any vector, reshape it into some generated size and you have a matrix. Unfortunately, there are at least three problems with this approach:

1. This doesn't shrink well, since the elements in the matrix end up "reflowing" across columns during shrinking. In essence this is because deleting a "row" doesn't actually delete the row, but as many elements from the end of the original vector as there are currently in a "column" (and vice versa). So a row/column in the "middle" of the matrix can't be deleted by this, which means a lot of edge cases are missed & shrinking stops progressing/simplifying the result much too soon, leading to really ugly matrices as a "minimal" counterexample.
2. The vast majority of matrices are (for lack of a better word) blobby. By this I mean that, looking at all possible matrix sizes from (1,1) to (m,n), very few look something like (m,1), (n,2)... and so on (and vice versa for m). Out of all possible sizes (m*n) only 4 are the "most extreme" cases, and only 2m/2n are the "edges" of all sizes. As m & n grow, those edge cases only get rarer and rarer as a fraction of all possible matrices. This is more or less the curse of dimensionality, but unlike in machine learning, you can already feel this kicking in with just 2 dimensions! Of course this gets even more extreme with higher dimensions, but luckily a solution for 2D should generalize to higher dimensions (I don't know which discussion you're referencing, but I'm pretty sure that's why that discussion talks about the general case). Generating a Matrix as described above doesn't solve this at all, and most matrices end up looking blobby.
3. Precisely because matrices grow like m*n in size, generating large matrices & testing with them slows testing down enormously. Generating Vectors is biased towards smaller ones for exactly this reason!

For testing purposes, most matrices that are of a similar shape are likely to behave mostly the same. It's the edge cases that are most interesting here, so it would be nicer to bias the generation process a bit to make those edge cases more likely, and in the limit perhaps even guarantee to hit the largest & smallest edge cases. At the same time, precisely because testing with large matrices necessarily takes longer, you also end up wanting to bias the generation towards smaller matrices, since it's generally unlikely that a given bug will only show up with huge matrices.

Fulfilling all of those criteria is a bit nontrivial to do - I do have an experiment on an old branch set up, which generates 2D matrices that look like so:

Apologies for the lack of labels, this is a graph I made for debugging purposes. The heatmap shows the sizes of various generated matrices that show up while a property is tested, while the bargraph shows how often that particular number of elements showed up in total (which is also important! 5x3 is the same as 3x5 in the amount of data, so making sure that this doesn't disadvantage the diagonal matters). The matrices here go from (30,20) to (90,80). This graph looks quite ok, but there are some bugs still left that I'd love to work out first, and unfortunately I've not been able to spend a bunch of time on this yet :/

[wilf-phasecraft]

Thanks for the incredibly detailed response, some of the problems you highlight are indeed ones I suspected might make this challenging - though you've certainly fleshed them out more formally than I had them in my head.

I guess my question is still somewhat unresolved in as much as given that I have a function that requires testing, and takes a BitMatrix as an input argument, how can I generate test matrices to input here, within some bounds.

My current solution looks something like this, does it seem reasonable?

intgen = Data.Integers(2, 16)
boolgen = Data.Booleans()
matgen = @composed function bitmatrix(ndim1=intgen, ndim2=intgen)
    return reshape(example(boolgen, ndim1*ndim2), ndim1, ndim2) |> BitVector
end

[Seelengrab]

My current solution looks something like this, does it seem reasonable?

Oh my, that's not how example is supposed to be used 😅 I'll amend the documentation,example is not supposed to be used inside of @composed, @check or similar. It's only for interactively inspecting what kind of stuff a Possibility generates, since it handles its own state internally that doesn't end up in the overall state handled by @check.

For example, with your matgen you'll get shrinks like this:

julia> @check db=false (m=matgen) -> begin
           (size(m, 1) < 4 && reject!())
           event!("size", size(m))
           !last(m)
       end
Found counterexample
  Context: ##SuppositionAnon#375

  Arguments:
      m::BitMatrix = Bool[1 1 0; 1 0 0; 0 1 0; 1 0 1]

  Events:
    size
        (4, 3)

julia> Bool[1 1 0; 1 0 0; 0 1 0; 1 0 1]
4×3 Matrix{Bool}:
 1  1  0
 1  0  0
 0  1  0
 1  0  1

which is contains a bunch of true values in places other than the last element. The data inside of the matrix hasn't shrunk at all, otherwise all elements (except for the last one) would be false!

For a simple version that's close to what you likely intended to write, take a look at this:

intgen = Data.Integers(2, 16)
boolgen = Data.Booleans()
matgen2 = map(intgen, intgen) do dim1, dim2
    len = dim1*dim2
    vec = produce!(Data.Vectors(boolgen; min_size=len, max_size=len))
    reshape(vec, (dim1, dim2)) |> BitMatrix
end

This will still shrink badly in some cases, like the one from above:

julia> @check db=false (m=matgen2) -> begin
           (size(m, 1) < 4 && reject!())
           event!("size", size(m))
           !last(m)
       end
Found counterexample
  Context: ##SuppositionAnon#1333

  Arguments:
      m::BitMatrix = Bool[0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 0; 0 0 1]

  Events:
    size
        (11, 3)

but at least the contents continue to shrink too. The minimal counterexample here is of size (4,2). This is exactly what a proper matrix generator can do a bit better (in that it is much more likely to get a minimal size), though even the one in my current experiments can't handle this properly, unfortunately. It's one of the bugs I mentioned above.

[wilf-phasecraft]

Ah, ok I'm not sure where I got the idea to use example thanks for the correction there. I think I understand the problem a little better now. I don't think I understand the shrinking process well enough to propose a solution, but I'd be interested to see the source code for the experimental version you've mentioned. Perhaps you could point me to the branch it's on?

[Seelengrab]

The main difference between the naive version and my experimental one is just some tricks to bias the size. Here's comparison of the naive version vs. the experimental one:

Unfortunately, adding this bias requires some changes to some more core functionality, so it's not as simple as just sharing the definition of the Possibility 😅 There's also some other problems, like it not always respecting the invariants about the size it should. There's some filtering for the plot going on. That being said, other than this bias (which is mostly just for speeding things up), the naive version should work. While the counterexample won't necessarily be minimal, it will still be a valid counterexample :)

[Seelengrab]

Actually, the bug I was talking about may have just been in the tests I was using for this 🤔 I'll run some more tests and get back to you!