Commit Graph

7 Commits

Author SHA1 Message Date
Jorge López
86a4714711 syntactic changes: remove unneeded paths when the type is already imported 2025-01-18 18:29:12 +01:00
alpaylan
c3ea02783d - add doc comments to generation traits and functions
- remove pick_index from places where it's possible to use pick instead
- allow multiple values to be inserted in the insert-select property
2025-01-13 15:56:10 +03:00
alpaylan
43f6c34408 fix arbitrary_from ergonomics by removing the implicit reference in the trait signature 2025-01-13 14:43:12 +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
alpaylan
58f23983e1 minor changes, add maximum time bound to the simulator, fix bug in the table create shadowing 2024-12-30 00:36:43 -05:00
alpaylan
d3fee3b331 add empty line at the end of cargo.toml, add create counts to the interaction stats, turn the percentages into f64 2024-12-29 14:00:57 -05:00
Pekka Enberg
13f229020e simulator: Use "mod.rs" for module top-level files
Let's use "mod.rs" for the module top-level file as we do in the rest of
the Limbo codebase for consistency.
2024-12-21 09:50:23 +02:00