diff --git a/tests/model_based.rs b/tests/model_based.rs index 8b62874..eed2d01 100644 --- a/tests/model_based.rs +++ b/tests/model_based.rs @@ -1,9 +1,6 @@ //! Model-based tests: traces generated from `spec/planner.qnt` are replayed //! against the Rust implementation, and both states are compared after each //! step. -//! -//! This file is the exercise of step 1: fill in every `TODO` below. -//! See `docs/tutorial.md` for what each of them is asking for. use itf::de::{self, As}; use quint_connect::{Config, Driver, Result, State, Step, quint_run, switch}; @@ -35,7 +32,9 @@ impl State for ModelState { let planner = &driver.planner; Ok(Self { start: planner.start(), - // TODO: read the three remaining values out of `planner`. + goal: planner.goal(), + obstacle: planner.obstacle(), + result: planner.result().clone(), }) } } @@ -50,10 +49,9 @@ impl Driver for PlannerDriver { type State = ModelState; fn config() -> Config { - // The whole state of the specification lives in a single variable. + // The whole state of the specification lives in the `state` variable. Config { - // TODO: name that variable. - state: &[""], + state: &["state"], ..Config::default() } } @@ -69,7 +67,8 @@ impl Driver for PlannerDriver { fn step(&mut self, step: &Step) -> Result { switch!(step { init(start, goal, obstacle, blocked) => self.set_inputs(start, goal, obstacle, blocked), - // TODO: add an arm for every other action the specification can take. + reset(start, goal, obstacle, blocked) => self.set_inputs(start, goal, obstacle, blocked), + computePlan => self.planner.compute_plan(), }) } } @@ -94,6 +93,7 @@ impl PlannerDriver { /// /// Failures report the seed the traces were generated from; set `QUINT_SEED` to /// that value to replay exactly the same ones. -// TODO: name the specification file. -#[quint_run(spec = "", max_samples = 100, max_steps = 20)] -// TODO: add the test function, which returns the driver to replay the traces through. +#[quint_run(spec = "spec/planner.qnt", max_samples = 100, max_steps = 20)] +fn planner_model_based_test() -> impl Driver { + PlannerDriver::default() +}