model_based.rs

//! Model-based tests: traces generated from `spec/planner.qnt` are replayed
//! against the Rust implementation, and both states are compared after each
//! step.

use itf::de::{self, As};
use quint_connect::{Config, Driver, Result, State, Step, quint_run, switch};
use quint_connect_tutorial::{PlanResult, Planner, Position};
use serde::Deserialize;

/// The specification state, i.e. the `PlannerState` record held by the `state`
/// variable of the Quint module.
///
/// `Position` and `PlanResult` already deserialize from the representation
/// Quint uses for them; only `Option` needs a helper, as Quint encodes it as a
/// sum type rather than as a nullable value.
#[derive(Debug, Clone, PartialEq, Eq, Deserialize)]
struct ModelState {
    start: Position,
    goal: Position,
    #[serde(with = "As::<de::Option::<_>>")]
    obstacle: Option<Position>,
    result: PlanResult,
}

impl State<PlannerDriver> for ModelState {
    /// Reads the state to compare out of the implementation.
    ///
    /// This is the oracle of the test: after every step, Quint Connect calls
    /// this, deserializes the state the trace recorded at that point, and fails
    /// the test if the two differ.
    fn from_driver(driver: &PlannerDriver) -> Result<Self> {
        let planner = &driver.planner;
        Ok(Self {
            start: planner.start(),
            goal: planner.goal(),
            obstacle: planner.obstacle(),
            result: planner.result().clone(),
        })
    }
}

/// The implementation under test.
#[derive(Default)]
struct PlannerDriver {
    planner: Planner,
}

impl Driver for PlannerDriver {
    type State = ModelState;

    fn config() -> Config {
        // The whole state of the specification lives in the `state` variable.
        Config {
            state: &["state"],
            ..Config::default()
        }
    }

    /// Replays one step of a trace against the implementation.
    ///
    /// `switch!` matches the action the specification took and hands over the
    /// values it chose nondeterministically, so the patterns must spell the
    /// action and `nondet` names of `spec/planner.qnt` exactly.
    ///
    /// One driver replays every trace, so `init` has to overwrite the whole
    /// state rather than assume a fresh one.
    fn step(&mut self, step: &Step) -> Result {
        switch!(step {
            init(start, goal, obstacle, blocked) => self.set_inputs(start, goal, obstacle, blocked),
            reset(start, goal, obstacle, blocked) => self.set_inputs(start, goal, obstacle, blocked),
            computePlan => self.planner.compute_plan(),
        })
    }
}

impl PlannerDriver {
    /// Applies the inputs the specification has chosen, as its `setInputs`
    /// action does, which is why `init` and `reset` map to the same call here.
    ///
    /// The specification picks an obstacle position together with a flag
    /// telling whether it is blocked, so `obstacle` here is a plain position.
    fn set_inputs(&mut self, start: Position, goal: Position, obstacle: Position, blocked: bool) {
        self.planner.reset(start, goal, blocked.then_some(obstacle));
    }
}

/// The model-based test itself.
///
/// The attribute runs the Quint CLI to simulate the specification, which yields
/// `max_samples` traces of up to `max_steps` steps, then replays every step of
/// every trace through the driver returned here, comparing the two states after
/// each one. A single `cargo test` case therefore covers 100 traces.
///
/// Failures report the seed the traces were generated from; set `QUINT_SEED` to
/// that value to replay exactly the same ones.
#[quint_run(spec = "spec/planner.qnt", max_samples = 100, max_steps = 20)]
fn planner_model_based_test() -> impl Driver {
    PlannerDriver::default()
}