From a70c72c418e3cfed8cde8b49d3e8703385ea6490 Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Sat, 6 Jun 2026 19:42:41 +0200 Subject: [PATCH 01/26] Feature-gate frontends Signed-off-by: Enrico Ghiorzi --- Cargo.lock | 16 ++++++++-------- Cargo.toml | 12 +++++++++--- src/lib.rs | 14 +++++++++++++- 3 files changed, 30 insertions(+), 12 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fea7518..ce4133d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -155,9 +155,9 @@ dependencies = [ [[package]] name = "bitflags" -version = "2.11.1" +version = "2.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" +checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8" [[package]] name = "boa_ast" @@ -929,9 +929,9 @@ checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0" [[package]] name = "log" -version = "0.4.30" +version = "0.4.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "616ec5685824bcc94416c6d4a7a446eea774a31efd7062c8480ba6fd06d7a6e5" +checksum = "953f07c43838f8e6f9758cab68bf5bed85465e7587ebe0b823f1bcd81978ad3a" [[package]] name = "logos" @@ -1809,9 +1809,9 @@ checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" [[package]] name = "unicode-segmentation" -version = "1.13.2" +version = "1.13.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9629274872b2bfaf8d66f5f15725007f635594914870f65218920345aa11aa8c" +checksum = "c6f5d3c3b1bf09027a88a6bc961fc00497d651009560b5463668dc81b0fa87a8" [[package]] name = "unicode-width" @@ -2264,9 +2264,9 @@ checksum = "1ffae5123b2d3fc086436f8834ae3ab053a283cfac8fe0a0b8eaae044768a4c4" [[package]] name = "yoke" -version = "0.8.2" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "abe8c5fda708d9ca3df187cae8bfb9ceda00dd96231bed36e445a1a48e66f9ca" +checksum = "709fe23a0424b6a435d82152b1bd3fdfb0833487d5fa90d05d42762a9891fef5" dependencies = [ "stable_deref_trait", "yoke-derive", diff --git a/Cargo.toml b/Cargo.toml index 98587f3..dfff3b2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -18,6 +18,12 @@ categories = [ ] exclude = ["scan_book/*", ".github/*"] +[features] +default = ["scxml", "jani"] +scxml = ["dep:smc_scan_scxml"] +jani = ["dep:smc_scan_jani"] +promela = ["dep:smc_scan_promela"] + [lib] name = "scan" # The name of the target. crate-type = ["lib"] # The crate types to generate. @@ -58,8 +64,8 @@ human-panic = "2.0.8" indicatif = { version = "0.18.4", features = ["improved_unicode"] } log = { workspace = true } smc_scan_core = { version = "0.2.0", path = "scan_core" } -smc_scan_jani = { version = "0.2.0", path = "scan_jani" } -smc_scan_scxml = { version = "0.3.0", path = "scan_scxml" } -smc_scan_promela = { version = "0.2.0", path = "scan_promela" } +smc_scan_jani = { version = "0.2.0", path = "scan_jani", optional = true } +smc_scan_scxml = { version = "0.3.0", path = "scan_scxml", optional = true } +smc_scan_promela = { version = "0.2.0", path = "scan_promela", optional = true } serde = { workspace = true } serde_json = { workspace = true } diff --git a/src/lib.rs b/src/lib.rs index 942db32..dc51050 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -51,6 +51,7 @@ enum Format { /// if present, or the path of a directory. /// In the latter case, SCAN will attempt to process appropriately /// all files in the given directory and its sub-directories. + #[cfg(feature = "scxml")] Scxml, /// JANI format, passed as the path to the .jani file. /// @@ -59,6 +60,7 @@ enum Format { /// The model has to be passed to SCAN as the path to the .jani file. /// /// WARNING: JANI support is still experimental. + #[cfg(feature = "jani")] Jani, /// Promela format, passed as the path to the .pml or .prm file. /// @@ -67,6 +69,7 @@ enum Format { /// The model has to be passed to SCAN as the path to the .pml or .prm file. /// /// WARNING: Promela support is still experimental. + #[cfg(feature = "promela")] Promela, } @@ -174,9 +177,12 @@ impl Cli { if let Some(format) = self.format { match format { + #[cfg(feature = "scxml")] Format::Scxml => self.run_scxml(&model), - Format::Promela => self.run_promela(&model), + #[cfg(feature = "jani")] Format::Jani => self.run_jani(&model), + #[cfg(feature = "promela")] + Format::Promela => self.run_promela(&model), } } else if self.model.is_dir() { self.run_scxml(&model) @@ -189,14 +195,18 @@ impl Cli { .to_str() .ok_or(anyhow!("file extension not recognized"))? { + #[cfg(feature = "scxml")] "xml" | "scxml" => self.run_scxml(&model), + #[cfg(feature = "jani")] "jani" => self.run_jani(&model), + #[cfg(feature = "promela")] "pml" | "prm" => self.run_promela(&model), _ => bail!("unsupported file format"), } } } + #[cfg(feature = "scxml")] fn run_scxml(self, model: &str) -> anyhow::Result<()> { use scan_scxml::*; @@ -231,6 +241,7 @@ impl Cli { Ok(()) } + #[cfg(feature = "jani")] fn run_jani(self, model: &str) -> anyhow::Result<()> { use scan_jani::*; @@ -263,6 +274,7 @@ impl Cli { Ok(()) } + #[cfg(feature = "promela")] fn run_promela(self, model: &str) -> anyhow::Result<()> { use scan_promela::*; From 0a2e84d96ce8706f3973fd519d609f1fb2804ee7 Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Mon, 8 Jun 2026 17:02:34 +0200 Subject: [PATCH 02/26] Add section on features to installation docs Signed-off-by: Enrico Ghiorzi --- README.md | 40 +++++++++++++++++++++++++++++---- scan_book/src/manual/install.md | 40 +++++++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 46f135b..3d79eb8 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,8 @@ API docs for the library crates: - [`smc_scan_scxml`](https://docs.rs/smc_scan_scxml/latest/scan_scxml/) - [`smc_scan_jani`](https://docs.rs/smc_scan_jani/latest/scan_jani/) - [`smc_scan_promela`](https://docs.rs/smc_scan_promela/latest/scan_promela/) +- [`smc_scan_pmtl`](https://docs.rs/smc_scan_pmtl/latest/scan_pmtl/) +- [`smc_scan_mtl`](https://docs.rs/smc_scan_mtl/latest/scan_mtl/) - [`smc_scan`](https://docs.rs/smc_scan/latest/scan/) ## Formalism @@ -35,7 +37,11 @@ At the moment the following languages are planned or (partially) implemented: - [ ] [Promela](https://spinroot.com/spin/Man/Manual.html) - [x] [JANI](https://jani-spec.org/) -## Build prerequisites +## Installation + +Currently, the only way to obtain SCAN is to build it from sources. + +### Build prerequisites SCAN is entirely written in [Rust](https://www.rust-lang.org/), so, to build it, you need to install a recent version of the Rust toolchain. @@ -43,9 +49,7 @@ The easiest and recommended way to do so is by installing [rustup](https://rustu either following the instructions on its homepage or through your OS's package manager. Do not forget to set your `PATH` correctly, if required. -## Installation and usage - -Currently, the only way to use SCAN is to build it from sources. +### Installing with Cargo To install and use SCAN on your system, the easiest way is to use the `cargo install` command. @@ -75,6 +79,34 @@ cargo install --git https://github.com/convince-project/scan (see `cargo install --help` for more options). +### Features + +By default, SCAN includes the SCXML and JANI frontends, +while the Promela frontend is disabled through the use of [Cargo features](https://doc.rust-lang.org/cargo/reference/features.html). +The available features for SCAN are: + +- `scxml` to include the SCXML frontend (included by default); +- `jani` to include the JANI frontend (included by default); +- `promela` to include the Promela frontend (disabled by default); + +To change which frontends to include at build time, +explicitly select the desired features with the `--features` option as follows: + +```console +cargo install smc_scan --locked --features FEATURES +``` + +where `FEATURES` is a (comma-separated, or space-separated inside quotes) list. +Alternatively, if you want all available features, install SCAN with: + +```console +cargo install smc_scan --locked --all-features +``` + +Be aware that each feature imports extra dependencies and increases build time. + +## Usage + After installation, SCAN can be used as a CLI tool. To print the help screen, use diff --git a/scan_book/src/manual/install.md b/scan_book/src/manual/install.md index 4c6bb7b..3c537a3 100644 --- a/scan_book/src/manual/install.md +++ b/scan_book/src/manual/install.md @@ -1,5 +1,7 @@ # Installation +Currently, the only way to obtain SCAN is to build it from sources. + ## Build prerequisites SCAN is entirely written in [Rust](https://www.rust-lang.org/), @@ -34,3 +36,41 @@ scan to verify that the installation completed successfully by displaying the in-line help. + +To install a specific SCAN version, e.g., v0.1.0, use: + +```console +cargo install smc_scan --version 0.1.0 --locked +``` + +It is also possible to install SCAN from the latest commit directly from this repository with: + +```console +cargo install --git https://github.com/convince-project/scan +``` + +## Features + +By default, SCAN includes the SCXML and JANI frontends, +while the Promela frontend is disabled through the use of [Cargo features](https://doc.rust-lang.org/cargo/reference/features.html). +The available features for SCAN are: + +- `scxml` to include the SCXML frontend (enabled by default); +- `jani` to include the JANI frontend (enabled by default); +- `promela` to include the Promela frontend (disabled by default); + +To change which frontends to include at build time, +explicitly select the desired features with the `--features` option as follows: + +```console +cargo install smc_scan --locked --features FEATURES +``` + +where `FEATURES` is a (comma-separated, or space-separated inside quotes) list. +Alternatively, if you want all available features, install SCAN with: + +```console +cargo install smc_scan --locked --all-features +``` + +Be aware that each feature imports extra dependencies and increases build time. From 8f9e6f023fd3c2d274e9fc0cc4e6ae969e4f9691 Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Mon, 8 Jun 2026 18:11:24 +0200 Subject: [PATCH 03/26] Add section on advanced build performance optimizations Signed-off-by: Enrico Ghiorzi --- README.md | 13 +++++++++++++ scan_book/src/manual/install.md | 15 +++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/README.md b/README.md index 3d79eb8..97e031e 100644 --- a/README.md +++ b/README.md @@ -65,6 +65,8 @@ Cargo will build and install SCAN on your system but it is recommended as it improves build reproducibility by enforcing the use of specified versions for dependencies). +### Installing specific versions + To install a specific SCAN version, e.g., v0.1.0, use: ```console @@ -105,6 +107,17 @@ cargo install smc_scan --locked --all-features Be aware that each feature imports extra dependencies and increases build time. +### Build optimization + +Even though by default the `cargo install` builds are highly-optimized, +there exist some further advanced build optimizations set via local configurations. +It can be difficult (and inappropriate) to enable these compiler optimizations on the SCAN side, +so we prefer to leave it to (advanced) individual users to decide what makes sense for their use cases. +Empirically, such optimization have been shown to yield up to, but no more than, a 10% performance improvement on typical SCAN use cases. + +An excellent, though unofficial, reference on Rust performance optimization is (https://nnethercote.github.io/perf-book/), +specifically the [Build configuration](https://nnethercote.github.io/perf-book/build-configuration.html) section. + ## Usage After installation, SCAN can be used as a CLI tool. diff --git a/scan_book/src/manual/install.md b/scan_book/src/manual/install.md index 3c537a3..05892da 100644 --- a/scan_book/src/manual/install.md +++ b/scan_book/src/manual/install.md @@ -37,6 +37,8 @@ scan to verify that the installation completed successfully by displaying the in-line help. +## Installing specific versions + To install a specific SCAN version, e.g., v0.1.0, use: ```console @@ -49,6 +51,8 @@ It is also possible to install SCAN from the latest commit directly from this re cargo install --git https://github.com/convince-project/scan ``` +(see `cargo install --help` for more options). + ## Features By default, SCAN includes the SCXML and JANI frontends, @@ -74,3 +78,14 @@ cargo install smc_scan --locked --all-features ``` Be aware that each feature imports extra dependencies and increases build time. + +## Build optimization + +Even though by default the `cargo install` builds are highly-optimized, +there exist some further advanced build optimizations set via local configurations. +It can be difficult (and inappropriate) to enable these compiler optimizations on the SCAN side, +so we prefer to leave it to (advanced) individual users to decide what makes sense for their use cases. +Empirically, such optimization have been shown to yield up to, but no more than, a 10% performance improvement on typical SCAN use cases. + +An excellent, though unofficial, reference on Rust performance optimization is (https://nnethercote.github.io/perf-book/), +specifically the [Build configuration](https://nnethercote.github.io/perf-book/build-configuration.html) section. From eeadb2e7804714b8d959da7c54f1f6ebb6659c93 Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Mon, 8 Jun 2026 18:43:22 +0200 Subject: [PATCH 04/26] Update docs on duration option Signed-off-by: Enrico Ghiorzi --- scan_book/src/manual/interface.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scan_book/src/manual/interface.md b/scan_book/src/manual/interface.md index 4900c5b..77f5dea 100644 --- a/scan_book/src/manual/interface.md +++ b/scan_book/src/manual/interface.md @@ -1,4 +1,4 @@ -# The User Interface +# The user interface SCAN provides a command line interface. @@ -95,10 +95,10 @@ via the new adaptive sampling method. This determines the number of necessary samples also based on the outcomes of the previous samples, so that this number cannot be known a-priori but has to be continually recalculated during the verification task. -The `--duration` flag's value sets the maximum duration (in model time) that the execution can take before being stopped. -As this may vary depending on the input model and SCAN has no means to determine it, -SCAN sets a reasonably large default value (10,000 time steps), -but for best results the developer should set a value fitting the model. +By default, the model passed to SCAN is assumed to be untimed. +For timed models, use the `--duration` option to set the maximum duration (in model time) that the execution can take before being stopped. +As the most appropriate value for this option may vary depending on the input model, +the developer should set a suitable value manually. __WARNING:__ if verification seems to be hanging without making any progress, it might be due to a wrong (too small) duration value. From d9d690a69714ff287d07def4ed01b631733805ad Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Mon, 8 Jun 2026 18:50:24 +0200 Subject: [PATCH 05/26] Improve book index and titles consistency Signed-off-by: Enrico Ghiorzi --- scan_book/src/SUMMARY.md | 18 +++++++++--------- scan_book/src/scxml/properties.md | 2 ++ scan_core/src/lib.rs | 14 +++++++------- 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/scan_book/src/SUMMARY.md b/scan_book/src/SUMMARY.md index b0c4ca7..d83e73c 100644 --- a/scan_book/src/SUMMARY.md +++ b/scan_book/src/SUMMARY.md @@ -2,19 +2,19 @@ [Introduction](./README.md) -# The SCAN User Manual +# The SCAN user manual - [Installation](./manual/install.md) -- [The User Interface](./manual/interface.md) +- [The user interface](./manual/interface.md) -# Model Checking Background in SCAN +# Model checking background - [Channel Systems]() -- [Temporal Logic]() -- [Statistical Model Checking]() +- [Temporal logic]() +- [Statistical model checking]() -# SCXML-based Model Specification Format +# SCXML model specification -- [Model Main File]() -- [Properties](./scxml/properties.md) -- [SCXML Processes]() +- [Model main file]() +- [XML properties](./scxml/properties.md) +- [SCXML processes]() diff --git a/scan_book/src/scxml/properties.md b/scan_book/src/scxml/properties.md index d36e1c6..b1f9143 100644 --- a/scan_book/src/scxml/properties.md +++ b/scan_book/src/scxml/properties.md @@ -1,3 +1,5 @@ +# XML properties + Properties are to be specified in a custom XML format (as there is no property specification format in SCXML). The following example shows the format structure and its elements: diff --git a/scan_core/src/lib.rs b/scan_core/src/lib.rs index 937812b..4c893a3 100644 --- a/scan_core/src/lib.rs +++ b/scan_core/src/lib.rs @@ -144,13 +144,13 @@ impl Scan { local_failures = self.failures.fetch_add(1, Ordering::Relaxed); let violations = &mut *self.violations.lock().unwrap(); violations.resize(violations.len().max(guarantees.len()), 0); - guarantees.iter().zip(violations.iter_mut()).for_each( - |(success, violations)| { - if !success { - *violations += 1; - } - }, - ); + guarantees + .into_iter() + .zip(violations.iter_mut()) + .filter(|(success, _)| !success) + .for_each(|(_, violations)| { + *violations += 1; + }); // If guarantee is violated, we have found a counter-example! trace!("runs: {local_failures} failures"); } From 465d9f51e9f6810b56ab0c87d883c9074750c0b2 Mon Sep 17 00:00:00 2001 From: Enrico Ghiorzi Date: Mon, 8 Jun 2026 19:23:30 +0200 Subject: [PATCH 06/26] Remove Smallvec optimization and dependency as it has no measurable benefits compared to std Vec Signed-off-by: Enrico Ghiorzi --- Cargo.lock | 7 ------- Cargo.toml | 4 ++-- scan_core/Cargo.toml | 1 - scan_core/src/channel_system.rs | 19 +++++++++---------- scan_core/src/program_graph.rs | 14 ++++++-------- scan_core/src/program_graph/builder.rs | 9 ++++----- scan_jani/Cargo.toml | 2 +- scan_promela/Cargo.toml | 8 ++++---- scan_scxml/Cargo.toml | 2 +- 9 files changed, 27 insertions(+), 39 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ce4133d..d8d8263 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1521,12 +1521,6 @@ version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" -[[package]] -name = "smallvec" -version = "1.15.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" - [[package]] name = "smc_scan" version = "0.3.0" @@ -1555,7 +1549,6 @@ dependencies = [ "log", "rand", "rayon", - "smallvec", "thiserror", ] diff --git a/Cargo.toml b/Cargo.toml index dfff3b2..c5dbb59 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -50,9 +50,9 @@ members = [ [workspace.dependencies] anyhow = "1.0.102" csv = "1.4.0" -log = "0.4.29" +log = "0.4.32" serde = { version = "1.0.228", features = ["derive"] } -serde_json = "1.0.149" +serde_json = "1.0.150" thiserror = "2.0.18" [dependencies] diff --git a/scan_core/Cargo.toml b/scan_core/Cargo.toml index ef49c59..470258e 100644 --- a/scan_core/Cargo.toml +++ b/scan_core/Cargo.toml @@ -27,7 +27,6 @@ log = { workspace = true } flate2 = { version = "1.1.9", features = ["zlib-rs"], default-features = false } rand = { version = "0.10.1" } rayon = "1.12.0" -smallvec = "1.15.1" [dev-dependencies] criterion = "0.8.2" diff --git a/scan_core/src/channel_system.rs b/scan_core/src/channel_system.rs index 128e4b9..73f5286 100644 --- a/scan_core/src/channel_system.rs +++ b/scan_core/src/channel_system.rs @@ -119,7 +119,6 @@ pub use builder::*; use rand::rngs::SmallRng; use rand::seq::IteratorRandom; use rand::{RngExt, SeedableRng}; -use smallvec::SmallVec; use std::collections::VecDeque; use thiserror::Error; @@ -269,9 +268,9 @@ pub struct Event { #[derive(Debug, Clone, PartialEq)] pub enum EventType { /// Sending a value to a channel. - Send(SmallVec<[Val; 2]>), + Send(Vec), /// Retrieving a value out of a channel. - Receive(SmallVec<[Val; 2]>), + Receive(Vec), /// Checking whether a channel is empty. ProbeEmptyQueue, /// Checking whether a channel is full. @@ -480,7 +479,7 @@ impl<'def> ChannelSystemRun<'def> { .filter_map(|(action, post_states)| { post_states .map(|locs| locs.choose(&mut rand1).map(|loc| Location(pg_id, loc))) - .collect::>>() + .collect::>>() .map(|locs| (action, locs)) }) .choose(&mut rand2) @@ -598,7 +597,7 @@ impl<'def> ChannelSystemRun<'def> { action.1, post.iter() .map(|loc| loc.1) - .collect::>() + .collect::>() .as_slice(), &mut self.rng, ) @@ -615,13 +614,13 @@ impl<'def> ChannelSystemRun<'def> { let (types, _) = &self.def.channels[channel.0 as usize]; let vals = self.message_queue[channel.0 as usize] .drain(..types.len()) - .collect::>(); + .collect::>(); self.program_graphs[pg_id.0 as usize] .receive( action.1, post.iter() .map(|loc| loc.1) - .collect::>() + .collect::>() .as_slice(), vals.as_slice(), ) @@ -642,7 +641,7 @@ impl<'def> ChannelSystemRun<'def> { action.1, post.iter() .map(|loc| loc.1) - .collect::>() + .collect::>() .as_slice(), &mut self.rng, ) @@ -660,7 +659,7 @@ impl<'def> ChannelSystemRun<'def> { action.1, post.iter() .map(|loc| loc.1) - .collect::>() + .collect::>() .as_slice(), &mut self.rng, ) @@ -685,7 +684,7 @@ impl<'def> ChannelSystemRun<'def> { action.1, post.iter() .map(|loc| loc.1) - .collect::>() + .collect::>() .as_slice(), &mut self.rng, ) diff --git a/scan_core/src/program_graph.rs b/scan_core/src/program_graph.rs index 33d278f..6dbaa5f 100644 --- a/scan_core/src/program_graph.rs +++ b/scan_core/src/program_graph.rs @@ -23,7 +23,6 @@ //! //! ``` //! # use scan_core::program_graph::{ProgramGraphBuilder, Location}; -//! # use smallvec::smallvec; //! // Create a new PG builder //! let mut pg_builder = ProgramGraphBuilder::new(); //! @@ -82,7 +81,6 @@ mod builder; use crate::{Time, grammar::*}; pub use builder::*; use rand::{Rng, rngs::SmallRng}; -use smallvec::SmallVec; use thiserror::Error; /// The index for [`Location`]s in a [`ProgramGraph`]. @@ -201,8 +199,8 @@ pub enum PgError { enum Effect { // NOTE: Could use a SmallVec for clock resets Effects(Vec<(Var, Expression)>, Vec), - Send(SmallVec<[Expression; 2]>), - Receive(SmallVec<[Var; 2]>), + Send(Vec>), + Receive(Vec), } type LocationData = (Vec<(Action, Vec)>, Vec); @@ -244,7 +242,7 @@ type LocationData = (Vec<(Action, Vec)>, Vec); /// ``` #[derive(Debug, Clone)] pub struct ProgramGraph { - initial_states: SmallVec<[Location; 8]>, + initial_states: Vec, effects: Vec, locations: Vec, // Time invariants of each location @@ -348,7 +346,7 @@ impl<'a, I: Iterator> Iterator for Transition /// because only the internal state needs to be duplicated. #[derive(Debug, Clone)] pub struct ProgramGraphRun<'def> { - current_states: SmallVec<[Location; 8]>, + current_states: Vec, vars: Vec, clocks: Vec