- makes interaction plans serializable
- fixes the shadowing bug where non-created tables were assumed to be created in the shadow tables map
- makes small changes to make clippy happy
- reorganizes simulation running flow to remove unnecessary plan regenerations while shrinking and double checking
...it is totally fine for a SQL query to fail as part of the simulation.
For example, if we attempt to create a table that already exists, the
expectation is that the query fails. No need to spam the logs.
- 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
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
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.
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 name "row result" is confusing because it really *is* a result from
a step() call. The only difference is how a row is represented as we
return from VDBE or from a statement.
Therefore, rename RowResult to StepResult.
This pr adds support for multiple readers and a single writer with a
custom made lock called `LimboRwLock`. Basically there are 5 allowed
read locks which store the max frame allowed in that "snapshot" and any
reader will try to acquire the biggest one possible. Writer will just
try to lock the `write_lock` and if not successful, it will return busy.
The only checkpoint mode supported for now is `PASSIVE` but it should be
trivial to add more modes.
This needs testing, but I will do it in another PR. I just wanted to do
it in another PR.
Closes#544
