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
- add `--watch` flag
- start saving seeds in persistent storage
- make a separate version of execution functions that use `vector of interaction` instead of `InteractionPlan`
- 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
- 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
