Commit Graph

56 Commits

Author SHA1 Message Date
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