Skip to main content

explore

Function explore 

Source
pub fn explore<F: Frontend>(frontend: &F, base: &F::Seed, opts: &Opts) -> Report
Expand description

Explore the frontend’s entry point from base inside the budgets.

The loop is the DART/CUTE shape: run, replay the path symbolically, pose a flip query at every decision (deepest first), apply a model, re-run, verify. A verified flip pushes the child path onto the frontier; the frontier emptying inside the budgets sets exhausted.