Struct Config 

pub struct Config {
    pub state: Path,
    pub nondet: Path,
}

Configuration for a Driver that specifies where to find state and nondeterministic picks within a Quint specification.

By default, both paths are empty (&[]). Empty paths indicate that:

• State is extracted from the top level of the specification’s state space
• Nondeterministic picks are extracted from Quint’s builtin mbt::actionTaken and mbt::nondetPicks variables

Override these paths when your specification nests the relevant state within a larger structure, or when tracking nondeterminism manually rather than using Quint’s builtin variables.

Examples

Specifying custom paths for nested state:

use quint_connect::{Driver, Config};

impl Driver for MyDriver {
    type State = MyState;

    fn config() -> Config {
        Config {
            state: &["global_var", "nested_record", "my_state"],
            nondet: &["global_var", "nondet_choices"],
        }
    }

    fn step(&mut self, step: &Step) -> Result {
        // ...
    }
}

Fields

state: Path

Path to the state within the Quint specification’s state space.

An empty path (&[]) indicates the state is at the top level.

nondet: Path

Path to nondeterministic picks within the Quint specification’s state space.

An empty path (&[]) uses Quint’s builtin mbt::actionTaken and mbt::nondetPicks variables.

Trait Implementations

impl Default for Config

fn default() -> Config

Returns the “default value” for a type.