Commit Graph

9 Commits

Author SHA1 Message Date
alpaylan
c133bbdd29 add differential testing against rusqlite 2025-02-11 14:13:14 -05:00
alpaylan
6308ce4544 fix the shrinking file and poison errors 2025-02-08 09:34:51 -05:00
Pekka Enberg
0d0906dce4 Merge 'simulator: implement --load and --watch flags' from Alperen Keleş
The current status of the PR is halfway. The new framing of simulation
runner where `setup_simulation` is separated from `run_simulation`
allows for injecting custom plans easily. The PR is currently missing
the functionality to update the `SimulatorEnv` ad hoc from the plan, as
the environment tables were typically created during the planning phase.
The next steps will be to implement a function `fn
mk_env(InteractionPlan, SimulatorEnv) -> SimulatorEnv`, add `--load`
flag to the CLI for loading a serialized plan file, making a
corresponding environment and running the simulation.
We can optionally combine this with a `--save` option, in which we keep
a seed-vault as part of limbo simulator, corresponding each seed with
its generated plan and save the time to regenerate existing seeds by
just loading them into memory. I am curious to hear thoughts on this?
Would the maintainers be open to adding such a seed-vault? Do you think
the saved time would be worth the complexity of the approach?

Reviewed-by: Pere Diaz Bou <pere-altea@homail.com>

Closes #720
2025-01-26 08:52:58 +02:00
alpaylan
e476b9f697 implement watch mode
- add `--watch` flag
- start saving seeds in persistent storage
- make a separate version of execution functions that use `vector of interaction` instead of `InteractionPlan`
2025-01-18 23:54:03 +03:00
Jorge López
e5faa3273a syntactic changes: remove unused self dependency to appease to our Clippy overlord... 2025-01-18 19:36:32 +01:00
Jorge López
86a4714711 syntactic changes: remove unneeded paths when the type is already imported 2025-01-18 18:29:12 +01:00
alpaylan
28cde537a8 this commit;
- 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
2025-01-17 01:30:46 +03:00
alpaylan
fb937eff7b fix non-determinism bug arising from a call to thread_rng while picking
which row to check existence for in the result of the select query
2025-01-13 17:26:23 +03:00
alpaylan
191b586f05 this commit restructures the interaction generation in order to have
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
2025-01-11 02:20:22 +03:00