Struct ConfigBuilder 

pub struct ConfigBuilder(/* private fields */);

Builds a Config struct.

Implementations

impl ConfigBuilder

pub fn new() -> Self

pub fn with_stack_size(self, s: usize) -> Self

Specifies the default stack size for user threads

pub fn with_progress_report(self, n: usize) -> Self

Prints a progress report message after every “n” executions. This is useful, when you are waiting for models with large numbers of executions.

Note that if you do not specify this option, you will get the default behavior, an adaptive progress report that prints after 1, 2, 3, …, 10, 20, 30, … 100, 200, 300, etc.

To completely disable such output, use with_progress_report(u32::MAX)

pub fn with_thread_threshold(self, s: u32) -> Self

Specifies the thread size above which TraceForge warns for infinite executions. That is, if a thread has more than s many events, a warning is printed on the console

pub fn with_warnings_as_errors(self, b: bool) -> Self

Whether to treat warnings as actual errors

pub fn with_keep_going_after_error(self, b: bool) -> Self

Allow the exploration to continue even after an assertion violation has been discovered. Works only with traceforge::asserts since unlike std::assert, it does not panic

pub fn with_cons_type(self, t: ConsType) -> Self

Specifies the consistency model for TraceForge

pub fn with_policy(self, p: SchedulePolicy) -> Self

Specifies the scheduling policy for TraceForge

pub fn with_max_iterations(self, n: u64) -> Self

Specifies an upper bound on the number of iterations

pub fn with_verbose(self, v: usize) -> Self

Controls how much input is printed in stdout 0 = default, sparse information 1 = more information, and print the execution graph every time it’s blocked. 2 = even more information, and also print the graph of every execution, whether blocked or not.

Note that you can ALSO get more information by increasing the log level by initializing the standard Rust logging.

pub fn with_seed(self, s: u64) -> Self

Seeds TraceForge’s random number gneerator. Has no effect without [SchedulePolicy::Random] being the selected scheduling policy.

pub fn with_symmetry(self, s: bool) -> Self

Enables symmetry reduction

pub fn with_value(self, _s: bool) -> Self

Enables value reduction

pub fn with_lossy(self, budget: usize) -> Self

Consider executions where up to budget lossy messages are dropped.

pub fn with_dot_out(self, filename: &str) -> Self

Whenever the execution graph is printed, the same information will be written to this file in DOT format.

Note that this is not printed when a counterexample is generated.

See with_verbose() for more information

pub fn with_trace_out(self, filename: &str) -> Self

Whenever the execution graph is printed, the same information will be written to this file in text format.

Note that this is not printed when a counterexample is generated.

See with_verbose() for more information

pub fn with_turmoil_trace_out(self, filename: &str) -> Self

Enables trace printing that can be read by turmoil in addition to console printing

pub fn with_error_trace(self, filename: &str) -> Self

If a counterexample is detected, a trace will be written to this file. This trace will allow you to replay the execution if you call replay(must_program, “/path/to/error/trace”). “must_program” must be the same function/closure that generated the counterexample.

pub fn with_parallel(self, use_parallel: bool) -> Self

Enables parallel processing of model. By default the number of system cores is chosen as for the max worker count unless .with_parallel_workers() explicitly sets a value or env var MUST_PARALLEL_WORKERS is set.

pub fn with_parallel_workers(self, max_workers: usize) -> Self

Sets the max number of parallel workers. None implies using using the number of available cores in the system unless overridden by env var MUST_PARALLEL_WORKERS. Requires that .with_parallel(true) is also set.

pub fn with_callback(self, cb: Box<dyn ExecutionObserver + Send>) -> Self

Registers a callback that is called at the end of an execution by the model checker

pub fn with_keep_per_execution_coverage(self, keep: bool) -> Self

Enables storing per-execution coverage data across all executions. When disabled (default), only the aggregate coverage and current execution coverage (for ExecutionObserver callbacks) are kept, significantly reducing memory usage. Enable this only if you need to query coverage for specific past executions.

pub fn with_predetermined_choices( self, choices: HashMap<String, Vec<Vec<bool>>>, ) -> Self

Sets predetermined values for named nondeterministic choices.

The map keys are choice names, and values are 2D vectors where:

• First dimension: thread index (0 = first thread to call this choice, 1 = second, etc.)
• Second dimension: occurrence within that thread (0 = first call, 1 = second, etc.)

If a choice is not found in the map, or if indices are out of bounds, the choice falls back to normal nondeterministic exploration.

Example:

let mut choices = HashMap::new();
choices.insert("my_choice".to_string(), vec![
    vec![true, false, true],  // Thread 0: 1st=true, 2nd=false, 3rd=true
    vec![false, false],        // Thread 1: 1st=false, 2nd=false
]);
Config::builder().with_predetermined_choices(choices).build()

pub fn build(self) -> Config

Consumes the builder and produces the Config

Trait Implementations

impl Default for ConfigBuilder

fn default() -> Self

Returns the “default value” for a type.