Commit graph

8 commits

Author SHA1 Message Date
pedrocarlo
4a13286d62 modify clock to use simulated time instead 2025-07-17 12:24:43 -03:00
alpaylan
489602b095 updates to the oracle implementations for differential and doublecheck, add integrity check to the end of the simulation, run cargo clippy --fix 2025-07-11 01:22:40 -04:00
alpaylan
64c2917e81 add bug base, refactor 2025-04-08 17:48:16 -04:00
alpaylan
c133bbdd29 add differential testing against rusqlite 2025-02-11 14:13:14 -05: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
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
PThorpe92
f6cd707544
Add clippy CI, fix or ignore warnings where appropriate 2024-12-29 10:25:41 -05:00
alpaylan
2186b3973b change the name of the simulator submodule into runner 2024-12-23 16:16:39 -05:00
Renamed from simulator/simulator/mod.rs (Browse further)