simulator: add counterexample minimization #623
Conversation
…perations that did not reflect the internal structure, in which they were actually concatenations of properties, which are a coherent set of interactions that are meaningful by themselves. this commit introduces this semantic layer into the data model by turning interaction plans into a sequence of properties, which are a sequence of interactions
the execution of the current property and switches to the next one.
three indexes(connection, interaction pointer, and secondary pointer) that can uniquely identify the executed interaction at any point. we will use the history for shrinking purposes.
|
This looks quite cool @alpaylan. Could you post some literature you think is relevant for this? |
Thanks @pereman2 ! Of course, here are some rather informal writing discussing different shrinking strategies(warning: they're quite opinionated with respect to author's position, which I don't agree)
Two other informal articles, ECOOP20 paper from the hypothesis author, I view shrinking very related to delta debugging, which I think is a lot more used in the literature. I have a submission that discusses shrinking too, I'm not sure if sharing it here breaks double blind, but I can send it over email if you would like. |
|
I thought this page had a nice layman definition for shrinking:
We could even add it to our code |
|
The shrinking is a bit harder than I hoped for, particularly due to the fact that we cannot shrink closures, which limits our ability to minimize aggressively by removing columns from tables, because we wouldn't be able to modify the assertion that checks it. The solution is to turn the assertions themselves into a small DSL, but at that point it goes into too much research, which I don't think is the right choice for now. I've instead focused on other shrinking mechanisms;
|
better counterexample minimization. - it separates interaction plans from their state of execution - it removes closures from the property definitions, encoding properties as an enum variant, and deriving the closures from the variants. - it adds some naive counterexample minimization capabilities to the Limbo simulator and reduces the plan sizes considerably. - it makes small changes to various points of the simulator for better error reporting, enhancing code readability, small fixes to handle previously missed cases
|
Oh no. How do I fix that.(I accidentally pushed the extra commits I hadn't pulled on top of mine, fixed it now) |
- previous query generation method was faulty, producing wrong assertions - this commit adds a new arbitrary_from implementation for predicates - new implementation takes a table and a row, and produces a predicate that would evaluate to true for the row this commit makes small changes to the main for increasing readability
…he trait signature
|
This has been going good, there's some more extra work;
I propose we split the PR into two parts, finish the first part here, move the second part to another PR.
The reason for the split is that I feel like this is gonna stale if I try to finish everything on the list, and I think implementers would probably benefit from the improved testing experience this PR has enabled so far. What do you think @jussisaurio @pereman2 ? edit: moved value shrinkage to the next work package, it's hard to do it without progressive shrinking, and we might even need further improvements to the system. |
- remove pick_index from places where it's possible to use pick instead - allow multiple values to be inserted in the insert-select property
…king which row to check existence for in the result of the select query
alpaylan
force-pushed
the
main
branch
2 times, most recently
from
fcdfb27 to
6f27442
Compare
This PR introduces counterexample minimization(shrinking) in the simulator. It will require changes to the current structure in various places, so I've opened it as a draft PR for now, in order to not overwhelm the reviewers all at once.