diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 7cf3b6d..a8454b7 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -15,6 +15,6 @@ jobs:
     - name: Check fmt
       run: cargo fmt --all -- --check
     - name: Check
-      run: cargo check --verbose
+      run: cargo check --verbose --all-features
     - name: Run tests
-      run: cargo test --verbose --workspace --all-targets
+      run: cargo test --verbose --workspace --all-targets --all-features
diff --git a/Cargo.lock b/Cargo.lock
index fea7518..1ac485e 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,15 +2,6 @@
 # It is not intended for manual editing.
 version = 4
 
-[[package]]
-name = "addr2line"
-version = "0.25.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1b5d307320b3181d6d7954e663bd7c774a838b8220fe0593c86d9fb09f498b4b"
-dependencies = [
- "gimli",
-]
-
 [[package]]
 name = "adler2"
 version = "2.0.1"
@@ -105,9 +96,9 @@ checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c"
 
 [[package]]
 name = "ar_archive_writer"
-version = "0.5.1"
+version = "0.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7eb93bbb63b9c227414f6eb3a0adfddca591a8ce1e9b60661bb08969b87e340b"
+checksum = "4087686b4b0a3427190bae57a1d9a478dbb2d40c5dc1bd6e2b6d797913bdd348"
 dependencies = [
  "object",
 ]
@@ -118,21 +109,6 @@ version = "1.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53"
 
-[[package]]
-name = "backtrace"
-version = "0.3.76"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bb531853791a215d7c62a30daf0dde835f381ab5de4589cfe7c649d2cbe92bd6"
-dependencies = [
- "addr2line",
- "cfg-if",
- "libc",
- "miniz_oxide",
- "object",
- "rustc-demangle",
- "windows-link",
-]
-
 [[package]]
 name = "bincode"
 version = "2.0.1"
@@ -155,9 +131,15 @@ dependencies = [
 
 [[package]]
 name = "bitflags"
-version = "2.11.1"
+version = "1.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
+
+[[package]]
+name = "bitflags"
+version = "2.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3"
+checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8"
 
 [[package]]
 name = "boa_ast"
@@ -165,7 +147,7 @@ version = "0.21.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6339a700715bda376f5ea65c76e8fe8fc880930d8b0638cea68e7f3da6538e0a"
 dependencies = [
- "bitflags",
+ "bitflags 2.13.0",
  "boa_interner",
  "boa_macros",
  "boa_string",
@@ -220,7 +202,7 @@ version = "0.21.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "35bd957fa9fa93e3a001a8aba5a5cd40c2bbfde486378be4c4b472fd304aaddb"
 dependencies = [
- "bitflags",
+ "bitflags 2.13.0",
  "boa_ast",
  "boa_interner",
  "boa_macros",
@@ -266,9 +248,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5"
 
 [[package]]
 name = "cc"
-version = "1.2.63"
+version = "1.2.65"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "556e016178bb5662a08681bbe0f00f8e17631781a4dfc8c45e466e4b185ec27f"
+checksum = "e228eec9be7c17ccb640b59b36a5cd805ea2a564a4c5e162c2f659fea30d3b96"
 dependencies = [
  "find-msvc-tools",
  "shlex",
@@ -517,14 +499,43 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "defmt"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a6e524506490a1953d237cb87b1cfc1e46f88c18f10a22dfe0f507dc6bfc7f7f"
+dependencies = [
+ "bitflags 1.3.2",
+ "defmt-macros",
+]
+
+[[package]]
+name = "defmt-macros"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0a27770e9c8f719a79d8b638281f4d828f77d8fd61e0bd94451b9b85e576a0b"
+dependencies = [
+ "defmt-parser",
+ "proc-macro-error2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "defmt-parser"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e"
+dependencies = [
+ "thiserror",
+]
+
 [[package]]
 name = "deranged"
 version = "0.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7cd812cc2bc1d69d4764bd80df88b4317eaef9e773c75226407d9bc0876b211c"
-dependencies = [
- "powerfmt",
-]
 
 [[package]]
 name = "displaydoc"
@@ -669,24 +680,16 @@ dependencies = [
 
 [[package]]
 name = "getrandom"
-version = "0.4.2"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555"
+checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099"
 dependencies = [
  "cfg-if",
  "libc",
  "r-efi",
  "rand_core",
- "wasip2",
- "wasip3",
 ]
 
-[[package]]
-name = "gimli"
-version = "0.32.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e629b9b98ef3dd8afe6ca2bd0f89306cec16d43d907889945bc5d6687f2f13c7"
-
 [[package]]
 name = "glob"
 version = "0.3.3"
@@ -738,22 +741,6 @@ version = "0.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
 
-[[package]]
-name = "human-panic"
-version = "2.0.8"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2815d0c49773c6e0a9753960b3d0e50b822e48e08c77bcb4780be8474c9cc3d"
-dependencies = [
- "anstream",
- "anstyle",
- "backtrace",
- "serde",
- "serde_derive",
- "sysinfo",
- "toml",
- "uuid",
-]
-
 [[package]]
 name = "icu_collections"
 version = "2.0.0"
@@ -820,12 +807,6 @@ dependencies = [
  "zerovec",
 ]
 
-[[package]]
-name = "id-arena"
-version = "2.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954"
-
 [[package]]
 name = "indexmap"
 version = "2.14.0"
@@ -834,8 +815,6 @@ checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
  "equivalent",
  "hashbrown 0.17.1",
- "serde",
- "serde_core",
 ]
 
 [[package]]
@@ -875,10 +854,11 @@ checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
 
 [[package]]
 name = "jiff"
-version = "0.2.28"
+version = "0.2.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4603d3033e49e2b0e31229fcab20a5d40089c607d975cd9c80551dc69eed9102"
+checksum = "34f877a98676d2fb664698d74cc6a51ce6c484ce8c770f05d0108ec9090aeb46"
 dependencies = [
+ "defmt",
  "jiff-static",
  "log",
  "portable-atomic",
@@ -888,9 +868,9 @@ dependencies = [
 
 [[package]]
 name = "jiff-static"
-version = "0.2.28"
+version = "0.2.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "782d32378dddf207193ac91cefb848ad41abb58195c95168e1291227a0832b47"
+checksum = "0666b5ab5ecaca213fc2a85b8c0083d9004e84ee2d5f9a7e0017aaf50986f25f"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -899,22 +879,15 @@ dependencies = [
 
 [[package]]
 name = "js-sys"
-version = "0.3.99"
+version = "0.3.102"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "142bc4740e452c1e57ade0cbc129f139c9093e354346f0872ef985f4f5cf5f11"
+checksum = "03d04c30968dffe80775bd4d7fb676131cd04a1fb46d2686dbffbaec2d9dfd31"
 dependencies = [
  "cfg-if",
  "futures-util",
- "once_cell",
  "wasm-bindgen",
 ]
 
-[[package]]
-name = "leb128fmt"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
-
 [[package]]
 name = "libc"
 version = "0.2.186"
@@ -929,9 +902,9 @@ checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0"
 
 [[package]]
 name = "log"
-version = "0.4.30"
+version = "0.4.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "616ec5685824bcc94416c6d4a7a446eea774a31efd7062c8480ba6fd06d7a6e5"
+checksum = "0ceec5bc11778974d1bcb055b18002eba7f4b3518b6a0081b3af5f21666da9ad"
 
 [[package]]
 name = "logos"
@@ -1027,9 +1000,9 @@ dependencies = [
 
 [[package]]
 name = "memchr"
-version = "2.8.1"
+version = "2.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8"
+checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4"
 
 [[package]]
 name = "miniz_oxide"
@@ -1041,15 +1014,6 @@ dependencies = [
  "simd-adler32",
 ]
 
-[[package]]
-name = "ntapi"
-version = "0.4.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c3b335231dfd352ffb0f8017f3b6027a4917f7df785ea2143d8af2adc66980ae"
-dependencies = [
- "winapi",
-]
-
 [[package]]
 name = "num-bigint"
 version = "0.4.6"
@@ -1093,25 +1057,6 @@ dependencies = [
  "libc",
 ]
 
-[[package]]
-name = "objc2-core-foundation"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a180dd8642fa45cdb7dd721cd4c11b1cadd4929ce112ebd8b9f5803cc79d536"
-dependencies = [
- "bitflags",
-]
-
-[[package]]
-name = "objc2-io-kit"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "33fafba39597d6dc1fb709123dfa8289d39406734be322956a69f0931c73bb15"
-dependencies = [
- "libc",
- "objc2-core-foundation",
-]
-
 [[package]]
 name = "object"
 version = "0.37.3"
@@ -1281,6 +1226,28 @@ dependencies = [
  "syn",
 ]
 
+[[package]]
+name = "proc-macro-error-attr2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
+dependencies = [
+ "proc-macro2",
+ "quote",
+]
+
+[[package]]
+name = "proc-macro-error2"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
+dependencies = [
+ "proc-macro-error-attr2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "proc-macro2"
 version = "1.0.106"
@@ -1311,9 +1278,9 @@ dependencies = [
 
 [[package]]
 name = "quote"
-version = "1.0.45"
+version = "1.0.46"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
 dependencies = [
  "proc-macro2",
 ]
@@ -1363,9 +1330,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.12.3"
+version = "1.12.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276"
+checksum = "f1292b7759ae1cb9ec195452d1390a074f0cd8541ab7a5a8c31cd6db45d4a6ba"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -1386,9 +1353,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.8.10"
+version = "0.8.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a"
+checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4"
 
 [[package]]
 name = "regress"
@@ -1400,12 +1367,6 @@ dependencies = [
  "memchr",
 ]
 
-[[package]]
-name = "rustc-demangle"
-version = "0.1.27"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d"
-
 [[package]]
 name = "rustc-hash"
 version = "2.1.2"
@@ -1439,12 +1400,6 @@ dependencies = [
  "winapi-util",
 ]
 
-[[package]]
-name = "semver"
-version = "1.0.28"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
-
 [[package]]
 name = "serde"
 version = "1.0.228"
@@ -1488,15 +1443,6 @@ dependencies = [
  "zmij",
 ]
 
-[[package]]
-name = "serde_spanned"
-version = "1.1.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6662b5879511e06e8999a8a235d848113e942c9124f211511b16466ee2995f26"
-dependencies = [
- "serde_core",
-]
-
 [[package]]
 name = "shlex"
 version = "2.0.1"
@@ -1521,12 +1467,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"
@@ -1535,7 +1475,6 @@ dependencies = [
  "clap",
  "clap-verbosity-flag",
  "env_logger",
- "human-panic",
  "indicatif",
  "log",
  "serde",
@@ -1550,12 +1489,12 @@ dependencies = [
 name = "smc_scan_core"
 version = "0.2.0"
 dependencies = [
+ "bumpalo",
  "criterion",
  "flate2",
  "log",
  "rand",
  "rayon",
- "smallvec",
  "thiserror",
 ]
 
@@ -1666,9 +1605,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
 
 [[package]]
 name = "syn"
-version = "2.0.117"
+version = "2.0.118"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1686,20 +1625,6 @@ dependencies = [
  "syn",
 ]
 
-[[package]]
-name = "sysinfo"
-version = "0.38.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "92ab6a2f8bfe508deb3c6406578252e491d299cbbf3bc0529ecc3313aee4a52f"
-dependencies = [
- "libc",
- "memchr",
- "ntapi",
- "objc2-core-foundation",
- "objc2-io-kit",
- "windows",
-]
-
 [[package]]
 name = "thiserror"
 version = "2.0.18"
@@ -1722,12 +1647,11 @@ dependencies = [
 
 [[package]]
 name = "time"
-version = "0.3.47"
+version = "0.3.51"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c"
+checksum = "85c17d80feb7334b40c484e45ed1a5273dfd8bfda537c3be2e74a06a6686f327"
 dependencies = [
  "deranged",
- "itoa",
  "libc",
  "num-conv",
  "num_threads",
@@ -1739,15 +1663,15 @@ dependencies = [
 
 [[package]]
 name = "time-core"
-version = "0.1.8"
+version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7694e1cfe791f8d31026952abf09c69ca6f6fa4e1a1229e18988f06a04a12dca"
+checksum = "9e1c906769ad99c88eaa54e728060edef082f8e358ff32030cb7c7d315e81109"
 
 [[package]]
 name = "time-macros"
-version = "0.2.27"
+version = "0.2.30"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2e70e4c5a0e0a8a4823ad65dfe1a6930e4f4d756dcd9dd7939022b5e8c501215"
+checksum = "dcef1a61bdb119096e153208ec5cbec23944ce8bca13be5c7f60c634f7403935"
 dependencies = [
  "num-conv",
  "time-core",
@@ -1774,33 +1698,6 @@ dependencies = [
  "serde_json",
 ]
 
-[[package]]
-name = "toml"
-version = "1.1.2+spec-1.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "81f3d15e84cbcd896376e6730314d59fb5a87f31e4b038454184435cd57defee"
-dependencies = [
- "serde_core",
- "serde_spanned",
- "toml_datetime",
- "toml_writer",
-]
-
-[[package]]
-name = "toml_datetime"
-version = "1.1.1+spec-1.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3165f65f62e28e0115a00b2ebdd37eb6f3b641855f9d636d3cd4103767159ad7"
-dependencies = [
- "serde_core",
-]
-
-[[package]]
-name = "toml_writer"
-version = "1.1.1+spec-1.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "756daf9b1013ebe47a8776667b466417e2d4c5679d441c26230efd9ef78692db"
-
 [[package]]
 name = "unicode-ident"
 version = "1.0.24"
@@ -1809,9 +1706,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"
@@ -1825,12 +1722,6 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254"
 
-[[package]]
-name = "unicode-xid"
-version = "0.2.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
-
 [[package]]
 name = "unit-prefix"
 version = "0.5.2"
@@ -1849,15 +1740,6 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
-[[package]]
-name = "uuid"
-version = "1.23.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d258b83ceec21034727ecee8c382cfa6c3e133699b0742c64571814fb420c9f7"
-dependencies = [
- "getrandom",
-]
-
 [[package]]
 name = "vergen"
 version = "8.3.2"
@@ -1895,29 +1777,11 @@ dependencies = [
  "winapi-util",
 ]
 
-[[package]]
-name = "wasip2"
-version = "1.0.3+wasi-0.2.9"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6"
-dependencies = [
- "wit-bindgen 0.57.1",
-]
-
-[[package]]
-name = "wasip3"
-version = "0.4.0+wasi-0.3.0-rc-2026-01-06"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5"
-dependencies = [
- "wit-bindgen 0.51.0",
-]
-
 [[package]]
 name = "wasm-bindgen"
-version = "0.2.122"
+version = "0.2.125"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3ed04576f974d2b2fba0f38c51dbc5518011e38c36bf1143164be765528fd409"
+checksum = "8ddb3f79143bced6de84270411622a2699cee572fc0875aeaf1e7867cf9fca1a"
 dependencies = [
  "cfg-if",
  "once_cell",
@@ -1928,9 +1792,9 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-macro"
-version = "0.2.122"
+version = "0.2.125"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "916151b09da36bd82f6615cbf3a419e2f0ba23a03c6160e8e92eb6bd4aa1dec6"
+checksum = "4e21a184b13fb19e157296e2c46056aec9092264fab83e4ba59e68c61b323c3d"
 dependencies = [
  "quote",
  "wasm-bindgen-macro-support",
@@ -1938,9 +1802,9 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-macro-support"
-version = "0.2.122"
+version = "0.2.125"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "299047362ccbfce148b67ab7e73349f77748e00c8296f9542adfad2ad82c5c5e"
+checksum = "fecefd9c35bd935a20fc3fc344b5f29138961e4f47fb03297d88f2587afb5ebd"
 dependencies = [
  "bumpalo",
  "proc-macro2",
@@ -1951,52 +1815,18 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-shared"
-version = "0.2.122"
+version = "0.2.125"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a929b2c61f11ba3e9bc35b50c1f25cb38e0e892c0c231ae2b8cf78d5dad4437"
+checksum = "23939e44bb9a5d7576fa2b563dc2e136628f1224e88a8deed09e04858b77871f"
 dependencies = [
  "unicode-ident",
 ]
 
-[[package]]
-name = "wasm-encoder"
-version = "0.244.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319"
-dependencies = [
- "leb128fmt",
- "wasmparser",
-]
-
-[[package]]
-name = "wasm-metadata"
-version = "0.244.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909"
-dependencies = [
- "anyhow",
- "indexmap",
- "wasm-encoder",
- "wasmparser",
-]
-
-[[package]]
-name = "wasmparser"
-version = "0.244.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe"
-dependencies = [
- "bitflags",
- "hashbrown 0.15.5",
- "indexmap",
- "semver",
-]
-
 [[package]]
 name = "web-sys"
-version = "0.3.99"
+version = "0.3.102"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6d621441cfc37b84979402712047321980c178f299193a3589d05b99e8763436"
+checksum = "a6430a72df5eb332242960fe84b3002a241163998241eb596d4f739b9757061d"
 dependencies = [
  "js-sys",
  "wasm-bindgen",
@@ -2043,107 +1873,12 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
 
-[[package]]
-name = "windows"
-version = "0.62.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "527fadee13e0c05939a6a05d5bd6eec6cd2e3dbd648b9f8e447c6518133d8580"
-dependencies = [
- "windows-collections",
- "windows-core",
- "windows-future",
- "windows-numerics",
-]
-
-[[package]]
-name = "windows-collections"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "23b2d95af1a8a14a3c7367e1ed4fc9c20e0a26e79551b1454d72583c97cc6610"
-dependencies = [
- "windows-core",
-]
-
-[[package]]
-name = "windows-core"
-version = "0.62.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8e83a14d34d0623b51dce9581199302a221863196a1dde71a7663a4c2be9deb"
-dependencies = [
- "windows-implement",
- "windows-interface",
- "windows-link",
- "windows-result",
- "windows-strings",
-]
-
-[[package]]
-name = "windows-future"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e1d6f90251fe18a279739e78025bd6ddc52a7e22f921070ccdc67dde84c605cb"
-dependencies = [
- "windows-core",
- "windows-link",
- "windows-threading",
-]
-
-[[package]]
-name = "windows-implement"
-version = "0.60.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn",
-]
-
-[[package]]
-name = "windows-interface"
-version = "0.59.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn",
-]
-
 [[package]]
 name = "windows-link"
 version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5"
 
-[[package]]
-name = "windows-numerics"
-version = "0.3.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e2e40844ac143cdb44aead537bbf727de9b044e107a0f1220392177d15b0f26"
-dependencies = [
- "windows-core",
- "windows-link",
-]
-
-[[package]]
-name = "windows-result"
-version = "0.4.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7781fa89eaf60850ac3d2da7af8e5242a5ea78d1a11c49bf2910bb5a73853eb5"
-dependencies = [
- "windows-link",
-]
-
-[[package]]
-name = "windows-strings"
-version = "0.5.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7837d08f69c77cf6b07689544538e017c1bfcf57e34b4c0ff58e6c2cd3b37091"
-dependencies = [
- "windows-link",
-]
-
 [[package]]
 name = "windows-sys"
 version = "0.61.2"
@@ -2153,109 +1888,6 @@ dependencies = [
  "windows-link",
 ]
 
-[[package]]
-name = "windows-threading"
-version = "0.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3949bd5b99cafdf1c7ca86b43ca564028dfe27d66958f2470940f73d86d75b37"
-dependencies = [
- "windows-link",
-]
-
-[[package]]
-name = "wit-bindgen"
-version = "0.51.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5"
-dependencies = [
- "wit-bindgen-rust-macro",
-]
-
-[[package]]
-name = "wit-bindgen"
-version = "0.57.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
-
-[[package]]
-name = "wit-bindgen-core"
-version = "0.51.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc"
-dependencies = [
- "anyhow",
- "heck",
- "wit-parser",
-]
-
-[[package]]
-name = "wit-bindgen-rust"
-version = "0.51.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21"
-dependencies = [
- "anyhow",
- "heck",
- "indexmap",
- "prettyplease",
- "syn",
- "wasm-metadata",
- "wit-bindgen-core",
- "wit-component",
-]
-
-[[package]]
-name = "wit-bindgen-rust-macro"
-version = "0.51.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a"
-dependencies = [
- "anyhow",
- "prettyplease",
- "proc-macro2",
- "quote",
- "syn",
- "wit-bindgen-core",
- "wit-bindgen-rust",
-]
-
-[[package]]
-name = "wit-component"
-version = "0.244.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2"
-dependencies = [
- "anyhow",
- "bitflags",
- "indexmap",
- "log",
- "serde",
- "serde_derive",
- "serde_json",
- "wasm-encoder",
- "wasm-metadata",
- "wasmparser",
- "wit-parser",
-]
-
-[[package]]
-name = "wit-parser"
-version = "0.244.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736"
-dependencies = [
- "anyhow",
- "id-arena",
- "indexmap",
- "log",
- "semver",
- "serde",
- "serde_derive",
- "serde_json",
- "unicode-xid",
- "wasmparser",
-]
-
 [[package]]
 name = "writeable"
 version = "0.6.3"
@@ -2264,9 +1896,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",
@@ -2287,18 +1919,18 @@ dependencies = [
 
 [[package]]
 name = "zerocopy"
-version = "0.8.50"
+version = "0.8.52"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3b065d4f0e55f82fae73202e189638116a87c55ab6b8e6c2721e13dd9d854ad1"
+checksum = "ce1022995ff5ff5d841ad7d994facc23098cd40152f2c1d11cd607c6f530653f"
 dependencies = [
  "zerocopy-derive",
 ]
 
 [[package]]
 name = "zerocopy-derive"
-version = "0.8.50"
+version = "0.8.52"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b631b19d36a892ab55420c92dbc83ccd79274f25be714855d3074aa71cab639"
+checksum = "1ae7f38b72ec2a254e2b87ef277cf2cd4fb97cbebf944faa6f33354da0867930"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -2363,9 +1995,9 @@ dependencies = [
 
 [[package]]
 name = "zlib-rs"
-version = "0.6.3"
+version = "0.6.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3be3d40e40a133f9c916ee3f9f4fa2d9d63435b5fbe1bfc6d9dae0aa0ada1513"
+checksum = "977347db8caa080403f6b6b7c1cda9479a8e869316f7e13a59b19076a40f94e3"
 
 [[package]]
 name = "zmij"
diff --git a/Cargo.toml b/Cargo.toml
index 98587f3..7f9d9eb 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.
@@ -26,9 +32,15 @@ crate-type = ["lib"]  # The crate types to generate.
 name = "scan"  # The name of the target.
 path = "src/main.rs"
 
-[profile.release]
+[profile.release-lto]
+inherits = "release"
 lto = true
 codegen-units = 1
+debug = "none"
+
+[profile.profiling]
+inherits = "release-lto"
+debug = "full"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 [workspace]
@@ -44,9 +56,9 @@ members = [
 [workspace.dependencies]
 anyhow = "1.0.102"
 csv = "1.4.0"
-log = "0.4.29"
+log = "0.4.33"
 serde = { version = "1.0.228", features = ["derive"] }
-serde_json = "1.0.149"
+serde_json = "1.0.150"
 thiserror = "2.0.18"
 
 [dependencies]
@@ -54,12 +66,11 @@ anyhow = { workspace = true }
 clap = { version = "4.6.1", features = ["derive"] }
 clap-verbosity-flag = "3.0.4"
 env_logger = "0.11.10"
-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/README.md b/README.md
index 46f135b..1277353 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.
@@ -61,19 +65,9 @@ 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).
 
-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:
+For advanced installation options, refer to the [Install](https://convince-project.github.io/scan/manual/install.html) section of the SCAN Book.
 
-```console
-cargo install --git https://github.com/convince-project/scan
-```
-
-(see `cargo install --help` for more options).
+## Usage
 
 After installation, SCAN can be used as a CLI tool.
 To print the help screen, use
@@ -92,14 +86,7 @@ scan <MODEL> verify --all
 
 where `MODEL` is the path to your model file or folder.
 
-It can be helpful to run SCAN with logging activated.
-Use the `--verbose` flag (even multiple times) to increase the verbosity level, or
-
-```console
-RUST_LOG=<LOG_LEVEL> scan <MODEL>
-```
-
-where `LOG_LEVEL=error|warn|info|debug|trace`.
+For an in-depth documentation of the user interface, refer to the [Interface](https://convince-project.github.io/scan/manual/interface.html) section of the SCAN Book.
 
 ## Development
 
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/manual/install.md b/scan_book/src/manual/install.md
index 4c6bb7b..6e2662a 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,65 @@ 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
+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
+```
+
+(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 (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.
+
+## Build optimization
+
+Even though by default the `cargo install` builds are well-optimized,
+some further advanced build optimizations are possible.
+The extent of the speed-up that can be obtained depends on the use-case,
+and is not always worth the extra effort required to enable these configurations.
+
+Advanced Rust users will already be familiar with compilation settings
+and can tune the build as they see fit.
+For users that are unfamiliar with Rust but still want to get high performances,
+and without going into the details,
+a more optimized built can be attempted with:
+
+```console
+RUSTFLAGS="-C target-cpu=native" cargo install smc_scan --locked --profile release-lto
+```
+
+An excellent, though unofficial, reference on Rust performance optimization is [The Rust Performance Book](https://nnethercote.github.io/perf-book/),
+specifically the [Build configuration](https://nnethercote.github.io/perf-book/build-configuration.html) section.
diff --git a/scan_book/src/manual/interface.md b/scan_book/src/manual/interface.md
index 4900c5b..252d5cd 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,18 +95,6 @@ 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.
-
-__WARNING:__ if verification seems to be hanging without making any progress,
-it might be due to a wrong (too small) duration value.
-Indeed, if the model is still running and the properties still undetermined when it reaches the time limit,
-the execution is discarded and does not count towards the result.
-If this happens systematically, all executions will be discarded.
-In such case, increase the duration to a value appropriate to your model.
-
 By default, SCAN only prints a short message informing the user that a verification task is underway,
 then it hangs silently until the task is finished (if ever).
 This is a fine behavior for use by other tools or in scripts,
@@ -138,7 +126,7 @@ scan [GLOBAL_OPTIONS] <MODEL> trace [OPTIONS] [PROPERTIES]
 
 where `TRACES` is the number of traces that are requested.
 
-The available options are `--duration` and `--single-thread`,
+The available option is `--single-thread`,
 with the same meaning as for the `verify` command.
 
 The traces produced during verification are saved in a `./traces_NN/` directory,
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/Cargo.toml b/scan_core/Cargo.toml
index ef49c59..fcf051a 100644
--- a/scan_core/Cargo.toml
+++ b/scan_core/Cargo.toml
@@ -27,7 +27,7 @@ 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"
+bumpalo = { version = "3.20.3", features = ["collections"] }
 
 [dev-dependencies]
 criterion = "0.8.2"
diff --git a/scan_core/benches/program_graph.rs b/scan_core/benches/program_graph.rs
index 759ad9e..830fc20 100644
--- a/scan_core/benches/program_graph.rs
+++ b/scan_core/benches/program_graph.rs
@@ -84,7 +84,7 @@ fn counter_pg() -> ProgramGraphBuilder {
     let mut pg = ProgramGraphBuilder::new();
     let initial = pg.new_initial_location();
     let action = pg.new_action();
-    let var = pg.new_var(Val::Integer(0)).unwrap();
+    let var = pg.new_var(Val::Integer(0));
     pg.add_effect(
         action,
         var,
diff --git a/scan_core/src/channel_system.rs b/scan_core/src/channel_system.rs
index 128e4b9..9034e79 100644
--- a/scan_core/src/channel_system.rs
+++ b/scan_core/src/channel_system.rs
@@ -110,27 +110,26 @@
 //! ```
 
 mod builder;
+mod run;
 
+use crate::grammar::*;
 use crate::program_graph::{
     Action as PgAction, Clock as PgClock, Location as PgLocation, Var as PgVar, *,
 };
-use crate::{Time, grammar::*};
 pub use builder::*;
-use rand::rngs::SmallRng;
-use rand::seq::IteratorRandom;
-use rand::{RngExt, SeedableRng};
-use smallvec::SmallVec;
-use std::collections::VecDeque;
+pub use run::ChannelSystemRun;
 use thiserror::Error;
 
+type PgIndex = u16;
+
 /// An indexing object for PGs in a CS.
 ///
 /// These cannot be directly created or manipulated,
 /// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
 #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
-pub struct PgId(u16);
+pub struct PgId(PgIndex);
 
-impl From<PgId> for u16 {
+impl From<PgId> for PgIndex {
     #[inline]
     fn from(val: PgId) -> Self {
         val.0
@@ -181,8 +180,6 @@ pub struct Var(PgId, PgVar);
 #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
 pub struct Clock(PgId, PgClock);
 
-type TimeConstraint = (Clock, Option<Time>, Option<Time>);
-
 /// A message to be sent through a CS's channel.
 #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
 pub enum Message {
@@ -269,9 +266,9 @@ pub struct Event {
 #[derive(Debug, Clone, PartialEq)]
 pub enum EventType {
     /// Sending a value to a channel.
-    Send(SmallVec<[Val; 2]>),
+    Send(Vec<Val>),
     /// Retrieving a value out of a channel.
-    Receive(SmallVec<[Val; 2]>),
+    Receive(Vec<Val>),
     /// Checking whether a channel is empty.
     ProbeEmptyQueue,
     /// Checking whether a channel is full.
@@ -337,25 +334,7 @@ impl ChannelSystem {
     ///
     /// See also [`ProgramGraph::new_instance`].
     pub fn new_instance<'def>(&'def self) -> ChannelSystemRun<'def> {
-        let pgs = self.program_graphs.len() as u16;
-        let mut pg_list = Vec::from_iter((0..pgs).map(PgId));
-        pg_list.shrink_to_fit();
-
-        ChannelSystemRun {
-            rng: rand::make_rng(),
-            time: 0,
-            program_graphs: Vec::from_iter(
-                self.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
-            ),
-            message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| match cap {
-                ChannelCapacity::Queue(queue) => queue.map_or_else(VecDeque::new, |cap| {
-                    VecDeque::with_capacity(types.len() * cap)
-                }),
-                ChannelCapacity::Sink => VecDeque::new(),
-            })),
-            def: self,
-            pg_list,
-        }
+        ChannelSystemRun::new(self)
     }
 
     #[inline]
@@ -368,348 +347,33 @@ impl ChannelSystem {
         }
     }
 
-    /// Returns the list of defined channels, given as the pair of their type and capacity
-    /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
+    /// Returns an immutable reference to the list of [`ProgramGraph`]s of the Channel System.
     #[inline]
-    pub fn channels(&self) -> &Vec<(Vec<Type>, ChannelCapacity)> {
-        &self.channels
+    pub fn program_graphs(&self) -> &[ProgramGraph] {
+        &self.program_graphs
     }
-}
 
-/// Representation of a CS that can be executed transition-by-transition.
-///
-/// The structure of the CS cannot be changed,
-/// meaning that it is not possible to introduce new PGs or modifying them, or add new channels.
-/// Though, this restriction makes it so that cloning the [`ChannelSystem`] is cheap,
-/// because only the internal state needs to be duplicated.
-#[derive(Debug, Clone)]
-pub struct ChannelSystemRun<'def> {
-    rng: SmallRng,
-    time: Time,
-    message_queue: Vec<VecDeque<Val>>,
-    program_graphs: Vec<ProgramGraphRun<'def>>,
-    def: &'def ChannelSystem,
-    pg_list: Vec<PgId>,
-}
-
-impl<'def> ChannelSystemRun<'def> {
-    /// Returns the current time of the CS.
+    /// Returns the list of [`PgId`]s associated to the Program Graphs of the Channel System.
     #[inline]
-    pub fn time(&self) -> Time {
-        self.time
-    }
-
-    /// Iterates over all transitions that can be admitted in the current state.
-    ///
-    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
-    /// (the pre-state being necessarily the current state of the machine).
-    /// The (eventual) guard is guaranteed to be satisfied.
-    ///
-    /// See also [`ProgramGraphRun::possible_transitions`].
-    pub fn possible_transitions(
-        &self,
-    ) -> impl Iterator<
-        Item = (
-            PgId,
-            Action,
-            impl Iterator<Item = impl Iterator<Item = Location> + '_> + '_,
-        ),
-    > + '_ {
-        self.program_graphs
-            .iter()
-            .enumerate()
-            .flat_map(move |(id, pg)| {
-                let pg_id = PgId(id as u16);
-                pg.possible_transitions().filter_map(move |(action, post)| {
-                    let action = Action(pg_id, action);
-                    self.check_communication(pg_id, action).ok().map(move |()| {
-                        let post = post.map(move |locs| locs.map(move |loc| Location(pg_id, loc)));
-                        (pg_id, action, post)
-                    })
-                })
-            })
-    }
-
-    pub(crate) fn montecarlo_execution(&mut self) -> Option<(Action, Event)> {
-        let mut rand1 = SmallRng::from_rng(&mut self.rng);
-        let mut rand2 = SmallRng::from_rng(&mut self.rng);
-        // Setting pgs_left as length resets the queue
-        let mut pgs_left = self.pg_list.len();
-        while pgs_left > 0 {
-            // Select random pg within 0..pgs_left
-            let pg_select = self.rng.random_range(0..pgs_left);
-            let pg_id = self.pg_list[pg_select];
-            // Swap selected pg with last element of the queue (possibly itself, probably not worth checking)
-            // Decrease the length of the queue (so that selected element is removed)
-            pgs_left -= 1;
-            self.pg_list.swap(pg_select, pgs_left);
-            // Execute randomly chosen transitions on the picked PG until an event is generated,
-            // or no more transition is possible
-            // NOTE: Special treatment for PGs with single-location state for optimization of this common case.
-            // Hopefully it will be possible to treat all cases in a general way eventually.
-            if self.program_graphs[pg_id.0 as usize].current_states().len() == 1 {
-                while let Some((action, post_state)) = self.program_graphs[pg_id.0 as usize]
-                    .nosync_possible_transitions()
-                    .filter(|&(action, _)| {
-                        self.def
-                            .communication(pg_id, action)
-                            .is_none_or(|(channel, message)| self.check_message(channel, message))
-                    })
-                    .filter_map(|(action, post_states)| {
-                        post_states
-                            .choose(&mut rand1)
-                            .map(|loc| (action, Location(pg_id, loc)))
-                    })
-                    .choose(&mut rand2)
-                {
-                    let event = self
-                        .transition(pg_id, Action(pg_id, action), &[post_state])
-                        .expect("successful transition");
-                    if event.is_some() {
-                        return event.map(|ev| (Action(pg_id, action), ev));
-                    }
-                }
-            } else {
-                while let Some((action, post_states)) = self.program_graphs[pg_id.0 as usize]
-                    .possible_transitions()
-                    .filter(|&(action, _)| {
-                        self.def
-                            .communication(pg_id, action)
-                            .is_none_or(|(channel, message)| self.check_message(channel, message))
-                    })
-                    .filter_map(|(action, post_states)| {
-                        post_states
-                            .map(|locs| locs.choose(&mut rand1).map(|loc| Location(pg_id, loc)))
-                            .collect::<Option<SmallVec<[Location; 4]>>>()
-                            .map(|locs| (action, locs))
-                    })
-                    .choose(&mut rand2)
-                {
-                    let event = self
-                        .transition(pg_id, Action(pg_id, action), post_states.as_slice())
-                        .expect("successful transition");
-                    if event.is_some() {
-                        return event.map(|ev| (Action(pg_id, action), ev));
-                    }
-                }
-            }
-        }
-        None
+    pub fn program_graph_ids(&self) -> impl Iterator<Item = PgId> {
+        (0..self.program_graphs.len()).map(|idx| PgId(idx as PgIndex))
     }
 
+    /// Returns the list of defined channels, given as the pair of their type and capacity
+    /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
     #[inline]
-    fn check_message(&self, channel: Channel, message: Message) -> bool {
-        let channel_idx = channel.0 as usize;
-        let (_, capacity) = self.def.channels[channel_idx];
-        let len = self.message_queue[channel_idx].len();
-        // Channel capacity must never be exceeded!
-        // debug_assert!(capacity.is_none_or(|cap| len <= cap));
-        // NOTE FIXME currently handshake is unsupported
-        // !matches!(capacity, Some(0))
-        match capacity {
-            ChannelCapacity::Queue(capacity) => match message {
-                Message::Send => capacity.is_none_or(|cap| len < cap),
-                Message::Receive => len > 0,
-                Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
-                Message::ProbeEmptyQueue => len == 0,
-            },
-            ChannelCapacity::Sink => match message {
-                Message::Send | Message::ProbeEmptyQueue => true,
-                Message::Receive | Message::ProbeFullQueue => false,
-            },
-        }
-    }
-
-    fn check_communication(&self, pg_id: PgId, action: Action) -> Result<(), CsError> {
-        if pg_id.0 >= self.program_graphs.len() as u16 {
-            Err(CsError::MissingPg(pg_id))
-        } else if action.0 != pg_id {
-            Err(CsError::ActionNotInPg(action, pg_id))
-        } else if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
-            let (_, capacity) = self.def.channels[channel.0 as usize];
-            let len = self.message_queue[channel.0 as usize].len();
-            // Channel capacity must never be exceeded!
-            // assert!(capacity.is_none_or(|cap| len <= cap));
-            match capacity {
-                ChannelCapacity::Queue(capacity) => match message {
-                    Message::Send if capacity.is_some_and(|cap| len >= cap) => {
-                        Err(CsError::OutOfCapacity(channel))
-                    }
-                    Message::Receive if len == 0 => Err(CsError::Empty(channel)),
-                    Message::ProbeEmptyQueue | Message::ProbeFullQueue
-                        if matches!(capacity, Some(0)) =>
-                    {
-                        Err(CsError::ProbingHandshakeChannel(channel))
-                    }
-                    Message::ProbeFullQueue if capacity.is_none() => {
-                        Err(CsError::ProbingInfiniteQueue(channel))
-                    }
-                    Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)),
-                    Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => {
-                        Err(CsError::NotFull(channel))
-                    }
-                    _ => Ok(()),
-                },
-                ChannelCapacity::Sink => match message {
-                    Message::Send | Message::ProbeEmptyQueue => Ok(()),
-                    Message::ProbeFullQueue => Err(CsError::NotFull(channel)),
-                    Message::Receive => Err(CsError::Empty(channel)),
-                },
-            }
-        } else {
-            Ok(())
-        }
-    }
-
-    /// Executes a transition on the given PG characterized by the argument action and post-state.
-    ///
-    /// Fails if the requested transition is not admissible.
-    ///
-    /// See also [`ProgramGraphRun::transition`].
-    pub fn transition(
-        &mut self,
-        pg_id: PgId,
-        action: Action,
-        post: &[Location],
-    ) -> Result<Option<Event>, CsError> {
-        // If action is a communication, check it is legal
-        if pg_id.0 >= self.program_graphs.len() as u16 {
-            return Err(CsError::MissingPg(pg_id));
-        } else if action.0 != pg_id {
-            return Err(CsError::ActionNotInPg(action, pg_id));
-        } else if let Some(post) = post.iter().find(|l| l.0 != pg_id) {
-            return Err(CsError::LocationNotInPg(*post, pg_id));
-        }
-        // If the action is a communication, send/receive the message
-        if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
-            let (_, capacity) = self.def.channels[channel.0 as usize];
-            let event_type = match message {
-                Message::Send
-                    if let ChannelCapacity::Queue(capacity) = capacity
-                        && capacity.is_some_and(|cap| {
-                            self.message_queue[channel.0 as usize].len() >= cap
-                        }) =>
-                {
-                    return Err(CsError::OutOfCapacity(channel));
-                }
-                Message::Send => {
-                    let vals = self.program_graphs[pg_id.0 as usize]
-                        .send(
-                            action.1,
-                            post.iter()
-                                .map(|loc| loc.1)
-                                .collect::<SmallVec<[PgLocation; 8]>>()
-                                .as_slice(),
-                            &mut self.rng,
-                        )
-                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
-                    if matches!(capacity, ChannelCapacity::Queue(_)) {
-                        self.message_queue[channel.0 as usize].extend(vals.iter().copied());
-                    }
-                    EventType::Send(vals)
-                }
-                Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
-                    return Err(CsError::Empty(channel));
-                }
-                Message::Receive => {
-                    let (types, _) = &self.def.channels[channel.0 as usize];
-                    let vals = self.message_queue[channel.0 as usize]
-                        .drain(..types.len())
-                        .collect::<SmallVec<[Val; 2]>>();
-                    self.program_graphs[pg_id.0 as usize]
-                        .receive(
-                            action.1,
-                            post.iter()
-                                .map(|loc| loc.1)
-                                .collect::<SmallVec<[PgLocation; 8]>>()
-                                .as_slice(),
-                            vals.as_slice(),
-                        )
-                        .expect("communication has been verified before");
-                    EventType::Receive(vals)
-                }
-                Message::ProbeEmptyQueue | Message::ProbeFullQueue
-                    if matches!(capacity, ChannelCapacity::Queue(Some(0))) =>
-                {
-                    return Err(CsError::ProbingHandshakeChannel(channel));
-                }
-                Message::ProbeEmptyQueue if !self.message_queue[channel.0 as usize].is_empty() => {
-                    return Err(CsError::NotEmpty(channel));
-                }
-                Message::ProbeEmptyQueue => {
-                    let _ = self.program_graphs[pg_id.0 as usize]
-                        .send(
-                            action.1,
-                            post.iter()
-                                .map(|loc| loc.1)
-                                .collect::<SmallVec<[PgLocation; 8]>>()
-                                .as_slice(),
-                            &mut self.rng,
-                        )
-                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
-                    EventType::ProbeEmptyQueue
-                }
-                Message::ProbeFullQueue => match capacity {
-                    ChannelCapacity::Queue(None) => {
-                        return Err(CsError::ProbingInfiniteQueue(channel));
-                    }
-                    ChannelCapacity::Queue(Some(capacity)) => {
-                        if self.message_queue[channel.0 as usize].len() >= capacity {
-                            let _ = self.program_graphs[pg_id.0 as usize]
-                                .send(
-                                    action.1,
-                                    post.iter()
-                                        .map(|loc| loc.1)
-                                        .collect::<SmallVec<[PgLocation; 8]>>()
-                                        .as_slice(),
-                                    &mut self.rng,
-                                )
-                                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
-                            EventType::ProbeFullQueue
-                        } else {
-                            return Err(CsError::NotFull(channel));
-                        }
-                    }
-                    ChannelCapacity::Sink => return Err(CsError::NotFull(channel)),
-                },
-            };
-            Ok(Some(Event {
-                pg_id,
-                channel,
-                event_type,
-            }))
-        } else {
-            // Transition the program graph
-            self.program_graphs[pg_id.0 as usize]
-                .transition(
-                    action.1,
-                    post.iter()
-                        .map(|loc| loc.1)
-                        .collect::<SmallVec<[PgLocation; 8]>>()
-                        .as_slice(),
-                    &mut self.rng,
-                )
-                .map_err(|err| CsError::ProgramGraph(pg_id, err))
-                .map(|()| None)
-        }
+    pub fn channels(&self) -> &[(Vec<Type>, ChannelCapacity)] {
+        &self.channels
     }
 
-    /// Tries waiting for the given delta of time.
-    /// Returns error if any of the PG cannot wait due to some time invariant.
-    pub fn wait(&mut self, delta: Time) -> Result<(), CsError> {
-        if let Some(pg) = self
-            .program_graphs
-            .iter()
-            .position(|pg| !pg.can_wait(delta))
-        {
-            Err(CsError::ProgramGraph(PgId(pg as u16), PgError::Invariant))
-        } else {
-            self.program_graphs.iter_mut().for_each(|pg| {
-                pg.wait(delta).expect("wait");
-            });
-            self.time += delta;
-            Ok(())
-        }
+    /// Returns the type and capacity of the given channel
+    /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
+    #[inline]
+    pub fn channel(&self, channel: Channel) -> Result<(&[Type], ChannelCapacity), CsError> {
+        self.channels
+            .get(channel.0 as usize)
+            .map(|(types, cap)| (types.as_slice(), *cap))
+            .ok_or(CsError::MissingChannel(channel))
     }
 }
 
@@ -820,7 +484,7 @@ mod tests {
         let cs_def = cs.build();
         let mut cs = cs_def.new_instance();
         // assert_eq!(cs.possible_transitions().count(), 1);
-        assert_eq!(cs.def.communications_pg_idxs, vec![0, 2, 5]);
+        assert_eq!(cs.def().communications_pg_idxs, vec![0, 2, 5]);
 
         cs.transition(pg1, send, &[post1])?;
         cs.transition(pg2, receive, &[post2])?;
diff --git a/scan_core/src/channel_system/builder.rs b/scan_core/src/channel_system/builder.rs
index 644f7d4..b804124 100644
--- a/scan_core/src/channel_system/builder.rs
+++ b/scan_core/src/channel_system/builder.rs
@@ -1,11 +1,11 @@
 use super::{
     Action, Channel, ChannelSystem, Clock, CsError, Location, Message, PgError, PgExpression, PgId,
-    ProgramGraphBuilder, TimeConstraint, Var,
+    ProgramGraphBuilder, Var,
 };
 use crate::channel_system::ChannelCapacity;
 use crate::grammar::{BooleanExpr, Type};
 use crate::program_graph::ProgramGraph;
-use crate::{Expression, Val};
+use crate::{Expression, TimeRange, Val};
 use log::info;
 use std::collections::BTreeMap;
 
@@ -60,7 +60,7 @@ impl ChannelSystemBuilder {
 
     /// Add a new variable of the given type to the given PG.
     ///
-    /// It fails if the CS contains no such PG, or if the expression is badly-typed.
+    /// It fails if the CS contains no such PG.
     ///
     /// See [`ProgramGraphBuilder::new_var`] for more info.
     pub fn new_var(&mut self, pg_id: PgId, val: Val) -> Result<Var, CsError> {
@@ -68,9 +68,7 @@ impl ChannelSystemBuilder {
             .program_graphs
             .get_mut(pg_id.0 as usize)
             .ok_or(CsError::MissingPg(pg_id))?;
-        let var = pg
-            .new_var(val)
-            .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+        let var = pg.new_var(val);
         Ok(Var(pg_id, var))
     }
 
@@ -214,13 +212,13 @@ impl ChannelSystemBuilder {
     pub fn new_timed_location(
         &mut self,
         pg_id: PgId,
-        invariants: &[TimeConstraint],
+        invariants: &[(Clock, TimeRange)],
     ) -> Result<Location, CsError> {
         let invariants = invariants
             .iter()
-            .map(|(c, l, u)| {
+            .map(|(c, range)| {
                 if c.0 == pg_id {
-                    Ok((c.1, *l, *u))
+                    Ok((c.1, *range))
                 } else {
                     Err(CsError::DifferentPgs(pg_id, c.0))
                 }
@@ -273,13 +271,13 @@ impl ChannelSystemBuilder {
     pub fn new_initial_timed_location(
         &mut self,
         pg_id: PgId,
-        invariants: &[TimeConstraint],
+        invariants: &[(Clock, TimeRange)],
     ) -> Result<Location, CsError> {
         let invariants = invariants
             .iter()
-            .map(|(c, l, u)| {
+            .map(|(c, range)| {
                 if c.0 == pg_id {
-                    Ok((c.1, *l, *u))
+                    Ok((c.1, *range))
                 } else {
                     Err(CsError::DifferentPgs(pg_id, c.0))
                 }
@@ -344,7 +342,7 @@ impl ChannelSystemBuilder {
         action: Action,
         post: Location,
         guard: Option<CsGuard>,
-        constraints: &[TimeConstraint],
+        constraints: &[(Clock, TimeRange)],
     ) -> Result<(), CsError> {
         if action.0 != pg_id {
             Err(CsError::ActionNotInPg(action, pg_id))
@@ -362,9 +360,9 @@ impl ChannelSystemBuilder {
             });
             let constraints = constraints
                 .iter()
-                .map(|(c, l, u)| {
+                .map(|(c, range)| {
                     if c.0 == pg_id {
-                        Ok((c.1, *l, *u))
+                        Ok((c.1, *range))
                     } else {
                         Err(CsError::DifferentPgs(pg_id, c.0))
                     }
@@ -425,7 +423,7 @@ impl ChannelSystemBuilder {
         pre: Location,
         post: Location,
         guard: Option<CsGuard>,
-        constraints: &[TimeConstraint],
+        constraints: &[(Clock, TimeRange)],
     ) -> Result<(), CsError> {
         if pre.0 != pg_id {
             Err(CsError::LocationNotInPg(pre, pg_id))
@@ -441,9 +439,9 @@ impl ChannelSystemBuilder {
             });
             let constraints = constraints
                 .iter()
-                .map(|(c, l, u)| {
+                .map(|(c, range)| {
                     if c.0 == pg_id {
-                        Ok((c.1, *l, *u))
+                        Ok((c.1, *range))
                     } else {
                         Err(CsError::DifferentPgs(pg_id, c.0))
                     }
diff --git a/scan_core/src/channel_system/run.rs b/scan_core/src/channel_system/run.rs
new file mode 100644
index 0000000..967c428
--- /dev/null
+++ b/scan_core/src/channel_system/run.rs
@@ -0,0 +1,360 @@
+use super::{
+    Action, Channel, ChannelCapacity, ChannelSystem, CsError, Event, EventType, Location, Message,
+    PgId, PgLocation,
+};
+use crate::{
+    Time, Val,
+    program_graph::{PgError, ProgramGraphRun},
+};
+use bumpalo::{Bump, collections::CollectIn};
+use rand::rngs::SmallRng;
+use std::collections::VecDeque;
+
+/// Representation of a CS that can be executed transition-by-transition.
+///
+/// The structure of the CS cannot be changed,
+/// meaning that it is not possible to introduce new PGs or modifying them, or add new channels.
+/// Though, this restriction makes it so that cloning the [`ChannelSystem`] is cheap,
+/// because only the internal state needs to be duplicated.
+#[derive(Debug)]
+pub struct ChannelSystemRun<'def> {
+    rng: SmallRng,
+    time: Time,
+    message_queue: Vec<VecDeque<Val>>,
+    program_graphs: Vec<ProgramGraphRun<'def>>,
+    def: &'def ChannelSystem,
+    bump: Bump,
+}
+
+impl<'def> Clone for ChannelSystemRun<'def> {
+    fn clone(&self) -> Self {
+        Self {
+            rng: self.rng.clone(),
+            time: self.time,
+            message_queue: self.message_queue.clone(),
+            program_graphs: self.program_graphs.clone(),
+            def: self.def,
+            bump: Bump::new(),
+        }
+    }
+}
+
+impl<'def> ChannelSystemRun<'def> {
+    /// Creates a new [`ChannelSystemRun`] which allows to execute the CS as defined.
+    ///
+    /// The new instance borrows the [`ChannelSystem`] to refer to the CS definition without copying its data,
+    /// so that spawning instances is (relatively) inexpensive.
+    ///
+    /// See also [`ProgramGraphRun::new`].
+    pub fn new(cs: &'def ChannelSystem) -> Self {
+        let pgs = cs.program_graphs.len() as u16;
+        let mut pg_list = Vec::from_iter((0..pgs).map(PgId));
+        pg_list.shrink_to_fit();
+
+        ChannelSystemRun {
+            rng: rand::make_rng(),
+            time: 0,
+            program_graphs: Vec::from_iter(
+                cs.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
+            ),
+            message_queue: Vec::from_iter(cs.channels.iter().map(|(types, cap)| match cap {
+                ChannelCapacity::Queue(queue) => queue.map_or_else(VecDeque::new, |cap| {
+                    VecDeque::with_capacity(types.len() * cap)
+                }),
+                ChannelCapacity::Sink => VecDeque::new(),
+            })),
+            def: cs,
+            bump: Bump::new(),
+        }
+    }
+
+    /// Returns a reference to the underlying [`ChannelSystem`] defining the execution.
+    pub fn def(&self) -> &ChannelSystem {
+        self.def
+    }
+
+    /// Returns the current time of the CS.
+    #[inline]
+    pub fn time(&self) -> Time {
+        self.time
+    }
+
+    /// Returns an immutable reference to the [`ProgramGraphRun`]s of the Channel System associated to the given [`PgId`].
+    #[inline]
+    pub fn program_graph(&self, pg_id: PgId) -> Result<&ProgramGraphRun<'_>, CsError> {
+        self.program_graphs
+            .get(pg_id.0 as usize)
+            .ok_or(CsError::MissingPg(pg_id))
+    }
+
+    /// Iterates over all transitions that can be admitted in the current state.
+    ///
+    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
+    /// (the pre-state being necessarily the current state of the machine).
+    /// The (eventual) guard is guaranteed to be satisfied.
+    ///
+    /// See also [`ProgramGraphRun::possible_transitions`].
+    pub fn possible_transitions(
+        &self,
+    ) -> impl Iterator<
+        Item = (
+            PgId,
+            Action,
+            impl Iterator<Item = impl Iterator<Item = Location>>,
+        ),
+    > {
+        self.def.program_graph_ids().flat_map(move |pg_id| {
+            self.possible_transitions_pg(pg_id)
+                .expect("pg exists")
+                .map(move |(action, transitions)| (pg_id, action, transitions))
+        })
+    }
+
+    /// Iterates over all transitions that can be admitted in the current state for the [`ProgramGraph`] associated to the given [`PgId`].
+    ///
+    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
+    /// (the pre-state being necessarily the current state of the machine).
+    /// The (eventual) guard is guaranteed to be satisfied.
+    ///
+    /// See also [`ProgramGraphRun::possible_transitions`].
+    pub fn possible_transitions_pg(
+        &self,
+        pg_id: PgId,
+    ) -> Result<
+        impl Iterator<Item = (Action, impl Iterator<Item = impl Iterator<Item = Location>>)>,
+        CsError,
+    > {
+        self.program_graph(pg_id).map(|pg| {
+            pg.possible_transitions().filter_map(move |(action, post)| {
+                let action = Action(pg_id, action);
+                if let Some((channel, message)) = self.def.communication(pg_id, action.1)
+                    && !self.check_message(channel, message)
+                {
+                    None
+                } else {
+                    let post = post.map(move |locs| locs.map(move |loc| Location(pg_id, loc)));
+                    Some((action, post))
+                }
+            })
+        })
+    }
+
+    /// Iterates over all transitions that can be admitted in the current state for the [`ProgramGraph`] associated to the given [`PgId`],
+    /// optimized for the special (but common) case in which the state of the PG is given by a single location.
+    ///
+    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
+    /// (the pre-state being necessarily the current state of the machine).
+    /// The (eventual) guard is guaranteed to be satisfied.
+    ///
+    /// See also [`ProgramGraphRun::nosync_possible_transitions`].
+    pub fn nosync_possible_transitions_pg(
+        &self,
+        pg_id: PgId,
+    ) -> Result<impl Iterator<Item = (Action, impl Iterator<Item = Location>)>, CsError> {
+        self.program_graph(pg_id)?
+            .nosync_possible_transitions()
+            .map_err(|err| CsError::ProgramGraph(pg_id, err))
+            .map(|transitions| {
+                transitions.filter_map(move |(action, post)| {
+                    let action = Action(pg_id, action);
+                    if let Some((channel, message)) = self.def.communication(pg_id, action.1)
+                        && !self.check_message(channel, message)
+                    {
+                        None
+                    } else {
+                        let post = post.map(move |loc| Location(pg_id, loc));
+                        Some((action, post))
+                    }
+                })
+            })
+    }
+
+    fn check_message(&self, channel: Channel, message: Message) -> bool {
+        let channel_idx = channel.0 as usize;
+        let (_, capacity) = self.def.channels[channel_idx];
+        let len = self.message_queue[channel_idx].len();
+        // Channel capacity must never be exceeded!
+        // debug_assert!(capacity.is_none_or(|cap| len <= cap));
+        // NOTE FIXME currently handshake is unsupported
+        // !matches!(capacity, Some(0))
+        match capacity {
+            ChannelCapacity::Queue(capacity) => match message {
+                Message::Send => capacity.is_none_or(|cap| len < cap),
+                Message::Receive => len > 0,
+                Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
+                Message::ProbeEmptyQueue => len == 0,
+            },
+            ChannelCapacity::Sink => match message {
+                Message::Send | Message::ProbeEmptyQueue => true,
+                Message::Receive | Message::ProbeFullQueue => false,
+            },
+        }
+    }
+
+    /// Executes a transition on the given PG characterized by the argument action and post-state.
+    ///
+    /// Fails if the requested transition is not admissible.
+    ///
+    /// See also [`ProgramGraphRun::transition`].
+    pub fn transition(
+        &mut self,
+        pg_id: PgId,
+        action: Action,
+        post: &[Location],
+    ) -> Result<Option<Event>, CsError> {
+        use bumpalo::collections::Vec as BumpVec;
+
+        self.bump.reset();
+
+        // If action is a communication, check it is legal
+        if pg_id.0 >= self.program_graphs.len() as u16 {
+            return Err(CsError::MissingPg(pg_id));
+        } else if action.0 != pg_id {
+            return Err(CsError::ActionNotInPg(action, pg_id));
+        } else if let Some(post) = post.iter().find(|l| l.0 != pg_id) {
+            return Err(CsError::LocationNotInPg(*post, pg_id));
+        }
+        // If the action is a communication, send/receive the message
+        if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
+            let (_, capacity) = self.def.channels[channel.0 as usize];
+            let event_type = match message {
+                Message::Send
+                    if let ChannelCapacity::Queue(capacity) = capacity
+                        && capacity.is_some_and(|cap| {
+                            self.message_queue[channel.0 as usize].len() >= cap
+                        }) =>
+                {
+                    return Err(CsError::OutOfCapacity(channel));
+                }
+                Message::Send => {
+                    let vals = self.program_graphs[pg_id.0 as usize]
+                        .send(
+                            action.1,
+                            post.iter()
+                                .map(|loc| loc.1)
+                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
+                                .as_slice(),
+                            &mut self.rng,
+                        )
+                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+                    if matches!(capacity, ChannelCapacity::Queue(_)) {
+                        self.message_queue[channel.0 as usize].extend(&vals);
+                    }
+                    EventType::Send(vals)
+                }
+                Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
+                    return Err(CsError::Empty(channel));
+                }
+                Message::Receive => {
+                    let (types, _) = &self.def.channels[channel.0 as usize];
+                    let vals = self.message_queue[channel.0 as usize]
+                        .drain(..types.len())
+                        .collect::<Vec<Val>>();
+                    self.program_graphs[pg_id.0 as usize]
+                        .receive(
+                            action.1,
+                            post.iter()
+                                .map(|loc| loc.1)
+                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
+                                .as_slice(),
+                            vals.as_slice(),
+                        )
+                        .expect("communication has been verified before");
+                    EventType::Receive(vals)
+                }
+                Message::ProbeEmptyQueue | Message::ProbeFullQueue
+                    if matches!(capacity, ChannelCapacity::Queue(Some(0))) =>
+                {
+                    return Err(CsError::ProbingHandshakeChannel(channel));
+                }
+                Message::ProbeEmptyQueue if !self.message_queue[channel.0 as usize].is_empty() => {
+                    return Err(CsError::NotEmpty(channel));
+                }
+                Message::ProbeEmptyQueue => {
+                    let _ = self.program_graphs[pg_id.0 as usize]
+                        .send(
+                            action.1,
+                            post.iter()
+                                .map(|loc| loc.1)
+                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
+                                .as_slice(),
+                            &mut self.rng,
+                        )
+                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+                    EventType::ProbeEmptyQueue
+                }
+                Message::ProbeFullQueue => match capacity {
+                    ChannelCapacity::Queue(None) => {
+                        return Err(CsError::ProbingInfiniteQueue(channel));
+                    }
+                    ChannelCapacity::Queue(Some(capacity)) => {
+                        if self.message_queue[channel.0 as usize].len() >= capacity {
+                            let _ = self.program_graphs[pg_id.0 as usize]
+                                .send(
+                                    action.1,
+                                    post.iter()
+                                        .map(|loc| loc.1)
+                                        .collect_in::<BumpVec<PgLocation>>(&self.bump)
+                                        .as_slice(),
+                                    &mut self.rng,
+                                )
+                                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+                            EventType::ProbeFullQueue
+                        } else {
+                            return Err(CsError::NotFull(channel));
+                        }
+                    }
+                    ChannelCapacity::Sink => return Err(CsError::NotFull(channel)),
+                },
+            };
+            Ok(Some(Event {
+                pg_id,
+                channel,
+                event_type,
+            }))
+        } else {
+            // Transition the program graph
+            self.program_graphs[pg_id.0 as usize]
+                .transition(
+                    action.1,
+                    post.iter()
+                        .map(|loc| loc.1)
+                        .collect_in::<BumpVec<PgLocation>>(&self.bump)
+                        .as_slice(),
+                    &mut self.rng,
+                )
+                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+            Ok(None)
+        }
+    }
+
+    /// Tries waiting for the given delta of time.
+    /// Returns error if any of the PG cannot wait due to some time invariant.
+    pub fn wait(&mut self, delta: Time) -> Result<(), CsError> {
+        if let Some(pg) = self
+            .program_graphs
+            .iter()
+            .position(|pg| !pg.can_wait(delta))
+        {
+            Err(CsError::ProgramGraph(PgId(pg as u16), PgError::Invariant))
+        } else {
+            self.program_graphs.iter_mut().for_each(|pg| {
+                pg.wait(delta).expect("wait");
+            });
+            self.time += delta;
+            Ok(())
+        }
+    }
+
+    /// Checks if it is possible to wait a given amount of time-units without violating the time invariants.
+    #[inline]
+    pub fn can_wait(&self, delta: Time) -> bool {
+        self.program_graphs.iter().all(|pg| pg.can_wait(delta))
+    }
+
+    /// Returns `true` if there is any transition from the current state that will be unlocked at some point in the future.
+    #[inline]
+    pub fn is_waiting(&self) -> bool {
+        self.can_wait(1) && self.program_graphs.iter().any(|pg| pg.is_waiting())
+    }
+}
diff --git a/scan_core/src/grammar.rs b/scan_core/src/grammar.rs
index 09bb012..a70c6ca 100644
--- a/scan_core/src/grammar.rs
+++ b/scan_core/src/grammar.rs
@@ -212,7 +212,7 @@ where
     ///
     /// Will assume the expression (with the variable assignment) is well-typed,
     /// and may panic if producing an unexpected type.
-    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option<R>) -> Val {
+    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: Option<&mut R>) -> Val {
         match self {
             Expression::Boolean(boolean_expr) => Val::Boolean(boolean_expr.eval(vars, rng)),
             Expression::Natural(natural_expr) => Val::Natural(natural_expr.eval(vars, rng)),
@@ -228,17 +228,15 @@ where
     pub fn eval_deterministic(&self, vars: &dyn Fn(V) -> Val) -> Val {
         match self {
             Expression::Boolean(boolean_expr) => {
-                Val::Boolean(boolean_expr.eval::<SmallRng>(vars, &mut None))
+                Val::Boolean(boolean_expr.eval::<SmallRng>(vars, None))
             }
             Expression::Natural(natural_expr) => {
-                Val::Natural(natural_expr.eval::<SmallRng>(vars, &mut None))
+                Val::Natural(natural_expr.eval::<SmallRng>(vars, None))
             }
             Expression::Integer(integer_expr) => {
-                Val::Integer(integer_expr.eval::<SmallRng>(vars, &mut None))
-            }
-            Expression::Float(float_expr) => {
-                Val::Float(float_expr.eval::<SmallRng>(vars, &mut None))
+                Val::Integer(integer_expr.eval::<SmallRng>(vars, None))
             }
+            Expression::Float(float_expr) => Val::Float(float_expr.eval::<SmallRng>(vars, None)),
         }
     }
 
@@ -257,7 +255,7 @@ where
     /// Returns an error if expression contains variables.
     pub fn eval_constant(&self) -> Result<Val, TypeError> {
         if self.is_constant() {
-            Ok(self.eval::<rand::rngs::SmallRng>(&|_| panic!("no vars"), &mut None))
+            Ok(self.eval::<rand::rngs::SmallRng>(&|_| panic!("no vars"), None))
         } else {
             Err(TypeError::UnknownVar)
         }
diff --git a/scan_core/src/grammar/boolean.rs b/scan_core/src/grammar/boolean.rs
index acdf62b..5741839 100644
--- a/scan_core/src/grammar/boolean.rs
+++ b/scan_core/src/grammar/boolean.rs
@@ -124,7 +124,7 @@ where
     ///
     /// - If a variable is not included in the evaluation;
     /// - If a variable included in the evaluation is not of Boolean type.
-    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option<R>) -> bool {
+    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, mut rng: Option<&mut R>) -> bool {
         match self {
             BooleanExpr::Const(b) => *b,
             BooleanExpr::Var(var) => {
@@ -135,68 +135,68 @@ where
                 }
             }
             BooleanExpr::Rand(float_expr) => {
-                let bernoulli = float_expr.eval(vars, rng);
+                let bernoulli = float_expr.eval(vars, rng.as_deref_mut());
                 rng.as_mut().expect("rng").random_bool(bernoulli)
             }
             BooleanExpr::And(boolean_exprs) => boolean_exprs
                 .iter()
-                .all(|boolean_expr| boolean_expr.eval(vars, rng)),
+                .all(|boolean_expr| boolean_expr.eval(vars, rng.as_deref_mut())),
             BooleanExpr::Or(boolean_exprs) => boolean_exprs
                 .iter()
-                .any(|boolean_expr| boolean_expr.eval(vars, rng)),
+                .any(|boolean_expr| boolean_expr.eval(vars, rng.as_deref_mut())),
             BooleanExpr::Implies(boolean_exprs) => {
                 let (lhs, rhs) = boolean_exprs.as_ref();
-                rhs.eval(vars, rng) || !lhs.eval(vars, rng)
+                rhs.eval(vars, rng.as_deref_mut()) || !lhs.eval(vars, rng)
             }
             BooleanExpr::Not(boolean_expr) => !&boolean_expr.eval(vars, rng),
             BooleanExpr::NatEqual(natural_expr_lhs, natural_expr_rhs) => {
-                natural_expr_lhs.eval(vars, rng) == natural_expr_rhs.eval(vars, rng)
+                natural_expr_lhs.eval(vars, rng.as_deref_mut()) == natural_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::IntEqual(integer_expr_lhs, integer_expr_rhs) => {
-                integer_expr_lhs.eval(vars, rng) == integer_expr_rhs.eval(vars, rng)
+                integer_expr_lhs.eval(vars, rng.as_deref_mut()) == integer_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::FloatEqual(float_expr_lhs, float_expr_rhs) => {
-                float_expr_lhs.eval(vars, rng) == float_expr_rhs.eval(vars, rng)
+                float_expr_lhs.eval(vars, rng.as_deref_mut()) == float_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::NatGreater(natural_expr_lhs, natural_expr_rhs) => {
-                natural_expr_lhs.eval(vars, rng) > natural_expr_rhs.eval(vars, rng)
+                natural_expr_lhs.eval(vars, rng.as_deref_mut()) > natural_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::IntGreater(integer_expr_lhs, integer_expr_rhs) => {
-                integer_expr_lhs.eval(vars, rng) > integer_expr_rhs.eval(vars, rng)
+                integer_expr_lhs.eval(vars, rng.as_deref_mut()) > integer_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::FloatGreater(float_expr_lhs, float_expr_rhs) => {
-                float_expr_lhs.eval(vars, rng) > float_expr_rhs.eval(vars, rng)
+                float_expr_lhs.eval(vars, rng.as_deref_mut()) > float_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::NatGreaterEq(natural_expr_lhs, natural_expr_rhs) => {
-                natural_expr_lhs.eval(vars, rng) >= natural_expr_rhs.eval(vars, rng)
+                natural_expr_lhs.eval(vars, rng.as_deref_mut()) >= natural_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::IntGreaterEq(integer_expr_lhs, integer_expr_rhs) => {
-                integer_expr_lhs.eval(vars, rng) >= integer_expr_rhs.eval(vars, rng)
+                integer_expr_lhs.eval(vars, rng.as_deref_mut()) >= integer_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::FloatGreaterEq(float_expr_lhs, float_expr_rhs) => {
-                float_expr_lhs.eval(vars, rng) >= float_expr_rhs.eval(vars, rng)
+                float_expr_lhs.eval(vars, rng.as_deref_mut()) >= float_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::NatLess(natural_expr_lhs, natural_expr_rhs) => {
-                natural_expr_lhs.eval(vars, rng) < natural_expr_rhs.eval(vars, rng)
+                natural_expr_lhs.eval(vars, rng.as_deref_mut()) < natural_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::IntLess(integer_expr_lhs, integer_expr_rhs) => {
-                integer_expr_lhs.eval(vars, rng) < integer_expr_rhs.eval(vars, rng)
+                integer_expr_lhs.eval(vars, rng.as_deref_mut()) < integer_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::FloatLess(float_expr_lhs, float_expr_rhs) => {
-                float_expr_lhs.eval(vars, rng) < float_expr_rhs.eval(vars, rng)
+                float_expr_lhs.eval(vars, rng.as_deref_mut()) < float_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::NatLessEq(natural_expr_lhs, natural_expr_rhs) => {
-                natural_expr_lhs.eval(vars, rng) <= natural_expr_rhs.eval(vars, rng)
+                natural_expr_lhs.eval(vars, rng.as_deref_mut()) <= natural_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::IntLessEq(integer_expr_lhs, integer_expr_rhs) => {
-                integer_expr_lhs.eval(vars, rng) <= integer_expr_rhs.eval(vars, rng)
+                integer_expr_lhs.eval(vars, rng.as_deref_mut()) <= integer_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::FloatLessEq(float_expr_lhs, float_expr_rhs) => {
-                float_expr_lhs.eval(vars, rng) <= float_expr_rhs.eval(vars, rng)
+                float_expr_lhs.eval(vars, rng.as_deref_mut()) <= float_expr_rhs.eval(vars, rng)
             }
             BooleanExpr::Ite(args) => {
                 let (ite, lhs, rhs) = args.as_ref();
-                if ite.eval(vars, rng) {
+                if ite.eval(vars, rng.as_deref_mut()) {
                     lhs.eval(vars, rng)
                 } else {
                     rhs.eval(vars, rng)
diff --git a/scan_core/src/grammar/float.rs b/scan_core/src/grammar/float.rs
index d281476..3f6d88e 100644
--- a/scan_core/src/grammar/float.rs
+++ b/scan_core/src/grammar/float.rs
@@ -94,7 +94,7 @@ where
     /// - If a variable included in the evaluation is not of [`Float`] type;
     /// - Division by 0;
     /// - Overflow.
-    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option<R>) -> Float {
+    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, mut rng: Option<&mut R>) -> Float {
         match self {
             FloatExpr::Const(float) => *float,
             FloatExpr::Var(var) => {
@@ -110,29 +110,30 @@ where
             FloatExpr::Int(integer_expr) => integer_expr.eval(vars, rng) as f64,
             FloatExpr::Rand(bounds) => {
                 let (lower_bound_expr, upper_bound_expr) = bounds.as_ref();
-                let lower_bound = lower_bound_expr.eval(vars, rng);
-                let upper_bound = upper_bound_expr.eval(vars, rng);
+                let lower_bound = lower_bound_expr.eval(vars, rng.as_deref_mut());
+                let upper_bound = upper_bound_expr.eval(vars, rng.as_deref_mut());
                 rng.as_mut()
                     .expect("rng")
                     .random_range(lower_bound..upper_bound)
             }
             FloatExpr::Opposite(float_expr) => -float_expr.eval(vars, rng),
-            FloatExpr::Sum(float_exprs) => {
-                float_exprs.iter().map(|expr| expr.eval(vars, rng)).sum()
-            }
+            FloatExpr::Sum(float_exprs) => float_exprs
+                .iter()
+                .map(|expr| expr.eval(vars, rng.as_deref_mut()))
+                .sum(),
             FloatExpr::Product(float_exprs) => float_exprs
                 .iter()
-                .map(|expr| expr.eval(vars, rng))
+                .map(|expr| expr.eval(vars, rng.as_deref_mut()))
                 .product(),
             FloatExpr::Div(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs / rhs
             }
             FloatExpr::Ite(args) => {
                 let (ite, lhs, rhs) = args.as_ref();
-                if ite.eval(vars, rng) {
+                if ite.eval(vars, rng.as_deref_mut()) {
                     lhs.eval(vars, rng)
                 } else {
                     rhs.eval(vars, rng)
@@ -140,13 +141,13 @@ where
             }
             FloatExpr::Min(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.min(rhs)
             }
             FloatExpr::Max(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.max(rhs)
             }
diff --git a/scan_core/src/grammar/integer.rs b/scan_core/src/grammar/integer.rs
index 3a67589..2435c47 100644
--- a/scan_core/src/grammar/integer.rs
+++ b/scan_core/src/grammar/integer.rs
@@ -102,7 +102,7 @@ where
     /// - If a variable included in the evaluation is not of [`Integer`] type;
     /// - Division by 0;
     /// - Overflow.
-    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option<R>) -> Integer {
+    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, mut rng: Option<&mut R>) -> Integer {
         match self {
             IntegerExpr::Const(int) => *int,
             IntegerExpr::Var(var) => {
@@ -115,28 +115,26 @@ where
             IntegerExpr::Nat(natural_expr) => natural_expr.eval(vars, rng) as Integer,
             IntegerExpr::Rand(bounds) => {
                 let (lower_bound_expr, upper_bound_expr) = bounds.as_ref();
-                let lower_bound = lower_bound_expr.eval(vars, rng);
-                let upper_bound = upper_bound_expr.eval(vars, rng);
-                rng.as_mut()
-                    .expect("rng")
-                    .random_range(lower_bound..upper_bound)
+                let lower_bound = lower_bound_expr.eval(vars, rng.as_deref_mut());
+                let upper_bound = upper_bound_expr.eval(vars, rng.as_deref_mut());
+                rng.expect("rng").random_range(lower_bound..upper_bound)
             }
             IntegerExpr::Opposite(integer_expr) => integer_expr.eval(vars, rng).strict_neg(),
-            IntegerExpr::Sum(integer_exprs) => integer_exprs
-                .iter()
-                .fold(0, |acc, expr| acc.strict_add(expr.eval(vars, rng))),
-            IntegerExpr::Product(integer_exprs) => integer_exprs
-                .iter()
-                .fold(1, |acc, expr| acc.strict_mul(expr.eval(vars, rng))),
+            IntegerExpr::Sum(integer_exprs) => integer_exprs.iter().fold(0, |acc, expr| {
+                acc.strict_add(expr.eval(vars, rng.as_deref_mut()))
+            }),
+            IntegerExpr::Product(integer_exprs) => integer_exprs.iter().fold(1, |acc, expr| {
+                acc.strict_mul(expr.eval(vars, rng.as_deref_mut()))
+            }),
             IntegerExpr::Div(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.strict_div(rhs)
             }
             IntegerExpr::Rem(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.strict_rem_euclid(rhs)
             }
@@ -144,7 +142,7 @@ where
             IntegerExpr::Ceil(float_expr) => float_expr.eval(vars, rng).ceil() as Integer,
             IntegerExpr::Ite(args) => {
                 let (ite, lhs, rhs) = args.as_ref();
-                if ite.eval(vars, rng) {
+                if ite.eval(vars, rng.as_deref_mut()) {
                     lhs.eval(vars, rng)
                 } else {
                     rhs.eval(vars, rng)
@@ -152,13 +150,13 @@ where
             }
             IntegerExpr::Min(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.min(rhs)
             }
             IntegerExpr::Max(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.max(rhs)
             }
diff --git a/scan_core/src/grammar/natural.rs b/scan_core/src/grammar/natural.rs
index 4176fbc..91ccc0c 100644
--- a/scan_core/src/grammar/natural.rs
+++ b/scan_core/src/grammar/natural.rs
@@ -92,7 +92,7 @@ where
     /// - If a variable included in the evaluation is not of [`Natural`] type;
     /// - Division by 0;
     /// - Overflow.
-    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option<R>) -> Natural {
+    pub fn eval<R: Rng>(&self, vars: &dyn Fn(V) -> Val, mut rng: Option<&mut R>) -> Natural {
         match self {
             NaturalExpr::Const(nat) => *nat,
             NaturalExpr::Var(var) => {
@@ -104,34 +104,34 @@ where
             }
             NaturalExpr::Rand(bounds) => {
                 let (lower_bound_expr, upper_bound_expr) = bounds.as_ref();
-                let lower_bound = lower_bound_expr.eval(vars, rng);
-                let upper_bound = upper_bound_expr.eval(vars, rng);
+                let lower_bound = lower_bound_expr.eval(vars, rng.as_deref_mut());
+                let upper_bound = upper_bound_expr.eval(vars, rng.as_deref_mut());
                 rng.as_mut()
                     .expect("rng")
                     .random_range(lower_bound..upper_bound)
             }
-            NaturalExpr::Sum(natural_exprs) => natural_exprs
-                .iter()
-                .fold(0, |acc, expr| acc.strict_add(expr.eval(vars, rng))),
-            NaturalExpr::Product(natural_exprs) => natural_exprs
-                .iter()
-                .fold(1, |acc, expr| acc.strict_mul(expr.eval(vars, rng))),
+            NaturalExpr::Sum(natural_exprs) => natural_exprs.iter().fold(0, |acc, expr| {
+                acc.strict_add(expr.eval(vars, rng.as_deref_mut()))
+            }),
+            NaturalExpr::Product(natural_exprs) => natural_exprs.iter().fold(1, |acc, expr| {
+                acc.strict_mul(expr.eval(vars, rng.as_deref_mut()))
+            }),
             NaturalExpr::Rem(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.strict_rem_euclid(rhs)
             }
             NaturalExpr::Div(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs / rhs
             }
             NaturalExpr::Abs(integer_expr) => integer_expr.eval(vars, rng).unsigned_abs(),
             NaturalExpr::Ite(args) => {
                 let (ite, lhs, rhs) = args.as_ref();
-                if ite.eval(vars, rng) {
+                if ite.eval(vars, rng.as_deref_mut()) {
                     lhs.eval(vars, rng)
                 } else {
                     rhs.eval(vars, rng)
@@ -139,13 +139,13 @@ where
             }
             NaturalExpr::Min(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.min(rhs)
             }
             NaturalExpr::Max(args) => {
                 let (lhs_expr, rhs_expr) = args.as_ref();
-                let lhs = lhs_expr.eval(vars, rng);
+                let lhs = lhs_expr.eval(vars, rng.as_deref_mut());
                 let rhs = rhs_expr.eval(vars, rng);
                 lhs.max(rhs)
             }
diff --git a/scan_core/src/lib.rs b/scan_core/src/lib.rs
index 937812b..772f5d9 100644
--- a/scan_core/src/lib.rs
+++ b/scan_core/src/lib.rs
@@ -1,6 +1,8 @@
 //! Implementation of *program graphs* (PG) and *channel systems* (CS) formalisms[^1]
 //! for use in the SCAN model checker.
 //!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+//!
 //! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.
 
 #![warn(missing_docs)]
@@ -11,6 +13,7 @@ mod grammar;
 mod oracle;
 pub mod program_graph;
 mod smc;
+mod time;
 mod tracer;
 mod transition_system;
 
@@ -29,6 +32,7 @@ use std::{
     time::Instant,
 };
 use thiserror::Error;
+pub use time::*;
 pub use tracer::{TraceWriter, Tracer};
 pub use transition_system::{Atom, TransitionSystem, TransitionSystemRun};
 
@@ -36,9 +40,6 @@ const TEMP: &str = ".temp";
 const SUCCESSES: &str = "successes";
 const FAILURES: &str = "failures";
 
-/// The type that represents time.
-pub type Time = u32;
-
 /// Errors that can be returned by a `[Scan]` method
 #[derive(Clone, Copy, Debug, Error)]
 pub enum ScanError {
@@ -50,18 +51,28 @@ pub enum ScanError {
     OutOfBoundsConfidence(f64),
 }
 
-/// The possible outcomes of a model execution.
+/// Final report for a verification run.
 #[derive(Debug, Clone)]
-pub enum RunOutcome {
-    /// The run was not completed because the execution violated an assume.
-    Incomplete,
-    /// The run failed by violating the guarantees corresponding to the given index (if any).
-    Verified(Vec<bool>),
+pub struct Report {
+    /// Total executions run (even partial).
+    pub runs: u32,
+    /// Successful executions.
+    pub successes: u32,
+    /// Failed executions.
+    pub failures: u32,
+    /// Breakdown of violations by property.
+    pub violations: Vec<u32>,
 }
 
+// The possible outcomes of a model execution:
+// - If the run was not completed (because the execution violated an assume), result is `None`.
+// - If the run succeeded, or failed by violating the guarantees, result is `Some(violations)`
+//   where the `violations` carries which (if any) guarantees were violated.
+type RunOutcome = Option<Vec<bool>>;
+
 /// The main type to interface with the verification capabilities of SCAN.
 /// [`Scan`] holds the model, properties and other data necessary to run the verification process.
-/// The type of models and properties is abstracted through the [`Oracle`] trait,
+/// The type of properties is abstracted through the [`Oracle`] trait,
 /// to provide a unified interface.
 #[derive(Debug, Clone)]
 pub struct Scan<O> {
@@ -118,65 +129,53 @@ impl<O> Scan<O> {
     }
 }
 
-impl<O: Oracle> Scan<O> {
-    fn verification(&self, confidence: f64, precision: f64, duration: Time) {
+impl<O: Oracle + Clone> Scan<O> {
+    fn verification(&self, confidence: f64, precision: f64) {
         assert!(0f64 < confidence && confidence < 1f64);
         assert!(0f64 < precision && precision < 1f64);
-        let local_successes;
-        let local_failures;
-
-        let result =
-            self.model
-                .new_run()
-                .experiment(duration, self.oracle.clone(), self.running.clone());
-        if !self.running.load(Ordering::Relaxed) {
-            return;
-        }
-        match result {
-            RunOutcome::Verified(guarantees) => {
-                if guarantees.iter().all(|b| *b) {
-                    local_successes = self.successes.fetch_add(1, Ordering::Relaxed);
-                    local_failures = self.failures.load(Ordering::Relaxed);
-                    // If all guarantees are satisfied, the execution is successful
-                    trace!("runs: {local_successes} successes");
-                } else {
-                    local_successes = self.successes.load(Ordering::Relaxed);
-                    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;
-                            }
-                        },
-                    );
-                    // If guarantee is violated, we have found a counter-example!
-                    trace!("runs: {local_failures} failures");
-                }
+
+        let result = self
+            .model
+            .new_run()
+            .experiment(self.oracle.clone(), self.running.clone());
+        if let Some(guarantees) = result
+            && self.running.load(Ordering::Relaxed)
+        {
+            let local_successes;
+            let local_failures;
+            if guarantees.iter().all(|b| *b) {
+                local_successes = self.successes.fetch_add(1, Ordering::Relaxed);
+                local_failures = self.failures.load(Ordering::Relaxed);
+                // If all guarantees are satisfied, the execution is successful
+                trace!("runs: {local_successes} successes");
+            } else {
+                local_successes = self.successes.load(Ordering::Relaxed);
+                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
+                    .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");
+            }
+            let runs = local_successes + local_failures;
+            // Division by 0 leads to Inf/NaN, which is not less than any other float number
+            // so this actually works as expected even for runs = 0.
+            let avg = local_successes as f64 / runs as f64;
+            if adaptive_bound(avg, confidence, precision) <= runs as f64 {
+                info!("adaptive bound satisfied");
+                self.running.store(false, Ordering::Relaxed);
             }
-            RunOutcome::Incomplete => return,
-        }
-        let runs = local_successes + local_failures;
-        // Avoid division by 0
-        let avg = if runs == 0 {
-            0.5f64
-        } else {
-            local_successes as f64 / runs as f64
-        };
-        if adaptive_bound(avg, confidence, precision) <= runs as f64 {
-            info!("adaptive bound satisfied");
-            self.running.store(false, Ordering::Relaxed);
         }
     }
 
     /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters.
-    pub fn adaptive(
-        &self,
-        confidence: f64,
-        precision: f64,
-        duration: Time,
-    ) -> Result<(), ScanError> {
+    pub fn adaptive(&self, confidence: f64, precision: f64) -> Result<Report, ScanError> {
         if !(0f64 < confidence && confidence < 1f64) {
             return Err(ScanError::OutOfBoundsConfidence(confidence));
         }
@@ -190,19 +189,24 @@ impl<O: Oracle> Scan<O> {
         info!("verification starting");
         let start_time = Instant::now();
 
-        let _ = (0..usize::MAX)
-            .map(|_| self.verification(confidence, precision, duration))
+        let runs = (0..)
+            .map(|_| self.verification(confidence, precision))
             .take_while(|_| self.running.load(Ordering::Relaxed))
-            .count();
+            .count() as u32;
 
         let elapsed = start_time.elapsed();
         info!("verification completed in {elapsed:0.2?}");
-        Ok(())
+        Ok(Report {
+            runs,
+            successes: self.successes(),
+            failures: self.failures(),
+            violations: self.violations(),
+        })
     }
 
     /// Produces and saves the traces for the given number of runs,
     /// using the provided [`Tracer`].
-    pub fn traces<T>(&self, runs: usize, duration: Time, path: PathBuf, model_data: &T::ModelData)
+    pub fn traces<T>(&self, runs: usize, path: PathBuf, model_data: &T::ModelData)
     where
         T: Tracer,
     {
@@ -212,14 +216,14 @@ impl<O: Oracle> Scan<O> {
         create_traces_dirs_tree(path.clone());
 
         (0..runs).for_each(|idx| {
-            self.trace::<T>(duration, path.clone(), model_data, idx);
+            self.trace::<T>(path.clone(), model_data, idx);
         });
 
         let elapsed = start_time.elapsed();
         info!("tracing completed in {elapsed:0.2?}");
     }
 
-    fn trace<T>(&self, duration: u32, mut path: PathBuf, model_data: &T::ModelData, idx: usize)
+    fn trace<T>(&self, mut path: PathBuf, model_data: &T::ModelData, idx: usize)
     where
         T: Tracer,
     {
@@ -236,9 +240,7 @@ impl<O: Oracle> Scan<O> {
             .comment("Scan-generated execution trace")
             .write(file, flate2::Compression::best());
         let tracer = T::init(writer, model_data);
-        if let RunOutcome::Verified(verified) =
-            ts.trace::<T, _>(duration, self.oracle.clone(), tracer, model_data)
-        {
+        if let Some(verified) = ts.trace::<T, _>(self.oracle.clone(), tracer, model_data) {
             let mut new_path = path.clone();
             // pop file name
             new_path.pop();
@@ -257,16 +259,11 @@ impl<O: Oracle> Scan<O> {
 
 impl<O> Scan<O>
 where
-    O: Oracle + Sync,
+    O: Oracle + Clone + Sync,
 {
     /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters,
     /// spawning multiple threads.
-    pub fn par_adaptive(
-        &self,
-        confidence: f64,
-        precision: f64,
-        duration: Time,
-    ) -> Result<(), ScanError> {
+    pub fn par_adaptive(&self, confidence: f64, precision: f64) -> Result<Report, ScanError> {
         if !(0f64 < confidence && confidence < 1f64) {
             return Err(ScanError::OutOfBoundsConfidence(confidence));
         }
@@ -280,27 +277,27 @@ where
         info!("verification starting");
         let start_time = Instant::now();
 
-        let _ = (0..usize::MAX)
+        let runs = (0..usize::MAX)
             .into_par_iter()
-            .map(|_| self.verification(confidence, precision, duration))
+            .map(|_| self.verification(confidence, precision))
             .take_any_while(|_| self.running.load(Ordering::Relaxed))
-            .count();
+            .count() as u32;
 
         let elapsed = start_time.elapsed();
         info!("verification completed in {elapsed:0.2?}");
-        Ok(())
+        Ok(Report {
+            runs,
+            successes: self.successes(),
+            failures: self.failures(),
+            violations: self.violations(),
+        })
     }
 
     /// Produces and saves the traces for the given number of runs,
     /// using the provided [`Tracer`],
     /// spawning multiple threads.
-    pub fn par_traces<T>(
-        &self,
-        runs: usize,
-        duration: Time,
-        path: PathBuf,
-        model_data: &T::ModelData,
-    ) where
+    pub fn par_traces<T>(&self, runs: usize, path: PathBuf, model_data: &T::ModelData)
+    where
         T: Tracer,
         T::ModelData: Sync,
     {
@@ -310,7 +307,7 @@ where
         create_traces_dirs_tree(path.clone());
 
         (0..runs).into_par_iter().for_each(|idx| {
-            self.trace::<T>(duration, path.clone(), model_data, idx);
+            self.trace::<T>(path.clone(), model_data, idx);
         });
 
         let elapsed = start_time.elapsed();
diff --git a/scan_core/src/oracle.rs b/scan_core/src/oracle.rs
index 08899b0..ed6c4a0 100644
--- a/scan_core/src/oracle.rs
+++ b/scan_core/src/oracle.rs
@@ -3,7 +3,7 @@ use crate::Time;
 /// Implementators are induced by a temporal property.
 /// They can update their internal state when fed a new state of a trace,
 /// and establish whether their corresponding property holds on such trace.
-pub trait Oracle: Clone + Sync {
+pub trait Oracle: Sync {
     /// Update the internal state of the [`Oracle`] with the latest state of a temporal trace.
     fn update_state(&mut self, state: &[bool]);
 
diff --git a/scan_core/src/program_graph.rs b/scan_core/src/program_graph.rs
index 33d278f..d2d43e7 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();
 //!
@@ -78,12 +77,14 @@
 //! ```
 
 mod builder;
+mod run;
+mod transitions;
 
-use crate::{Time, grammar::*};
+use crate::{TimeRange, grammar::*};
 pub use builder::*;
-use rand::{Rng, rngs::SmallRng};
-use smallvec::SmallVec;
+pub use run::ProgramGraphRun;
 use thiserror::Error;
+use transitions::TransitionsIterator;
 
 /// The index for [`Location`]s in a [`ProgramGraph`].
 pub type LocationIdx = u32;
@@ -131,14 +132,22 @@ pub struct Var(u16);
 #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
 pub struct Clock(u16);
 
-/// A time constraint given by a clock and, optionally, a lower bound and/or an upper bound.
-pub type TimeConstraint = (Clock, Option<Time>, Option<Time>);
-
 /// An expression using PG's [`Var`] as variables.
 pub type PgExpression = Expression<Var>;
 
 /// A Boolean expression over [`Var`] variables.
-pub type PgGuard = BooleanExpr<Var>;
+type PgGuard = BooleanExpr<Var>;
+
+#[derive(Debug, Clone)]
+enum Effect {
+    Effects(Vec<(Var, Expression<Var>)>, Vec<Clock>),
+    Send(Vec<Expression<Var>>),
+    Receive(Vec<Var>),
+}
+
+type Transition = (Location, Option<BooleanExpr<Var>>, Vec<(Clock, TimeRange)>);
+
+type LocationData = (Vec<(Action, Vec<Transition>)>, Vec<(Clock, TimeRange)>);
 
 /// The error type for operations with [`ProgramGraphBuilder`]s and [`ProgramGraph`]s.
 #[derive(Debug, Clone, Copy, Error)]
@@ -192,21 +201,14 @@ pub enum PgError {
     /// A time invariant is not satisfied.
     #[error("A time invariant is not satisfied")]
     Invariant,
+    /// Program graph is a synchronous composition
+    #[error("synchronous composition")]
+    Sync,
     /// A type error
     #[error("type error")]
     Type(#[source] TypeError),
 }
 
-#[derive(Debug, Clone)]
-enum Effect {
-    // NOTE: Could use a SmallVec for clock resets
-    Effects(Vec<(Var, Expression<Var>)>, Vec<Clock>),
-    Send(SmallVec<[Expression<Var>; 2]>),
-    Receive(SmallVec<[Var; 2]>),
-}
-
-type LocationData = (Vec<(Action, Vec<Transition>)>, Vec<TimeConstraint>);
-
 /// A definition object for a PG.
 /// It represents the abstract definition of a PG.
 ///
@@ -244,7 +246,7 @@ type LocationData = (Vec<(Action, Vec<Transition>)>, Vec<TimeConstraint>);
 /// ```
 #[derive(Debug, Clone)]
 pub struct ProgramGraph {
-    initial_states: SmallVec<[Location; 8]>,
+    initial_states: Vec<Location>,
     effects: Vec<Effect>,
     locations: Vec<LocationData>,
     // Time invariants of each location
@@ -259,12 +261,7 @@ impl ProgramGraph {
     /// The new instance borrows the caller to refer to the PG definition without copying its data,
     /// so that spawning instances is (relatively) inexpensive.
     pub fn new_instance<'def>(&'def self) -> ProgramGraphRun<'def> {
-        ProgramGraphRun {
-            current_states: self.initial_states.clone(),
-            vars: self.vars.clone(),
-            def: self,
-            clocks: vec![0; self.clocks as usize],
-        }
+        ProgramGraphRun::new(self)
     }
 
     // Returns transition's guard.
@@ -275,7 +272,7 @@ impl ProgramGraph {
         pre_state: Location,
         action: Action,
         post_state: Location,
-    ) -> impl Iterator<Item = (Option<&PgGuard>, &[TimeConstraint])> {
+    ) -> impl Iterator<Item = (Option<&PgGuard>, &[(Clock, TimeRange)])> {
         let a_transitions = self.locations[pre_state.0 as usize].0.as_slice();
         a_transitions
             .binary_search_by_key(&action, |&(a, ..)| a)
@@ -292,442 +289,6 @@ impl ProgramGraph {
     }
 }
 
-// WARN: This iterator allocates a [`Vec`] every time `next` is called.
-// To avoid this, one way would be to allocate a vector at creation and return a reference to it
-// for every iteration of next, but this requires "streaming iterators" or analogous solution.
-// TODO: Find a way to implement preallocation (or no allocation).
-struct TransitionsIterator<'a, I: Iterator<Item = (Action, &'a [Transition])>> {
-    iters: Vec<I>,
-    // vals: Vec<&'a [Transition]>,
-}
-
-impl<'a, I: Iterator<Item = (Action, &'a [Transition])>> TransitionsIterator<'a, I> {
-    fn new(iters: Vec<I>) -> Self {
-        Self {
-            // vals: Vec::with_capacity(iters.len()),
-            iters,
-        }
-    }
-}
-
-impl<'a, I: Iterator<Item = (Action, &'a [Transition])>> Iterator for TransitionsIterator<'a, I> {
-    type Item = (Action, Vec<&'a [Transition]>);
-
-    fn next(&mut self) -> Option<Self::Item> {
-        let len = self.iters.len();
-        let (first_a, first_t) = self.iters.first_mut().and_then(|it| it.next())?;
-        let mut first_a = first_a;
-        let mut vals = vec![first_t; len];
-
-        let mut total = 1;
-        let mut i = 0;
-        while total < len {
-            i = (i + 1) % len;
-            let (next_a, next_t) = self
-                .iters
-                .get_mut(i)
-                .expect("i < len")
-                .find(|(a, _)| *a >= first_a)?;
-            if next_a > first_a {
-                first_a = next_a;
-                total = 1;
-            } else {
-                total += 1;
-            }
-            vals[i] = next_t;
-        }
-        Some((first_a, vals))
-    }
-}
-
-/// Representation of a PG that can be executed transition-by-transition.
-///
-/// The structure of the PG cannot be changed,
-/// meaning that it is not possible to introduce new locations, actions, variables, etc.
-/// Though, this restriction makes it so that cloning the [`ProgramGraphRun`] is cheap,
-/// because only the internal state needs to be duplicated.
-#[derive(Debug, Clone)]
-pub struct ProgramGraphRun<'def> {
-    current_states: SmallVec<[Location; 8]>,
-    vars: Vec<Val>,
-    clocks: Vec<Time>,
-    def: &'def ProgramGraph,
-}
-
-impl<'def> ProgramGraphRun<'def> {
-    /// Returns the current location.
-    ///
-    /// ```
-    /// # use scan_core::program_graph::ProgramGraphBuilder;
-    /// // Create a new PG builder
-    /// let mut pg_builder = ProgramGraphBuilder::new();
-    ///
-    /// // The builder is initialized with an initial location
-    /// let initial_loc = pg_builder.new_initial_location();
-    ///
-    /// // Build the PG from its builder
-    /// // The builder is always guaranteed to build a well-defined PG and building cannot fail
-    /// let pg = pg_builder.build();
-    /// let instance = pg.new_instance();
-    ///
-    /// // Execution starts in the initial location
-    /// assert_eq!(instance.current_states().as_slice(), &[initial_loc]);
-    /// ```
-    #[inline]
-    pub fn current_states(&self) -> &SmallVec<[Location; 8]> {
-        &self.current_states
-    }
-
-    /// Iterates over all transitions that can be admitted in the current state.
-    ///
-    /// An admissible transition is characterized by the required action and the post-state
-    /// (the pre-state being necessarily the current state of the machine).
-    /// The guard (if any) is guaranteed to be satisfied.
-    pub fn possible_transitions(
-        &self,
-    ) -> impl Iterator<Item = (Action, impl Iterator<Item = impl Iterator<Item = Location>>)> {
-        let mut last_post_state: Option<Location> = None;
-        let iters = self
-            .current_states
-            .iter()
-            .map(|loc| {
-                self.def.locations[loc.0 as usize]
-                    .0
-                    .iter()
-                    .map(|(action, transitions)| (*action, transitions.as_slice()))
-            })
-            .collect::<Vec<_>>();
-        TransitionsIterator::new(iters).map(move |(action, loc_transitions)| {
-            (
-                action,
-                loc_transitions.into_iter().map(move |transitions| {
-                    transitions
-                        .iter()
-                        .filter_map(move |(post_state, guard, constraints)| {
-                            // prevent post_states to be duplicated wastefully
-                            if last_post_state.is_some_and(|s| s == *post_state) {
-                                return None;
-                            }
-                            let (_, ref invariants) = self.def.locations[post_state.0 as usize];
-                            if if action == EPSILON {
-                                self.active_autonomous_transition(
-                                    guard.as_ref(),
-                                    constraints,
-                                    invariants,
-                                )
-                            } else {
-                                match self.def.effects[action.0 as usize] {
-                                    Effect::Effects(_, ref resets) => self.active_transition(
-                                        guard.as_ref(),
-                                        constraints,
-                                        invariants,
-                                        resets,
-                                    ),
-                                    Effect::Send(_) | Effect::Receive(_) => self
-                                        .active_autonomous_transition(
-                                            guard.as_ref(),
-                                            constraints,
-                                            invariants,
-                                        ),
-                                }
-                            } {
-                                last_post_state = Some(*post_state);
-                                last_post_state
-                                // Some(*post_state)
-                            } else {
-                                None
-                            }
-                        })
-                }),
-            )
-        })
-        // self.current_states
-        //     .first()
-        //     .into_iter()
-        //     .flat_map(|loc| {
-        //         self.def.locations[loc.0 as usize]
-        //             .0
-        //             .iter()
-        //             .map(|&(action, ..)| action)
-        //     })
-        //     .chain(
-        //         self.current_states
-        //             .is_empty()
-        //             .then(|| (0..self.def.effects.len() as ActionIdx).map(Action))
-        //             .into_iter()
-        //             .flatten(),
-        //     )
-        // .map(|action| (action, self.possible_transitions_action(action)))
-    }
-
-    pub(crate) fn nosync_possible_transitions(
-        &self,
-    ) -> impl Iterator<Item = (Action, impl Iterator<Item = Location>)> {
-        assert_eq!(self.current_states.len(), 1);
-        let current_loc = self.current_states[0];
-        let mut last_post_state: Option<Location> = None;
-        self.def.locations[current_loc.0 as usize]
-            .0
-            .iter()
-            .map(move |(action, transitions)| {
-                (
-                    *action,
-                    transitions
-                        .iter()
-                        .filter_map(move |(post_state, guard, constraints)| {
-                            // prevent post_states to be duplicated wastefully
-                            if last_post_state.is_some_and(|s| s == *post_state) {
-                                return None;
-                            }
-                            let (_, ref invariants) = self.def.locations[post_state.0 as usize];
-                            if if *action == EPSILON {
-                                self.active_autonomous_transition(
-                                    guard.as_ref(),
-                                    constraints,
-                                    invariants,
-                                )
-                            } else {
-                                match self.def.effects[action.0 as usize] {
-                                    Effect::Effects(_, ref resets) => self.active_transition(
-                                        guard.as_ref(),
-                                        constraints,
-                                        invariants,
-                                        resets,
-                                    ),
-                                    Effect::Send(_) | Effect::Receive(_) => self
-                                        .active_autonomous_transition(
-                                            guard.as_ref(),
-                                            constraints,
-                                            invariants,
-                                        ),
-                                }
-                            } {
-                                last_post_state = Some(*post_state);
-                                last_post_state
-                            } else {
-                                None
-                            }
-                        }),
-                )
-            })
-    }
-
-    #[inline]
-    fn active_transition(
-        &self,
-        guard: Option<&PgGuard>,
-        constraints: &[TimeConstraint],
-        invariants: &[TimeConstraint],
-        resets: &[Clock],
-    ) -> bool {
-        guard.is_none_or(|guard| {
-            // TODO FIXME: is there a way to avoid creating a dummy RNG?
-            guard.eval::<SmallRng>(&|var| self.vars[var.0 as usize], &mut None)
-        }) && constraints.iter().all(|(c, l, u)| {
-            let time = self.clocks[c.0 as usize];
-            l.is_none_or(|l| l <= time) && u.is_none_or(|u| time < u)
-        }) && invariants.iter().all(|(c, l, u)| {
-            let time = if resets.binary_search(c).is_ok() {
-                0
-            } else {
-                self.clocks[c.0 as usize]
-            };
-            l.is_none_or(|l| l <= time) && u.is_none_or(|u| time < u)
-        })
-    }
-
-    #[inline]
-    fn active_autonomous_transition(
-        &self,
-        guard: Option<&PgGuard>,
-        constraints: &[TimeConstraint],
-        invariants: &[TimeConstraint],
-    ) -> bool {
-        guard.is_none_or(|guard| {
-            // TODO FIXME: is there a way to avoid creating a dummy RNG?
-            guard.eval::<SmallRng>(&|var| self.vars[var.0 as usize], &mut None)
-        }) && constraints.iter().chain(invariants).all(|(c, l, u)| {
-            let time = self.clocks[c.0 as usize];
-            l.is_none_or(|l| l <= time) && u.is_none_or(|u| time < u)
-        })
-    }
-
-    fn active_transitions(
-        &self,
-        action: Action,
-        post_states: &[Location],
-        resets: &[Clock],
-    ) -> bool {
-        self.current_states
-            .iter()
-            .zip(post_states)
-            .all(|(current_state, post_state)| {
-                self.def
-                    .guards(*current_state, action, *post_state)
-                    .any(|(guard, constraints)| {
-                        self.active_transition(
-                            guard,
-                            constraints,
-                            &self.def.locations[post_state.0 as usize].1,
-                            resets,
-                        )
-                    })
-            })
-    }
-
-    fn active_autonomous_transitions(&self, post_states: &[Location]) -> bool {
-        self.current_states
-            .iter()
-            .zip(post_states)
-            .all(|(current_state, post_state)| {
-                self.def
-                    .guards(*current_state, EPSILON, *post_state)
-                    .any(|(guard, constraints)| {
-                        self.active_autonomous_transition(
-                            guard,
-                            constraints,
-                            &self.def.locations[post_state.0 as usize].1,
-                        )
-                    })
-            })
-    }
-
-    /// Executes a transition characterized by the argument action and post-state.
-    ///
-    /// Fails if the requested transition is not admissible,
-    /// or if the post-location time invariants are violated.
-    pub fn transition<R: Rng>(
-        &mut self,
-        action: Action,
-        post_states: &[Location],
-        rng: &mut R,
-    ) -> Result<(), PgError> {
-        if post_states.len() != self.current_states.len() {
-            return Err(PgError::MismatchingPostStates);
-        }
-        if let Some(ps) = post_states
-            .iter()
-            .find(|ps| ps.0 >= self.def.locations.len() as LocationIdx)
-        {
-            return Err(PgError::MissingLocation(*ps));
-        }
-        if action == EPSILON {
-            if !self.active_autonomous_transitions(post_states) {
-                return Err(PgError::UnsatisfiedGuard);
-            }
-        } else if action.0 >= self.def.effects.len() as LocationIdx {
-            return Err(PgError::MissingAction(action));
-        } else if let Effect::Effects(ref effects, ref resets) = self.def.effects[action.0 as usize]
-        {
-            if self.active_transitions(action, post_states, resets) {
-                let rng = &mut Some(rng);
-                effects.iter().for_each(|(var, effect)| {
-                    self.vars[var.0 as usize] = effect.eval(&|var| self.vars[var.0 as usize], rng)
-                });
-                resets
-                    .iter()
-                    .for_each(|clock| self.clocks[clock.0 as usize] = 0);
-            } else {
-                return Err(PgError::UnsatisfiedGuard);
-            }
-        } else {
-            return Err(PgError::Communication(action));
-        }
-        self.current_states.copy_from_slice(post_states);
-        Ok(())
-    }
-
-    /// Checks if it is possible to wait a given amount of time-units without violating the time invariants.
-    #[inline]
-    pub fn can_wait(&self, delta: Time) -> bool {
-        self.current_states
-            .iter()
-            .flat_map(|current_state| self.def.locations[current_state.0 as usize].1.iter())
-            .all(|(c, l, u)| {
-                // Invariants need to be satisfied during the whole wait.
-                let start_time = self.clocks[c.0 as usize];
-                let end_time = start_time + delta;
-                l.is_none_or(|l| l <= start_time) && u.is_none_or(|u| end_time < u)
-            })
-    }
-
-    /// Waits a given amount of time-units.
-    ///
-    /// Returns error if the waiting would violate the current location's time invariant (if any).
-    #[inline]
-    pub fn wait(&mut self, delta: Time) -> Result<(), PgError> {
-        if self.can_wait(delta) {
-            self.clocks.iter_mut().for_each(|t| *t += delta);
-            Ok(())
-        } else {
-            Err(PgError::Invariant)
-        }
-    }
-
-    pub(crate) fn send<'a, R: Rng>(
-        &'a mut self,
-        action: Action,
-        post_states: &[Location],
-        rng: &'a mut R,
-    ) -> Result<SmallVec<[Val; 2]>, PgError> {
-        if action == EPSILON {
-            Err(PgError::NotSend(action))
-        } else if self.active_transitions(action, post_states, &[]) {
-            if let Effect::Send(effects) = &self.def.effects[action.0 as usize] {
-                let rng = &mut Some(rng);
-                let vals = effects
-                    .iter()
-                    .map(|effect| effect.eval(&|var| self.vars[var.0 as usize], rng))
-                    .collect();
-                self.current_states.copy_from_slice(post_states);
-                Ok(vals)
-            } else {
-                Err(PgError::NotSend(action))
-            }
-        } else {
-            Err(PgError::UnsatisfiedGuard)
-        }
-    }
-
-    pub(crate) fn receive(
-        &mut self,
-        action: Action,
-        post_states: &[Location],
-        vals: &[Val],
-    ) -> Result<(), PgError> {
-        if action == EPSILON {
-            Err(PgError::NotReceive(action))
-        } else if self.active_transitions(action, post_states, &[]) {
-            if let Effect::Receive(ref vars) = self.def.effects[action.0 as usize] {
-                // let var_content = self.vars.get_mut(var.0 as usize).expect("variable exists");
-                if vars.len() == vals.len()
-                    && vals.iter().zip(vars).all(|(val, var)| {
-                        self.vars
-                            .get(var.0 as usize)
-                            .expect("variable exists")
-                            .r#type()
-                            == val.r#type()
-                    })
-                {
-                    vals.iter().zip(vars).for_each(|(&val, var)| {
-                        *self.vars.get_mut(var.0 as usize).expect("variable exists") = val
-                    });
-                    self.current_states.copy_from_slice(post_states);
-                    // self.current_states = post_states;
-                    // self.update_buf();
-                    Ok(())
-                } else {
-                    Err(PgError::TypeMismatch)
-                }
-            } else {
-                Err(PgError::NotReceive(action))
-            }
-        } else {
-            Err(PgError::UnsatisfiedGuard)
-        }
-    }
-}
-
 #[cfg(test)]
 mod tests {
     use rand::SeedableRng;
@@ -746,37 +307,126 @@ mod tests {
     }
 
     #[test]
-    fn transitions() {
+    fn transition() {
         let mut builder = ProgramGraphBuilder::new();
         let initial = builder.new_initial_location();
         let r#final = builder.new_location();
-        let action = builder.new_action();
         builder
-            .add_transition(initial, action, r#final, None)
+            .add_autonomous_transition(initial, r#final, None)
             .expect("add transition");
         let pg_def = builder.build();
         let mut pg = pg_def.new_instance();
-        // assert_eq!(pg.current_states().as_slice(), &[initial]);
-        // assert_eq!(
-        //     pg.possible_transitions().collect::<Vec<_>>(),
-        //     vec![(
-        //         action,
-        //         SmallVec::<[_; 4]>::from(vec![SmallVec::<[_; 8]>::from(vec![r#final])])
-        //     )]
-        // );
+        assert_eq!(pg.current_states(), &[initial]);
+        {
+            let mut possible_transitions = pg.possible_transitions();
+            assert!(
+                possible_transitions
+                    .next()
+                    .is_some_and(|(a, _)| a == EPSILON),
+            );
+            assert!(possible_transitions.next().is_none());
+        }
         let mut rng = SmallRng::from_seed([0; 32]);
-        pg.transition(action, &[r#final], &mut rng)
+        pg.transition(EPSILON, &[r#final], &mut rng)
             .expect("transition to final");
+        assert_eq!(pg.current_states(), &[r#final]);
         assert_eq!(pg.possible_transitions().count(), 0);
     }
 
+    #[test]
+    fn guard() {
+        let mut builder = ProgramGraphBuilder::new();
+        let initial = builder.new_initial_location();
+        let r#final = builder.new_location();
+        builder
+            .add_autonomous_transition(initial, r#final, Some(BooleanExpr::Const(true)))
+            .expect("add transition");
+        builder
+            .add_autonomous_transition(r#final, initial, Some(BooleanExpr::Const(false)))
+            .expect("add transition");
+        let pg_def = builder.build();
+        let mut pg = pg_def.new_instance();
+        let mut rng = SmallRng::from_seed([0; 32]);
+        // It is possible to transition from initial to final
+        pg.transition(EPSILON, &[r#final], &mut rng)
+            .expect("transition to final");
+        assert_eq!(pg.current_states(), &[r#final]);
+        // It is not possible to transition from final to initial
+        let mut possible_transitions = pg.possible_transitions();
+        let (next_action, mut next_locations) = possible_transitions.next().unwrap();
+        assert_eq!(next_action, EPSILON);
+        let mut next_location = next_locations.next().unwrap();
+        assert!(next_location.next().is_none());
+        assert!(possible_transitions.next().is_none());
+    }
+
+    #[test]
+    fn effect() {
+        const TRESHOLD: Natural = 3;
+        let mut builder = ProgramGraphBuilder::new();
+        let initial = builder.new_initial_location();
+        let r#final = builder.new_location();
+        let var = builder.new_var(Val::from(0 as Natural));
+        let action = builder.new_action();
+        builder
+            .add_effect(
+                action,
+                var,
+                Expression::Natural(NaturalExpr::Var(var) + NaturalExpr::Const(1)),
+            )
+            .expect("add effect");
+        builder
+            .add_transition(
+                initial,
+                action,
+                initial,
+                Some(
+                    Expression::from_var(var, Type::Natural)
+                        .less_than(Expression::from(TRESHOLD))
+                        .expect("boolean expression"),
+                ),
+            )
+            .expect("add transition");
+        builder
+            .add_autonomous_transition(
+                initial,
+                r#final,
+                Some(
+                    Expression::from_var(var, Type::Natural)
+                        .equal_to(Expression::from(TRESHOLD))
+                        .expect("boolean expression"),
+                ),
+            )
+            .expect("add transition");
+        let pg_def = builder.build();
+        let mut pg = pg_def.new_instance();
+        let mut rng = SmallRng::from_seed([0; 32]);
+        for _ in 0..TRESHOLD {
+            assert_eq!(pg.current_states(), &[initial]);
+            // It is not possible to transition from initial to final
+            pg.transition(EPSILON, &[r#final], &mut rng)
+                .expect_err("transition to final not possible");
+            // It is possible to transition from initial to initial
+            pg.transition(action, &[initial], &mut rng)
+                .expect("transition to initial");
+        }
+        assert_eq!(pg.current_states(), &[initial]);
+        // It is not possible to transition from initial to initial
+        pg.transition(action, &[initial], &mut rng)
+            .expect_err("transition to initial not possible");
+        // It is possible to transition from initial to final
+        pg.transition(EPSILON, &[r#final], &mut rng)
+            .expect("transition to final");
+        assert_eq!(pg.current_states(), &[r#final]);
+    }
+
     #[test]
     fn program_graph() -> Result<(), PgError> {
         // Create Program Graph
         let mut builder = ProgramGraphBuilder::new();
         // Variables
         let mut rng = SmallRng::from_seed([0; 32]);
-        let battery = builder.new_var(Val::from(0i64))?;
+        let battery = builder.new_var(Val::from(0i64));
         // Locations
         let initial = builder.new_initial_location();
         let left = builder.new_location();
diff --git a/scan_core/src/program_graph/builder.rs b/scan_core/src/program_graph/builder.rs
index bc6afae..be0f955 100644
--- a/scan_core/src/program_graph/builder.rs
+++ b/scan_core/src/program_graph/builder.rs
@@ -1,27 +1,21 @@
-use super::{
-    Action, ActionIdx, Clock, EPSILON, Effect, Location, LocationData, LocationIdx, PgError,
-    PgExpression, ProgramGraph, TimeConstraint, Var,
-};
-use crate::{
-    grammar::{BooleanExpr, Type, Val},
-    program_graph::PgGuard,
-};
+use std::{collections::BTreeMap, ops::RangeBounds};
+
+use super::*;
+use crate::grammar::{Type, Val};
 use log::info;
-use smallvec::SmallVec;
 
-// type TransitionBuilder = (Location, Option<PgExpression>, Vec<TimeConstraint>);
-pub(crate) type Transition = (Location, Option<BooleanExpr<Var>>, Vec<TimeConstraint>);
+type LocationBuilderData = (BTreeMap<Action, Vec<Transition>>, Vec<(Clock, TimeRange)>);
 
 /// Defines and builds a PG.
 #[derive(Debug, Clone)]
 pub struct ProgramGraphBuilder {
     // initial_states: Vec<Location>,
-    initial_states: SmallVec<[Location; 8]>,
+    initial_states: Vec<Location>,
     // Effects are indexed by actions
     effects: Vec<Effect>,
     // Transitions are indexed by locations
     // Time invariants of each location
-    locations: Vec<LocationData>,
+    locations: Vec<LocationBuilderData>,
     // Local variables with initial value.
     vars: Vec<Val>,
     // Number of clocks
@@ -39,7 +33,7 @@ impl ProgramGraphBuilder {
     /// At creation, this will only have the initial location with no variables, no actions and no transitions.
     pub fn new() -> Self {
         Self {
-            initial_states: SmallVec::new(),
+            initial_states: Vec::new(),
             effects: Vec::new(),
             vars: Vec::new(),
             locations: Vec::new(),
@@ -56,9 +50,6 @@ impl ProgramGraphBuilder {
     }
 
     /// Adds a new variable with the given initial value (and the inferred type) to the PG.
-    /// It creates and uses a default RNG for probabilistic expressions.
-    ///
-    /// It fails if the expression giving the initial value of the variable is not well-typed.
     ///
     /// ```
     /// # use scan_core::program_graph::{PgExpression, ProgramGraphBuilder};
@@ -71,13 +62,12 @@ impl ProgramGraphBuilder {
     ///
     /// // Create a new variable
     /// let var = pg_builder
-    ///     .new_var(val)
-    ///     .unwrap();
+    ///     .new_var(val);
     /// ```
-    pub fn new_var(&mut self, val: Val) -> Result<Var, PgError> {
+    pub fn new_var(&mut self, val: Val) -> Var {
         let idx = self.vars.len();
         self.vars.push(val);
-        Ok(Var(idx as u16))
+        Var(idx as u16)
     }
 
     /// Adds a new clock and returns a [`Clock`] id object.
@@ -199,7 +189,7 @@ impl ProgramGraphBuilder {
         }
     }
 
-    pub(crate) fn new_send(&mut self, msgs: Vec<PgExpression>) -> Result<Action, PgError> {
+    pub(crate) fn new_send(&mut self, mut msgs: Vec<PgExpression>) -> Result<Action, PgError> {
         // Check message is well-typed
         msgs.iter()
             .try_for_each(|msg| {
@@ -208,17 +198,19 @@ impl ProgramGraphBuilder {
             .map_err(PgError::Type)?;
         // Actions are indexed progressively
         let idx = self.effects.len();
-        self.effects.push(Effect::Send(msgs.into()));
+        msgs.shrink_to_fit();
+        self.effects.push(Effect::Send(msgs));
         Ok(Action(idx as ActionIdx))
     }
 
-    pub(crate) fn new_receive(&mut self, vars: Vec<Var>) -> Result<Action, PgError> {
+    pub(crate) fn new_receive(&mut self, mut vars: Vec<Var>) -> Result<Action, PgError> {
         if let Some(var) = vars.iter().find(|var| self.vars.len() as u16 <= var.0) {
             Err(PgError::MissingVar(var.to_owned()))
         } else {
             // Actions are indexed progressively
             let idx = self.effects.len();
-            self.effects.push(Effect::Receive(vars.into()));
+            vars.shrink_to_fit();
+            self.effects.push(Effect::Receive(vars));
             Ok(Action(idx as ActionIdx))
         }
     }
@@ -234,14 +226,16 @@ impl ProgramGraphBuilder {
     /// and returns its [`Location`] indexing object.
     pub fn new_timed_location(
         &mut self,
-        invariants: Vec<TimeConstraint>,
+        mut invariants: Vec<(Clock, TimeRange)>,
     ) -> Result<Location, PgError> {
-        if let Some((clock, _, _)) = invariants.iter().find(|(c, _, _)| c.0 >= self.clocks) {
+        if let Some((clock, _)) = invariants.iter().find(|(c, _)| c.0 >= self.clocks) {
             Err(PgError::MissingClock(*clock))
         } else {
             // Locations are indexed progressively
             let idx = self.locations.len();
-            self.locations.push((Vec::new(), invariants));
+            invariants.sort_unstable_by_key(|(c, _)| *c);
+            invariants.shrink_to_fit();
+            self.locations.push((BTreeMap::new(), invariants));
             Ok(Location(idx as LocationIdx))
         }
     }
@@ -253,9 +247,9 @@ impl ProgramGraphBuilder {
             .ok_or(PgError::MissingLocation(location))?
             .1 // location's time invariants
             .iter()
-            .all(|(_, l, u)| {
+            .all(|(_, range)| {
                 // All clocks start at time 0
-                l.is_none_or(|l| l == 0) && u.is_none_or(|u| u > 0)
+                range.contains(&0)
             })
             .then(|| self.initial_states.push(location))
             .ok_or(PgError::Invariant)
@@ -272,7 +266,7 @@ impl ProgramGraphBuilder {
     /// and returns the [`Location`] indexing object.
     pub fn new_initial_timed_location(
         &mut self,
-        invariants: Vec<TimeConstraint>,
+        invariants: Vec<(Clock, TimeRange)>,
     ) -> Result<Location, PgError> {
         let location = self.new_timed_location(invariants)?;
         self.new_process(location)?;
@@ -351,7 +345,7 @@ impl ProgramGraphBuilder {
         action: Action,
         post: Location,
         guard: Option<PgGuard>,
-        constraints: Vec<TimeConstraint>,
+        mut constraints: Vec<(Clock, TimeRange)>,
     ) -> Result<(), PgError> {
         // Check 'pre' and 'post' locations exists
         if self.locations.len() as LocationIdx <= pre.0 {
@@ -361,8 +355,7 @@ impl ProgramGraphBuilder {
         } else if action != EPSILON && self.effects.len() as ActionIdx <= action.0 {
             // Check 'action' exists
             Err(PgError::MissingAction(action))
-        } else if let Some((clock, _, _)) = constraints.iter().find(|(c, _, _)| c.0 >= self.clocks)
-        {
+        } else if let Some((clock, _)) = constraints.iter().find(|(c, _)| c.0 >= self.clocks) {
             Err(PgError::MissingClock(*clock))
         } else {
             if let Some(ref guard) = guard {
@@ -371,13 +364,17 @@ impl ProgramGraphBuilder {
                     .map_err(PgError::Type)?;
             }
             let (transitions, _) = &mut self.locations[pre.0 as usize];
+            constraints.sort_unstable_by_key(|(c, _)| *c);
+            constraints.shrink_to_fit();
             let transition = (post, guard, constraints);
             // WARN: Actions have to be inserted in order but insertion has worst-case complexity O(n)
             // so in some cases insertion of all actions could have complexity O(n^2).
             // In practice though this is unlikely to ever be a bottleneck
-            match transitions.binary_search_by_key(&action, |(a, _)| *a) {
-                Ok(idx) => transitions[idx].1.push(transition),
-                Err(idx) => transitions.insert(idx, (action, vec![transition])),
+            match transitions.get_mut(&action) {
+                Some(action_transitions) => action_transitions.push(transition),
+                None => {
+                    let _ = transitions.insert(action, vec![transition]);
+                }
             }
             Ok(())
         }
@@ -447,7 +444,7 @@ impl ProgramGraphBuilder {
         pre: Location,
         post: Location,
         guard: Option<PgGuard>,
-        constraints: Vec<TimeConstraint>,
+        constraints: Vec<(Clock, TimeRange)>,
     ) -> Result<(), PgError> {
         self.add_timed_transition(pre, EPSILON, post, guard, constraints)
     }
@@ -459,45 +456,43 @@ impl ProgramGraphBuilder {
     pub fn build(mut self) -> ProgramGraph {
         // Since vectors of effects and transitions will become immutable,
         // they should be shrunk to take as little space as possible
+        self.initial_states.shrink_to_fit();
+        self.vars.shrink_to_fit();
         self.effects.iter_mut().for_each(|effect| {
             if let Effect::Effects(_, resets) = effect {
                 resets.sort_unstable();
+                resets.shrink_to_fit();
             }
         });
         self.effects.shrink_to_fit();
-        self.vars.shrink_to_fit();
-        self.locations
-            .iter_mut()
-            .for_each(|(transitions, invariants)| {
-                assert!(transitions.is_sorted_by_key(|(action, ..)| *action));
-                transitions
-                    .iter_mut()
-                    .for_each(|(_action, loc_transitions)| {
-                        loc_transitions.sort_unstable_by_key(|(p, ..)| *p);
-                        loc_transitions
-                            .iter_mut()
-                            .for_each(|(_p, _guard, time_guards)| {
-                                time_guards.sort_unstable();
-                            });
-                    });
+        let mut locations = self
+            .locations
+            .into_iter()
+            .map(|(transitions, loc_invariants)| {
+                let mut transitions = Vec::from_iter(transitions);
                 transitions.shrink_to_fit();
-                invariants.sort_unstable();
-                invariants.shrink_to_fit();
-            });
-        self.locations.shrink_to_fit();
+                transitions.iter_mut().for_each(|(_, loc_transitions)| {
+                    assert!(!loc_transitions.is_empty());
+                    loc_transitions.sort_unstable_by_key(|(p, ..)| *p);
+                    loc_transitions.shrink_to_fit();
+                });
+                // Actions are assumed to be sorted
+                assert!(transitions.is_sorted_by_key(|(action, _)| *action));
+                (transitions, loc_invariants)
+            })
+            .collect::<Vec<_>>();
+        locations.shrink_to_fit();
         // Build program graph
         info!(
             "create Program Graph with: {} locations; {} actions; {} vars",
-            self.locations.len(),
+            locations.len(),
             self.effects.len(),
             self.vars.len()
         );
-        self.initial_states.sort_unstable();
-        self.initial_states.shrink_to_fit();
         ProgramGraph {
             initial_states: self.initial_states,
             effects: self.effects,
-            locations: self.locations,
+            locations,
             vars: self.vars,
             clocks: self.clocks,
         }
diff --git a/scan_core/src/program_graph/run.rs b/scan_core/src/program_graph/run.rs
new file mode 100644
index 0000000..ed07b69
--- /dev/null
+++ b/scan_core/src/program_graph/run.rs
@@ -0,0 +1,410 @@
+use std::ops::{Bound, RangeBounds};
+
+use bumpalo::{Bump, collections::CollectIn};
+use rand::{Rng, rngs::SmallRng};
+
+use super::{
+    Action, Clock, EPSILON, Effect, Location, LocationIdx, PgError, PgGuard, ProgramGraph,
+    Transition, TransitionsIterator, Var,
+};
+use crate::{BooleanExpr, Time, Val, program_graph::TimeRange};
+
+/// Representation of a PG that can be executed transition-by-transition.
+///
+/// The structure of the PG cannot be changed,
+/// meaning that it is not possible to introduce new locations, actions, variables, etc.
+/// Though, this restriction makes it so that cloning the [`ProgramGraphRun`] is cheap,
+/// because only the internal state needs to be duplicated.
+#[derive(Debug)]
+pub struct ProgramGraphRun<'def> {
+    current_states: Vec<Location>,
+    vars: Vec<Val>,
+    clocks: Vec<Time>,
+    def: &'def ProgramGraph,
+    bump: Bump,
+}
+
+impl<'def> Clone for ProgramGraphRun<'def> {
+    fn clone(&self) -> Self {
+        Self {
+            current_states: self.current_states.clone(),
+            vars: self.vars.clone(),
+            clocks: self.clocks.clone(),
+            def: self.def,
+            bump: Bump::new(),
+        }
+    }
+}
+
+impl<'def> ProgramGraphRun<'def> {
+    /// Create a new executions from a given PG definition.
+    pub fn new(program_graph: &'def ProgramGraph) -> Self {
+        Self {
+            current_states: program_graph.initial_states.clone(),
+            vars: program_graph.vars.clone(),
+            clocks: vec![0; program_graph.clocks as usize],
+            def: program_graph,
+            bump: Bump::new(),
+        }
+    }
+
+    /// Returns the current location.
+    ///
+    /// ```
+    /// # use scan_core::program_graph::ProgramGraphBuilder;
+    /// // Create a new PG builder
+    /// let mut pg_builder = ProgramGraphBuilder::new();
+    ///
+    /// // The builder is initialized with an initial location
+    /// let initial_loc = pg_builder.new_initial_location();
+    ///
+    /// // Build the PG from its builder
+    /// // The builder is always guaranteed to build a well-defined PG and building cannot fail
+    /// let pg = pg_builder.build();
+    /// let instance = pg.new_instance();
+    ///
+    /// // Execution starts in the initial location
+    /// assert_eq!(instance.current_states().as_slice(), &[initial_loc]);
+    /// ```
+    #[inline]
+    pub fn current_states(&self) -> &[Location] {
+        &self.current_states
+    }
+
+    #[inline]
+    fn transitions<'a>(
+        &'a self,
+    ) -> TransitionsIterator<'a, impl Iterator<Item = &'a (Action, Vec<Transition>)>> {
+        let iters = self
+            .current_states
+            .iter()
+            .map(|loc| self.def.locations[loc.0 as usize].0.iter())
+            .collect_in::<bumpalo::collections::Vec<_>>(&self.bump)
+            .into_bump_slice_mut();
+        TransitionsIterator::new(iters, &self.bump)
+    }
+
+    /// Iterates over all transitions that can be admitted in the current state.
+    ///
+    /// An admissible transition is characterized by the required action and the post-state
+    /// (the pre-state being necessarily the current state of the machine).
+    /// The guard (if any) is guaranteed to be satisfied.
+    pub fn possible_transitions(
+        &self,
+    ) -> impl Iterator<Item = (Action, impl Iterator<Item = impl Iterator<Item = Location>>)> {
+        self.transitions().map(move |(action, loc_transitions)| {
+            (
+                action,
+                loc_transitions.iter().map(move |transitions| {
+                    transitions
+                        .iter()
+                        .filter(move |(post_state, guard, constraints)| {
+                            self.check_transition(action, *post_state, guard.as_ref(), constraints)
+                        })
+                        .map(|(post_state, ..)| *post_state)
+                }),
+            )
+        })
+    }
+
+    /// Iterates over all transitions that can be admitted in the current state,
+    /// optimized for the special (but common) case in which the state is given by a single location.
+    ///
+    /// An admissible transition is characterized by the required action and the post-state
+    /// (the pre-state being necessarily the current state of the machine).
+    /// The guard (if any) is guaranteed to be satisfied.
+    ///
+    /// Returns error if the state is not given by a single location.
+    pub fn nosync_possible_transitions(
+        &self,
+    ) -> Result<impl Iterator<Item = (Action, impl Iterator<Item = Location>)>, PgError> {
+        if self.current_states.len() == 1 {
+            let current_loc = self.current_states[0];
+            Ok(self.def.locations[current_loc.0 as usize].0.iter().map(
+                move |(action, transitions)| {
+                    (
+                        *action,
+                        transitions
+                            .iter()
+                            .filter(move |(post_state, guard, constraints)| {
+                                self.check_transition(
+                                    *action,
+                                    *post_state,
+                                    guard.as_ref(),
+                                    constraints,
+                                )
+                            })
+                            .map(|(post_state, ..)| *post_state),
+                    )
+                },
+            ))
+        } else {
+            Err(PgError::Sync)
+        }
+    }
+
+    fn check_transition(
+        &self,
+        action: Action,
+        post_state: Location,
+        guard: Option<&BooleanExpr<Var>>,
+        constraints: &[(Clock, TimeRange)],
+    ) -> bool {
+        let (_, ref invariants) = self.def.locations[post_state.0 as usize];
+        if action != EPSILON
+            && let Effect::Effects(_, ref resets) = self.def.effects[action.0 as usize]
+        {
+            self.active_transition(guard, constraints, invariants, resets)
+        } else {
+            self.active_autonomous_transition(guard, constraints, invariants)
+        }
+    }
+
+    fn active_transition(
+        &self,
+        guard: Option<&PgGuard>,
+        constraints: &[(Clock, TimeRange)],
+        invariants: &[(Clock, TimeRange)],
+        resets: &[Clock],
+    ) -> bool {
+        guard.is_none_or(|guard| guard.eval::<SmallRng>(&|var| self.vars[var.0 as usize], None))
+            && constraints.iter().all(|(c, range)| {
+                let time = self.clocks[c.0 as usize];
+                range.contains(&time)
+            })
+            && invariants.iter().all(|(c, range)| {
+                let time = if resets.binary_search(c).is_ok() {
+                    0
+                } else {
+                    self.clocks[c.0 as usize]
+                };
+                range.contains(&time)
+            })
+    }
+
+    #[inline]
+    fn active_autonomous_transition(
+        &self,
+        guard: Option<&PgGuard>,
+        constraints: &[(Clock, TimeRange)],
+        invariants: &[(Clock, TimeRange)],
+    ) -> bool {
+        guard.is_none_or(|guard| guard.eval::<SmallRng>(&|var| self.vars[var.0 as usize], None))
+            && constraints.iter().chain(invariants).all(|(c, range)| {
+                let time = self.clocks[c.0 as usize];
+                range.contains(&time)
+            })
+    }
+
+    fn active_transitions(
+        &self,
+        action: Action,
+        post_states: &[Location],
+        resets: &[Clock],
+    ) -> bool {
+        self.current_states
+            .iter()
+            .zip(post_states)
+            .all(|(current_state, post_state)| {
+                self.def
+                    .guards(*current_state, action, *post_state)
+                    .any(|(guard, constraints)| {
+                        self.active_transition(
+                            guard,
+                            constraints,
+                            &self.def.locations[post_state.0 as usize].1,
+                            resets,
+                        )
+                    })
+            })
+    }
+
+    fn active_autonomous_transitions(&self, post_states: &[Location]) -> bool {
+        self.current_states
+            .iter()
+            .zip(post_states)
+            .all(|(current_state, post_state)| {
+                self.def
+                    .guards(*current_state, EPSILON, *post_state)
+                    .any(|(guard, constraints)| {
+                        self.active_autonomous_transition(
+                            guard,
+                            constraints,
+                            &self.def.locations[post_state.0 as usize].1,
+                        )
+                    })
+            })
+    }
+
+    /// Executes a transition characterized by the argument action and post-state.
+    ///
+    /// Fails if the requested transition is not admissible,
+    /// or if the post-location time invariants are violated.
+    pub fn transition<R: Rng>(
+        &mut self,
+        action: Action,
+        post_states: &[Location],
+        rng: &mut R,
+    ) -> Result<(), PgError> {
+        self.bump.reset();
+        if post_states.len() != self.current_states.len() {
+            return Err(PgError::MismatchingPostStates);
+        }
+        if let Some(ps) = post_states
+            .iter()
+            .find(|ps| ps.0 >= self.def.locations.len() as LocationIdx)
+        {
+            return Err(PgError::MissingLocation(*ps));
+        }
+        if action == EPSILON {
+            if !self.active_autonomous_transitions(post_states) {
+                return Err(PgError::UnsatisfiedGuard);
+            }
+        } else if action.0 >= self.def.effects.len() as LocationIdx {
+            return Err(PgError::MissingAction(action));
+        } else if let Effect::Effects(ref effects, ref resets) = self.def.effects[action.0 as usize]
+        {
+            if self.active_transitions(action, post_states, resets) {
+                effects.iter().for_each(|(var, effect)| {
+                    self.vars[var.0 as usize] =
+                        effect.eval(&|var| self.vars[var.0 as usize], Some(rng))
+                });
+                resets
+                    .iter()
+                    .for_each(|clock| self.clocks[clock.0 as usize] = 0);
+            } else {
+                return Err(PgError::UnsatisfiedGuard);
+            }
+        } else {
+            return Err(PgError::Communication(action));
+        }
+        self.current_states.copy_from_slice(post_states);
+        Ok(())
+    }
+
+    /// Checks if it is possible to wait a given amount of time-units without violating the time invariants.
+    #[inline]
+    pub fn can_wait(&self, delta: Time) -> bool {
+        self.current_states
+            .iter()
+            .flat_map(|current_state| self.def.locations[current_state.0 as usize].1.iter())
+            .all(|(c, range)| {
+                // Invariants need to be satisfied during the whole wait.
+                let start_time = self.clocks[c.0 as usize];
+                let end_time = start_time + delta;
+                // range.contains(&start_time) &&
+                range.contains(&end_time)
+            })
+    }
+
+    /// Waits a given amount of time-units.
+    ///
+    /// Returns error if the waiting would violate the current location's time invariant (if any).
+    #[inline]
+    pub fn wait(&mut self, delta: Time) -> Result<(), PgError> {
+        self.bump.reset();
+        if self.can_wait(delta) {
+            self.clocks.iter_mut().for_each(|t| *t += delta);
+            Ok(())
+        } else {
+            Err(PgError::Invariant)
+        }
+    }
+
+    pub(crate) fn send<'a, R: Rng>(
+        &'a mut self,
+        action: Action,
+        post_states: &[Location],
+        rng: &'a mut R,
+    ) -> Result<Vec<Val>, PgError> {
+        self.bump.reset();
+        if action == EPSILON {
+            Err(PgError::NotSend(action))
+        } else if self.active_transitions(action, post_states, &[]) {
+            if let Effect::Send(effects) = &self.def.effects[action.0 as usize] {
+                let vals = effects
+                    .iter()
+                    .map(|effect| effect.eval(&|var| self.vars[var.0 as usize], Some(rng)))
+                    .collect();
+                self.current_states.copy_from_slice(post_states);
+                Ok(vals)
+            } else {
+                Err(PgError::NotSend(action))
+            }
+        } else {
+            Err(PgError::UnsatisfiedGuard)
+        }
+    }
+
+    pub(crate) fn receive(
+        &mut self,
+        action: Action,
+        post_states: &[Location],
+        vals: &[Val],
+    ) -> Result<(), PgError> {
+        self.bump.reset();
+        if action == EPSILON {
+            Err(PgError::NotReceive(action))
+        } else if self.active_transitions(action, post_states, &[]) {
+            if let Effect::Receive(ref vars) = self.def.effects[action.0 as usize] {
+                // let var_content = self.vars.get_mut(var.0 as usize).expect("variable exists");
+                if vars.len() == vals.len()
+                    && vals.iter().zip(vars).all(|(val, var)| {
+                        self.vars
+                            .get(var.0 as usize)
+                            .expect("variable exists")
+                            .r#type()
+                            == val.r#type()
+                    })
+                {
+                    vals.iter().zip(vars).for_each(|(&val, var)| {
+                        *self.vars.get_mut(var.0 as usize).expect("variable exists") = val
+                    });
+                    self.current_states.copy_from_slice(post_states);
+                    Ok(())
+                } else {
+                    Err(PgError::TypeMismatch)
+                }
+            } else {
+                Err(PgError::NotReceive(action))
+            }
+        } else {
+            Err(PgError::UnsatisfiedGuard)
+        }
+    }
+
+    /// Returns `true` if there is any transition from the current state that will be unlocked at some point in the future,
+    /// either because of a temporal guard on the transition becoming true, or a time invariant on the post-location becoming true.
+    pub fn is_waiting(&self) -> bool {
+        let unsatisfied_lower_bound = |(c, range): &(Clock, TimeRange)| {
+            let time = self.clocks[c.0 as usize];
+            let bound = range.start_bound();
+            match bound {
+                Bound::Included(b) => time < *b,
+                Bound::Excluded(b) => time <= *b,
+                Bound::Unbounded => false,
+            }
+        };
+        let satisfied_upper_bound = |(c, range): &(Clock, TimeRange)| {
+            let time = self.clocks[c.0 as usize];
+            let bound = range.end_bound();
+            match bound {
+                Bound::Included(b) => time <= *b,
+                Bound::Excluded(b) => time < *b,
+                Bound::Unbounded => true,
+            }
+        };
+        self.can_wait(1)
+            && self.transitions().any(move |(_, loc_transitions)| {
+                loc_transitions.iter().any(move |transitions| {
+                    transitions.iter().any(move |(post_state, _, constraints)| {
+                        let invariants = self.def.locations[post_state.0 as usize].1.as_slice();
+                        (constraints.iter().any(unsatisfied_lower_bound)
+                            && constraints.iter().all(satisfied_upper_bound))
+                            || (invariants.iter().any(unsatisfied_lower_bound)
+                                && invariants.iter().all(satisfied_upper_bound))
+                    })
+                })
+            })
+    }
+}
diff --git a/scan_core/src/program_graph/transitions.rs b/scan_core/src/program_graph/transitions.rs
new file mode 100644
index 0000000..a6dd811
--- /dev/null
+++ b/scan_core/src/program_graph/transitions.rs
@@ -0,0 +1,40 @@
+use bumpalo::Bump;
+
+use crate::program_graph::{Action, Transition};
+
+pub(super) struct TransitionsIterator<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> {
+    iters: &'a mut [I],
+    bump: &'a Bump,
+    action: Action,
+}
+
+impl<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> TransitionsIterator<'a, I> {
+    pub(super) fn new(iters: &'a mut [I], bump: &'a Bump) -> Self {
+        Self {
+            iters,
+            bump,
+            action: Action(0),
+        }
+    }
+}
+
+impl<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> Iterator
+    for TransitionsIterator<'a, I>
+{
+    type Item = (Action, &'a [&'a [Transition]]);
+
+    fn next(&mut self) -> Option<Self::Item> {
+        let len = self.iters.len();
+        let mut total = 0;
+        let mut i = 0;
+        let mut vals = bumpalo::vec![in self.bump; [].as_slice(); len];
+        while total < len {
+            let &(next_a, ref next_t) = self.iters[i].find(|&&(a, _)| a.0 >= self.action.0)?;
+            vals[i] = next_t.as_slice();
+            i = (i + 1) % len;
+            total = total * (next_a.0 == self.action.0) as usize + 1;
+            self.action = next_a;
+        }
+        Some((self.action, vals.into_bump_slice()))
+    }
+}
diff --git a/scan_core/src/time.rs b/scan_core/src/time.rs
new file mode 100644
index 0000000..1dad66a
--- /dev/null
+++ b/scan_core/src/time.rs
@@ -0,0 +1,49 @@
+use std::ops::{Bound, RangeBounds};
+
+/// The type that represents time.
+pub type Time = u32;
+
+/// A time constraint given by lower bound and upper bounds.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct TimeRange {
+    lower_bound: Bound<Time>,
+    upper_bound: Bound<Time>,
+}
+
+impl RangeBounds<Time> for TimeRange {
+    fn start_bound(&self) -> Bound<&Time> {
+        self.lower_bound.as_ref()
+    }
+
+    fn end_bound(&self) -> Bound<&Time> {
+        self.upper_bound.as_ref()
+    }
+}
+
+impl TimeRange {
+    /// Creates new [`TimeRange`] from any range.
+    pub fn new<R: RangeBounds<Time>>(range: R) -> Self {
+        TimeRange {
+            lower_bound: range.start_bound().cloned(),
+            upper_bound: range.end_bound().cloned(),
+        }
+    }
+
+    /// Shift time range in the future for the given delta.
+    pub fn shift(&self, delta: Time) -> Self {
+        let lower_bound = match self.lower_bound {
+            Bound::Included(l) => Bound::Included(l.saturating_add(delta)),
+            Bound::Excluded(l) => Bound::Excluded(l.saturating_add(delta)),
+            Bound::Unbounded => Bound::Unbounded,
+        };
+        let upper_bound = match self.upper_bound {
+            Bound::Included(r) => Bound::Included(r.saturating_add(delta)),
+            Bound::Excluded(r) => Bound::Excluded(r.saturating_add(delta)),
+            Bound::Unbounded => Bound::Unbounded,
+        };
+        TimeRange {
+            lower_bound,
+            upper_bound,
+        }
+    }
+}
diff --git a/scan_core/src/transition_system.rs b/scan_core/src/transition_system.rs
index 5545b05..9b591ee 100644
--- a/scan_core/src/transition_system.rs
+++ b/scan_core/src/transition_system.rs
@@ -1,14 +1,37 @@
 use std::sync::Arc;
 use std::sync::atomic::{AtomicBool, Ordering};
 
+use bumpalo::Bump;
+use bumpalo::collections::CollectIn;
 use log::trace;
 use rand::rngs::SmallRng;
+use rand::seq::IteratorRandom;
+use rand::{RngExt, SeedableRng, make_rng};
+use thiserror::Error;
 
 use crate::channel_system::{
-    Action, Channel, ChannelSystem, ChannelSystemBuilder, ChannelSystemRun, Event, EventType,
+    Action, Channel, ChannelSystem, ChannelSystemRun, CsError, Event, EventType, Location, PgId,
 };
 use crate::{BooleanExpr, Oracle, RunOutcome, Time, Tracer, Val};
 
+/// Errors produced by a [`TransitionSystem`].
+#[derive(Debug, Clone, Copy, Error)]
+pub enum TsError {
+    /// The CS returned an error of its own.
+    #[error("error from channel system {0:?}")]
+    ChannelSystem(CsError),
+    /// The default value set for the port is not the right type,
+    /// i.e., the type of messages of the channel.
+    #[error("default port value is not the type of the channel {0:?}")]
+    WrongPortType(Channel),
+}
+
+impl From<CsError> for TsError {
+    fn from(value: CsError) -> Self {
+        Self::ChannelSystem(value)
+    }
+}
+
 /// An atomic variable exposed by the [`ChannelSystem to the TransitionSystem`].
 #[derive(Debug, Clone, Copy)]
 pub enum Atom {
@@ -30,8 +53,7 @@ pub struct TransitionSystem {
 
 impl TransitionSystem {
     /// Creates a new [`CsModel`] from a [`ChannelSystemBuilder`].
-    pub fn new(cs: ChannelSystemBuilder) -> Self {
-        let cs = cs.build();
+    pub fn new(cs: ChannelSystem) -> Self {
         Self {
             ports: Vec::new(),
             vals: Vec::new(),
@@ -42,10 +64,12 @@ impl TransitionSystem {
 
     /// Adds a new port to the [`CsModel`],
     /// which is given by an [`Channel`] and a default [`Val`] value.
-    pub fn add_port(&mut self, channel: Channel, mut value: Vec<Val>) {
-        let len = self.cs.channels()[u16::from(channel) as usize].0.len();
-        assert_eq!(len, value.len());
-        // TODO FIXME: error handling and type checking.
+    pub fn add_port(&mut self, channel: Channel, mut value: Vec<Val>) -> Result<(), TsError> {
+        let types = self.cs.channel(channel)?.0;
+        if types.len() != value.len() || types.iter().zip(&value).any(|(t, val)| val.r#type() != *t)
+        {
+            return Err(TsError::WrongPortType(channel));
+        }
         // Keep ports list ordered
         // Don't insert duplicated ports
         if let Err(index) = self.ports.binary_search(&channel) {
@@ -55,11 +79,12 @@ impl TransitionSystem {
         }
         assert!(self.ports.is_sorted());
         assert_eq!(self.ports.len(), self.vals.len());
+        Ok(())
     }
 
     /// Adds a new predicate to the [`CsModel`],
     /// which is an expression over the CS's channels.
-    pub fn add_predicate(&mut self, predicate: BooleanExpr<Atom>) {
+    pub fn add_predicate(&mut self, predicate: BooleanExpr<Atom>) -> Result<(), TsError> {
         // Make sure predicate type-checks
         let _ = predicate.eval::<SmallRng>(
             &|port| match port {
@@ -72,9 +97,10 @@ impl TransitionSystem {
                 }
                 Atom::Event(..) => Val::Boolean(false),
             },
-            &mut None,
+            None,
         );
         self.predicates.push(predicate);
+        Ok(())
     }
 
     /// Shrink ports storage to optimize space use.
@@ -88,12 +114,17 @@ impl TransitionSystem {
     pub fn new_run(&self) -> TransitionSystemRun<'_> {
         let mut vals = self.vals.clone();
         vals.shrink_to_fit();
+        let mut pg_list = Vec::from_iter(self.cs.program_graph_ids());
+        pg_list.shrink_to_fit();
         TransitionSystemRun {
             cs: self.cs.new_instance(),
             ports: &self.ports,
             vals,
             predicates: &self.predicates,
             last_event: None,
+            pg_list,
+            rng: make_rng(),
+            bump: Bump::new(),
         }
     }
 }
@@ -102,13 +133,31 @@ impl TransitionSystem {
 ///
 /// It is essentially a CS which keeps track of the [`Event`]s produced by the execution
 /// and determining a set of predicates.
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 pub struct TransitionSystemRun<'def> {
     cs: ChannelSystemRun<'def>,
     ports: &'def [Channel],
     vals: Vec<Vec<Val>>,
     predicates: &'def [BooleanExpr<Atom>],
     last_event: Option<(Action, Event)>,
+    pg_list: Vec<PgId>,
+    rng: SmallRng,
+    bump: Bump,
+}
+
+impl<'def> Clone for TransitionSystemRun<'def> {
+    fn clone(&self) -> Self {
+        Self {
+            cs: self.cs.clone(),
+            ports: self.ports,
+            vals: self.vals.clone(),
+            predicates: self.predicates,
+            last_event: self.last_event.clone(),
+            pg_list: self.pg_list.clone(),
+            rng: self.rng.clone(),
+            bump: Bump::new(),
+        }
+    }
 }
 
 impl<'def> TransitionSystemRun<'def> {
@@ -116,7 +165,7 @@ impl<'def> TransitionSystemRun<'def> {
     ///
     /// Used to generate Montecarlo-like executions
     pub fn transition(&mut self) {
-        self.last_event = self.cs.montecarlo_execution();
+        self.last_event = self.montecarlo_transition();
         if let Some((_, ref event)) = self.last_event
             && let EventType::Send(ref vals) = event.event_type
             && let Ok(index) = self.ports.binary_search(&event.channel)
@@ -161,7 +210,7 @@ impl<'def> TransitionSystemRun<'def> {
                         }))
                     }
                 },
-                &mut None,
+                None,
             )
         })
     }
@@ -174,44 +223,38 @@ impl<'def> TransitionSystemRun<'def> {
     /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] and returns a [`RunOutcome`].
     pub(crate) fn experiment<O: Oracle>(
         &mut self,
-        duration: Time,
         mut oracle: O,
         running: Arc<AtomicBool>,
     ) -> RunOutcome {
-        trace!("new run starting");
         // reuse vector to avoid allocations
         let mut labels = Vec::from_iter(self.labels());
         // Initialize oracle with TS initial state
         oracle.update_state(&labels);
-        while self.time() <= duration {
+        while oracle.output_guarantees().any(|b| b.is_none()) {
             self.transition();
-            if self.last_event().is_some() {
+            if !running.load(Ordering::Relaxed) {
+                trace!("run stopped");
+                return None;
+            } else if self.last_event().is_some() {
                 labels.clear();
                 labels.extend(self.labels());
                 oracle.update_state(&labels);
-            } else {
+            } else if self.cs.is_waiting() {
                 self.time_tick();
                 oracle.update_time(self.time());
-            }
-            if !running.load(Ordering::Relaxed) {
-                trace!("run stopped");
-                return RunOutcome::Incomplete;
-            } else if oracle.output_guarantees().all(|b| b.is_some()) {
-                trace!("run complete early");
-                let verified = Vec::from_iter(oracle.output_guarantees().map(Option::unwrap));
-                return RunOutcome::Verified(verified);
+            } else {
+                break;
             }
         }
         trace!("run complete");
         let verified = Vec::from_iter(oracle.final_output_guarantees());
-        RunOutcome::Verified(verified)
+        Some(verified)
     }
 
     /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`]
     /// and process the execution trace via the given [`Tracer`].
     pub(crate) fn trace<T, O: Oracle>(
         &mut self,
-        duration: Time,
         mut oracle: O,
         mut tracer: T,
         model_data: &T::ModelData,
@@ -226,20 +269,93 @@ impl<'def> TransitionSystemRun<'def> {
         oracle.update_state(&labels);
         // WARN FIXME TODO: Initial state is not written as there is no corresponding action/event
         // Same issue for time-tick events
-        while self.time() <= duration {
+        while oracle.output_guarantees().any(|b| b.is_none()) {
             self.transition();
             if let Some((action, event)) = self.last_event() {
                 tracer.trace(model_data, *action, event, self.time(), self.state());
                 labels.clear();
                 labels.extend(self.labels());
                 oracle.update_state(&labels);
-            } else {
+            } else if self.cs.is_waiting() {
                 self.time_tick();
                 oracle.update_time(self.time());
+            } else {
+                break;
             }
         }
         trace!("run complete");
         let verified = Vec::from_iter(oracle.final_output_guarantees());
-        RunOutcome::Verified(verified)
+        Some(verified)
+    }
+
+    fn montecarlo_transition(&mut self) -> Option<(Action, Event)> {
+        let mut rand1 = SmallRng::from_rng(&mut self.rng);
+        // Setting pgs_left as length resets the queue
+        let mut pgs_left = self.pg_list.len();
+        while pgs_left > 0 {
+            // Select random pg within 0..pgs_left
+            let pg_select = self.rng.random_range(0..pgs_left);
+            let pg_id = self.pg_list[pg_select];
+            // Swap selected pg with last element of the queue (possibly itself, probably not worth checking)
+            // Decrease the length of the queue (so that selected element is removed)
+            pgs_left -= 1;
+            self.pg_list.swap(pg_select, pgs_left);
+            // Execute randomly chosen transitions on the picked PG until an event is generated,
+            // or no more transition is possible
+            // NOTE: Special treatment for PGs with single-location state for optimization of this common case.
+            // Hopefully it will be possible to treat all cases in a general way eventually.
+            if self
+                .cs
+                .program_graph(pg_id)
+                .expect("pg exists")
+                .current_states()
+                .len()
+                == 1
+            {
+                while let Some((action, post_state)) = self
+                    .cs
+                    .nosync_possible_transitions_pg(pg_id)
+                    .expect("pg exists")
+                    .filter_map(|(action, post_states)| {
+                        post_states.choose(&mut rand1).map(|loc| (action, loc))
+                    })
+                    .choose(&mut self.rng)
+                {
+                    let event = self
+                        .cs
+                        .transition(pg_id, action, &[post_state])
+                        .expect("successful transition");
+                    if event.is_some() {
+                        return event.map(|ev| (action, ev));
+                    }
+                }
+            } else {
+                use bumpalo::collections::Vec as BumpVec;
+
+                self.bump.reset();
+                while let Some((action, post_states)) = self
+                    .cs
+                    .possible_transitions_pg(pg_id)
+                    .expect("pg exists")
+                    .filter_map(|(action, post_states)| {
+                        post_states
+                            .map(|locs| locs.choose(&mut rand1))
+                            .collect_in::<Option<BumpVec<Location>>>(&self.bump)
+                            // .collect::<Option<Vec<Location>>>()
+                            .map(|locs| (action, locs))
+                    })
+                    .choose(&mut self.rng)
+                {
+                    let event = self
+                        .cs
+                        .transition(pg_id, action, post_states.as_slice())
+                        .expect("successful transition");
+                    if event.is_some() {
+                        return event.map(|ev| (action, ev));
+                    }
+                }
+            }
+        }
+        None
     }
 }
diff --git a/scan_core/tests/counter.rs b/scan_core/tests/counter.rs
index ed2b80e..02184c0 100644
--- a/scan_core/tests/counter.rs
+++ b/scan_core/tests/counter.rs
@@ -23,10 +23,11 @@ fn counter_pg() {
         cs.add_transition(pg, initial, action, initial, Some(guard))
             .unwrap();
     }
-    let cs = TransitionSystem::new(cs);
-    let mut pg: TransitionSystemRun = cs.new_run();
-    pg.transition();
-    while pg.last_event().is_some() {
-        pg.transition();
+    let cs = cs.build();
+    let ts = TransitionSystem::new(cs);
+    let mut run: TransitionSystemRun = ts.new_run();
+    run.transition();
+    while run.last_event().is_some() {
+        run.transition();
     }
 }
diff --git a/scan_jani/Cargo.toml b/scan_jani/Cargo.toml
index 20f0665..ea3f162 100644
--- a/scan_jani/Cargo.toml
+++ b/scan_jani/Cargo.toml
@@ -29,5 +29,5 @@ smc_scan_mtl = { version = "0.1.0", path = "../scan_mtl" }
 thiserror = { workspace = true }
 serde = { workspace = true }
 serde_json = { workspace = true }
-either = "1.15.0"
+either = "1.16.0"
 csv = { workspace = true }
diff --git a/scan_jani/src/builder.rs b/scan_jani/src/builder.rs
index 8b1dc57..332e83d 100644
--- a/scan_jani/src/builder.rs
+++ b/scan_jani/src/builder.rs
@@ -639,9 +639,10 @@ impl JaniBuilder {
             }
         }
 
+        let cs = cs.build();
         let mut cs_model = TransitionSystem::new(cs);
         // global state port, only one we need
-        cs_model.add_port(global_state_channel, global_state_init);
+        cs_model.add_port(global_state_channel, global_state_init)?;
 
         // Add properties
         let properties = if properties.is_empty() {
@@ -709,9 +710,7 @@ impl JaniBuilder {
         property_exprs
             .iter()
             .flat_map(|prop| extract_predicates(prop).into_iter())
-            .for_each(|predicate| {
-                cs_model.add_predicate(predicate);
-            });
+            .try_for_each(|predicate| cs_model.add_predicate(predicate))?;
         property_exprs
             .into_iter()
             .map(|p| extract_mtl(&p, &mut idx))
diff --git a/scan_jani/src/lib.rs b/scan_jani/src/lib.rs
index f31d5af..fc7a805 100644
--- a/scan_jani/src/lib.rs
+++ b/scan_jani/src/lib.rs
@@ -1,4 +1,8 @@
 //! Parser and model builder for SCAN's JANI specification format.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![forbid(unsafe_code)]
 
 mod builder;
 mod parser;
@@ -14,12 +18,10 @@ use scan_mtl::MtlOracle;
 use std::{fs::File, io::Read, path::Path};
 pub use tracer::TracePrinter;
 
-pub type JaniScan = Scan<MtlOracle>;
-
 pub fn load<'def>(
     path: &'def Path,
     properties: &'def [String],
-) -> anyhow::Result<(JaniScan, JaniModelData)> {
+) -> anyhow::Result<(Scan<MtlOracle>, JaniModelData)> {
     let time = std::time::Instant::now();
     info!(target: "parser", "parsing JANI model file '{}'", path.display());
     // NOTE: See <https://github.com/serde-rs/json/issues/160>
diff --git a/scan_jani/tests/tests.rs b/scan_jani/tests/tests.rs
index 0ed4ebf..a6dd2c3 100644
--- a/scan_jani/tests/tests.rs
+++ b/scan_jani/tests/tests.rs
@@ -32,5 +32,5 @@ fn leader_sync_5_4() {
 
 fn test(path: &Path) {
     let (scan, ..) = scan_jani::load(path, &[]).expect("load");
-    scan.adaptive(0.95, 0.01, 0).expect("run verification");
+    scan.adaptive(0.95, 0.01).expect("run verification");
 }
diff --git a/scan_mtl/src/lib.rs b/scan_mtl/src/lib.rs
index 270e7d3..c035815 100644
--- a/scan_mtl/src/lib.rs
+++ b/scan_mtl/src/lib.rs
@@ -1,3 +1,10 @@
+//! Metric Temporal Logic (MTL) oracle.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![warn(missing_docs)]
+#![forbid(unsafe_code)]
+
 mod oracle;
 
 pub use oracle::{Mtl, MtlOracle};
diff --git a/scan_pmtl/src/lib.rs b/scan_pmtl/src/lib.rs
index 3ab2ca3..d335ff7 100644
--- a/scan_pmtl/src/lib.rs
+++ b/scan_pmtl/src/lib.rs
@@ -1,3 +1,10 @@
+//! Past-Metric Temporal Logic (pMTL) oracle.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![warn(missing_docs)]
+#![forbid(unsafe_code)]
+
 mod oracle;
 
 pub use oracle::{Pmtl, PmtlOracle};
diff --git a/scan_pmtl/src/oracle.rs b/scan_pmtl/src/oracle.rs
index c32905e..9311e71 100644
--- a/scan_pmtl/src/oracle.rs
+++ b/scan_pmtl/src/oracle.rs
@@ -1,8 +1,8 @@
 mod numset;
 
 use numset::NumSet;
-use scan_core::{Oracle, Time};
-use std::hash::Hash;
+use scan_core::{Oracle, Time, TimeRange};
+use std::{hash::Hash, ops::RangeBounds};
 
 /// A Past-time Metric Temporal Logic (PMTL) formula.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -25,11 +25,11 @@ where
     /// Logical implication of a antecedent formula and a consequent formula.
     Implies(Box<(Pmtl<V>, Pmtl<V>)>),
     /// Temporal historical predicate over a formula (with bounds).
-    Historically(Box<Pmtl<V>>, Time, Time),
+    Historically(Box<Pmtl<V>>, TimeRange),
     /// Temporal previously predicate over a formula (with bounds).
-    Once(Box<Pmtl<V>>, Time, Time),
+    Once(Box<Pmtl<V>>, TimeRange),
     /// Temporal since predicate over a formula (with bounds).
-    Since(Box<(Pmtl<V>, Pmtl<V>)>, Time, Time),
+    Since(Box<(Pmtl<V>, Pmtl<V>)>, TimeRange),
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -41,9 +41,9 @@ enum ValPmtl {
     Or(Vec<ValPmtl>),
     Not(Box<ValPmtl>),
     Implies(Box<(ValPmtl, ValPmtl)>),
-    Historically(Box<ValPmtl>, Time, Time, NumSet),
-    Once(Box<ValPmtl>, Time, Time, NumSet),
-    Since(Box<(ValPmtl, ValPmtl)>, Time, Time, NumSet),
+    Historically(Box<ValPmtl>, TimeRange, NumSet),
+    Once(Box<ValPmtl>, TimeRange, NumSet),
+    Since(Box<(ValPmtl, ValPmtl)>, TimeRange, NumSet),
 }
 
 impl From<&Pmtl<usize>> for ValPmtl {
@@ -58,16 +58,15 @@ impl From<&Pmtl<usize>> for ValPmtl {
             Pmtl::Implies(pmtls) => {
                 ValPmtl::Implies(Box::new(((&pmtls.0).into(), (&pmtls.1).into())))
             }
-            Pmtl::Historically(pmtl, lb, ub) => {
-                ValPmtl::Historically(Box::new(pmtl.as_ref().into()), *lb, *ub, NumSet::empty())
+            Pmtl::Historically(pmtl, range) => {
+                ValPmtl::Historically(Box::new(pmtl.as_ref().into()), *range, NumSet::empty())
             }
-            Pmtl::Once(pmtl, lb, ub) => {
-                ValPmtl::Once(Box::new(pmtl.as_ref().into()), *lb, *ub, NumSet::empty())
+            Pmtl::Once(pmtl, range) => {
+                ValPmtl::Once(Box::new(pmtl.as_ref().into()), *range, NumSet::empty())
             }
-            Pmtl::Since(pmtls, lb, ub) => ValPmtl::Since(
+            Pmtl::Since(pmtls, range) => ValPmtl::Since(
                 Box::new(((&pmtls.0).into(), (&pmtls.1).into())),
-                *lb,
-                *ub,
+                *range,
                 NumSet::empty(),
             ),
         }
@@ -88,13 +87,9 @@ impl ValPmtl {
                 let (lhs, rhs) = subformulae.as_ref();
                 rhs.output(time) || !lhs.output(time)
             }
-            ValPmtl::Historically(_sub, _lower_bound, _upper_bound, valuation) => {
-                !valuation.contains(time)
-            }
-            ValPmtl::Once(_sub, _lower_bound, _upper_bound, valuation) => valuation.contains(time),
-            ValPmtl::Since(_subformulae, _lower_bound, _upper_bound, valuation) => {
-                valuation.contains(time)
-            }
+            ValPmtl::Historically(_sub, _range, valuation) => !valuation.contains(time),
+            ValPmtl::Once(_sub, _range, valuation) => valuation.contains(time),
+            ValPmtl::Since(_subformulae, _range, valuation) => valuation.contains(time),
         }
     }
 
@@ -116,25 +111,19 @@ impl ValPmtl {
                 lhs.update_state(state, time);
                 rhs.update_state(state, time);
             }
-            ValPmtl::Historically(sub, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Historically(sub, range, valuation) => {
                 sub.update_state(state, time);
                 if !sub.output(time) {
-                    valuation.add_interval(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation += range.shift(time);
                 }
             }
-            ValPmtl::Once(sub, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Once(sub, range, valuation) => {
                 sub.update_state(state, time);
                 if sub.output(time) {
-                    valuation.add_interval(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation += range.shift(time);
                 }
             }
-            ValPmtl::Since(subformulae, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Since(subformulae, range, valuation) => {
                 let (lhs, rhs) = subformulae.as_mut();
                 // Make sure all subformulae are updated
                 lhs.update_state(state, time);
@@ -143,16 +132,10 @@ impl ValPmtl {
                 let out_rhs = rhs.output(time);
                 if out_lhs {
                     if out_rhs {
-                        valuation.add_interval(
-                            lower_bound.saturating_add(time),
-                            upper_bound.saturating_add(time),
-                        );
+                        *valuation += range.shift(time);
                     }
                 } else if out_rhs {
-                    *valuation = NumSet::from_range(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation = NumSet::from(range.shift(time));
                 } else {
                     *valuation = NumSet::empty();
                 }
@@ -178,25 +161,19 @@ impl ValPmtl {
                 lhs.update_time(time);
                 rhs.update_time(time);
             }
-            ValPmtl::Historically(sub, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Historically(sub, range, valuation) => {
                 sub.update_time(time);
                 if !sub.output(time) {
-                    valuation.add_interval(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation += range.shift(time);
                 }
             }
-            ValPmtl::Once(sub, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Once(sub, range, valuation) => {
                 sub.update_time(time);
                 if sub.output(time) {
-                    valuation.add_interval(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation += range.shift(time);
                 }
             }
-            ValPmtl::Since(subformulae, lower_bound, upper_bound, valuation) => {
+            ValPmtl::Since(subformulae, range, valuation) => {
                 let (lhs, rhs) = subformulae.as_mut();
                 // Make sure all subformulae are updated
                 lhs.update_time(time);
@@ -205,16 +182,10 @@ impl ValPmtl {
                 let out_rhs = rhs.output(time);
                 if out_lhs {
                     if out_rhs {
-                        valuation.add_interval(
-                            lower_bound.saturating_add(time),
-                            upper_bound.saturating_add(time),
-                        );
+                        *valuation += range.shift(time);
                     }
                 } else if out_rhs {
-                    *valuation = NumSet::from_range(
-                        lower_bound.saturating_add(time),
-                        upper_bound.saturating_add(time),
-                    );
+                    *valuation = NumSet::from(range.shift(time));
                 } else {
                     *valuation = NumSet::empty();
                 }
@@ -252,29 +223,29 @@ impl ValPmtl {
             // Valuation of Historically represents the set of time moments in which we know the formula to be false.
             // If the argument of the operator is know to be always true, then Historically is always true.
             // If the argument of the operator is know to be always false, then Historically is always false provided that the lower time bound is 0.
-            ValPmtl::Historically(subformula, lb, _, valuation) => subformula
+            ValPmtl::Historically(subformula, range, valuation) => subformula
                 .valuation(time)
-                .and_then(|v| (*lb == 0 || v).then_some(v))
+                .and_then(|v| (range.contains(&0) || v).then_some(v))
                 .or_else(|| valuation.contains_unbounded_interval(time).then_some(false)),
             // Valuation of Previously represents the set of time moments in which we know the formula to be false.
             // If the argument of the operator is know to be always true, then Previously is always true provided that the lower time bound is 0.
             // If the argument of the operator is know to be always false, then Previously is always false.
-            ValPmtl::Once(subformula, lb, _, valuation) => subformula
+            ValPmtl::Once(subformula, range, valuation) => subformula
                 .valuation(time)
-                .and_then(|v| (*lb == 0 || !v).then_some(v))
+                .and_then(|v| (range.contains(&0) || !v).then_some(v))
                 .or_else(|| valuation.contains_unbounded_interval(time).then_some(true)),
             // Valuation of Since represents the set of time moments in which we know the formula to be true if its lhs argument is true from then on.
             // If the rhs argument of the operator is know to be always false, then Since is always false.
             // If the Since valuation is always true and the lhs argument of the operator is know to be always true, then Since is always true.
             // If the Since valuation is always true and the lhs argument of the operator is know to be always false, then Since is always false provided that the lower time bound is 0.
-            ValPmtl::Since(subformulae, lb, _, valuation) => {
+            ValPmtl::Since(subformulae, range, valuation) => {
                 if let Some(false) = subformulae.1.valuation(time) {
                     Some(false)
                 } else if valuation.contains_unbounded_interval(time) {
                     subformulae
                         .0
                         .valuation(time)
-                        .and_then(|v| (*lb == 0 || v).then_some(v))
+                        .and_then(|v| (range.contains(&0) || v).then_some(v))
                 } else {
                     None
                 }
@@ -348,7 +319,7 @@ mod tests {
 
     #[test]
     fn since_1() {
-        let formula = Pmtl::Since(Box::new((Pmtl::Atom(0), Pmtl::Atom(1))), 0, Time::MAX);
+        let formula = Pmtl::Since(Box::new((Pmtl::Atom(0), Pmtl::Atom(1))), TimeRange::new(..));
         let mut oracle = PmtlOracle::new(&[], &[formula]);
         oracle.update_state(&[false, true]);
         assert!(oracle.final_output_guarantees().any(|b| b));
@@ -374,7 +345,10 @@ mod tests {
 
     #[test]
     fn since_2() {
-        let formula = Pmtl::Since(Box::new((Pmtl::Atom(0), Pmtl::Atom(1))), 0, 2);
+        let formula = Pmtl::Since(
+            Box::new((Pmtl::Atom(0), Pmtl::Atom(1))),
+            TimeRange::new(0..=2),
+        );
         let mut oracle = PmtlOracle::new(&[], &[formula]);
         oracle.update_state(&[false, true]);
         assert!(oracle.final_output_guarantees().any(|b| b));
@@ -402,7 +376,10 @@ mod tests {
 
     #[test]
     fn since_3() {
-        let formula = Pmtl::Since(Box::new((Pmtl::Atom(0), Pmtl::Atom(1))), 1, 2);
+        let formula = Pmtl::Since(
+            Box::new((Pmtl::Atom(0), Pmtl::Atom(1))),
+            TimeRange::new(1..=2),
+        );
         let mut oracle = PmtlOracle::new(&[], &[formula]);
         oracle.update_state(&[false, true]);
         assert!(oracle.final_output_guarantees().any(|b| !b));
diff --git a/scan_pmtl/src/oracle/numset.rs b/scan_pmtl/src/oracle/numset.rs
index 866c226..4444c0c 100644
--- a/scan_pmtl/src/oracle/numset.rs
+++ b/scan_pmtl/src/oracle/numset.rs
@@ -1,5 +1,25 @@
+use std::ops::{AddAssign, Bound, RangeBounds};
+
 use scan_core::Time;
 
+#[inline]
+fn lower_bound<R: RangeBounds<Time>>(range: &R) -> Time {
+    match range.start_bound() {
+        Bound::Included(b) => *b,
+        Bound::Excluded(b) => *b + 1,
+        Bound::Unbounded => Time::MIN,
+    }
+}
+
+#[inline]
+fn upper_bound<R: RangeBounds<Time>>(range: &R) -> Time {
+    match range.end_bound() {
+        Bound::Included(b) => *b,
+        Bound::Excluded(b) => *b - 1,
+        Bound::Unbounded => Time::MAX,
+    }
+}
+
 // Represent union of closed intervals,
 // each interval being represented by lower and upper bounds.
 // So, `(lower_bound, upper_bound)` represents the closed interval `lower_bound..=upper_bound`.
@@ -7,51 +27,25 @@ use scan_core::Time;
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(super) struct NumSet(Vec<(Time, Time)>);
 
-impl NumSet {
+impl<R: RangeBounds<Time>> From<R> for NumSet {
     #[inline]
-    pub(super) fn empty() -> Self {
-        Self(Vec::new())
-    }
-
-    #[inline]
-    fn _full() -> Self {
-        Self(vec![(0, Time::MAX)])
-    }
-
-    #[inline]
-    pub(super) fn from_range(lower_bound: Time, upper_bound: Time) -> Self {
-        assert!(lower_bound <= upper_bound);
+    fn from(value: R) -> Self {
+        let lower_bound = lower_bound(&value);
+        let upper_bound = upper_bound(&value);
         Self(vec![(lower_bound, upper_bound)])
     }
+}
 
-    #[inline]
-    pub(super) fn contains(&self, t: Time) -> bool {
-        match self.0.binary_search_by_key(&t, |&(t, _)| t) {
-            Ok(_) => true,
-            Err(i) if i > 0 => self.0[i - 1].1 >= t,
-            _ => false,
-        }
-    }
+impl<R: RangeBounds<Time>> AddAssign<R> for NumSet {
+    fn add_assign(&mut self, rhs: R) {
+        let lower_bound = lower_bound(&rhs);
+        let upper_bound = upper_bound(&rhs);
 
-    #[inline]
-    fn _contains_interval(&self, lower_bound: Time, upper_bound: Time) -> bool {
-        assert!(lower_bound <= upper_bound);
-        match self.0.binary_search_by_key(&lower_bound, |&(t, _)| t) {
-            Ok(i) => self.0[i].1 >= upper_bound,
-            Err(i) if i > 0 => self.0[i - 1].1 >= upper_bound,
-            _ => false,
+        // Skip if empty range
+        if lower_bound > upper_bound {
+            return;
         }
-    }
-
-    #[inline]
-    pub(super) fn contains_unbounded_interval(&self, lower_bound: Time) -> bool {
-        self.0
-            .last()
-            .is_some_and(|&(l, u)| l <= lower_bound && u == Time::MAX)
-    }
 
-    pub(super) fn add_interval(&mut self, lower_bound: Time, upper_bound: Time) {
-        assert!(lower_bound <= upper_bound);
         let len = self.0.len();
 
         match self
@@ -111,7 +105,44 @@ impl NumSet {
                 }
             }
         }
-        // Self(new)
+    }
+}
+
+impl NumSet {
+    #[inline]
+    pub(super) fn empty() -> Self {
+        Self(Vec::new())
+    }
+
+    #[inline]
+    fn _full() -> Self {
+        Self(vec![(0, Time::MAX)])
+    }
+
+    #[inline]
+    pub(super) fn contains(&self, t: Time) -> bool {
+        match self.0.binary_search_by_key(&t, |&(t, _)| t) {
+            Ok(_) => true,
+            Err(i) if i > 0 => self.0[i - 1].1 >= t,
+            _ => false,
+        }
+    }
+
+    #[inline]
+    fn _contains_interval(&self, lower_bound: Time, upper_bound: Time) -> bool {
+        assert!(lower_bound <= upper_bound);
+        match self.0.binary_search_by_key(&lower_bound, |&(t, _)| t) {
+            Ok(i) => self.0[i].1 >= upper_bound,
+            Err(i) if i > 0 => self.0[i - 1].1 >= upper_bound,
+            _ => false,
+        }
+    }
+
+    #[inline]
+    pub(super) fn contains_unbounded_interval(&self, lower_bound: Time) -> bool {
+        self.0
+            .last()
+            .is_some_and(|&(l, u)| l <= lower_bound && u == Time::MAX)
     }
 }
 
@@ -122,66 +153,66 @@ mod tests {
     #[test]
     fn add_interval_1() {
         let mut set = NumSet::empty();
-        set.add_interval(0, 1);
+        set += 0..=1;
         assert_eq!(set, NumSet(vec![(0, 1)]));
 
         let mut set = NumSet::empty();
-        set.add_interval(1, 1);
+        set += 1..=1;
         assert_eq!(set, NumSet(vec![(1, 1)]));
 
         let mut set = NumSet::empty();
-        set.add_interval(1, Time::MAX);
+        set += 1..;
         assert_eq!(set, NumSet(vec![(1, Time::MAX)]));
     }
 
     #[test]
     fn add_interval_2() {
         let mut set = NumSet::_full();
-        set.add_interval(0, 1);
+        set += 0..=1;
         assert_eq!(set, NumSet::_full());
 
-        set.add_interval(1, 1);
+        set += 1..=1;
         assert_eq!(set, NumSet::_full());
 
-        set.add_interval(1, Time::MAX);
+        set += 1..=Time::MAX;
         assert_eq!(set, NumSet::_full());
     }
 
     #[test]
     fn add_interval_3() {
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(0, 1);
+        let mut set = NumSet::from(5..=10);
+        set += 0..=1;
         assert_eq!(set, NumSet(vec![(0, 1), (5, 10)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(12, 13);
+        let mut set = NumSet::from(5..=10);
+        set += 12..=13;
         assert_eq!(set, NumSet(vec![(5, 10), (12, 13)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(7, 8);
+        let mut set = NumSet::from(5..=10);
+        set += 7..=8;
         assert_eq!(set, NumSet(vec![(5, 10)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(3, 12);
+        let mut set = NumSet::from(5..=10);
+        set += 3..=12;
         assert_eq!(set, NumSet(vec![(3, 12)]));
     }
 
     #[test]
     fn add_interval_4() {
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(0, 5);
+        let mut set = NumSet::from(5..=10);
+        set += 0..=5;
         assert_eq!(set, NumSet(vec![(0, 10)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(0, 4);
+        let mut set = NumSet::from(5..=10);
+        set += 0..=4;
         assert_eq!(set, NumSet(vec![(0, 10)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(10, 15);
+        let mut set = NumSet::from(5..=10);
+        set += 10..=15;
         assert_eq!(set, NumSet(vec![(5, 15)]));
 
-        let mut set = NumSet::from_range(5, 10);
-        set.add_interval(11, 15);
+        let mut set = NumSet::from(5..=10);
+        set += 11..=15;
         assert_eq!(set, NumSet(vec![(5, 15)]));
     }
 }
diff --git a/scan_promela/Cargo.toml b/scan_promela/Cargo.toml
index ff3d652..8842d1c 100644
--- a/scan_promela/Cargo.toml
+++ b/scan_promela/Cargo.toml
@@ -23,13 +23,13 @@ crate-type = ["lib"]  # The crate types to generate.
 
 [build-dependencies]
 cfgrammar = "0.14"
-lrlex = "0.14.1"
-lrpar = "0.14.1"
+lrlex = "0.14.2"
+lrpar = "0.14.2"
 
 [dependencies]
 cfgrammar = "0.14"
-lrlex = "0.14.1"
-lrpar = "0.14.1"
+lrlex = "0.14.2"
+lrpar = "0.14.2"
 regex = "1"
 smc_scan_core = { version = "0.2.0", path = "../scan_core" }
 smc_scan_pmtl = { version = "0.1.0", path = "../scan_pmtl" }
diff --git a/scan_promela/src/lib.rs b/scan_promela/src/lib.rs
index c2afa66..1bb1b22 100644
--- a/scan_promela/src/lib.rs
+++ b/scan_promela/src/lib.rs
@@ -1,3 +1,9 @@
+//! Parser and model builder for SCAN's Promela specification format.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![forbid(unsafe_code)]
+
 use std::{fs::File, io::Read, path::Path};
 
 pub use crate::spinv4_y::*;
@@ -16,15 +22,13 @@ use regex::Regex;
 use scan_core::{Scan, TransitionSystem};
 use scan_pmtl::PmtlOracle;
 
-pub type PromelaScan = Scan<PmtlOracle>;
-
 pub type PromelaModel = ();
 
 pub fn load(
     path: &Path,
     _properties: &[String],
     _all_properties: bool,
-) -> anyhow::Result<(PromelaScan, PromelaModel)> {
+) -> anyhow::Result<(Scan<PmtlOracle>, PromelaModel)> {
     // let time = std::time::Instant::now();
     // info!(target: "parser", "parse SCXML model");
 
@@ -46,7 +50,7 @@ pub fn load(
     // Ok((scan, model))
 }
 
-fn process_file(path: &Path, debug_mode: bool) -> anyhow::Result<(PromelaScan, PromelaModel)> {
+fn process_file(path: &Path, debug_mode: bool) -> anyhow::Result<(Scan<PmtlOracle>, PromelaModel)> {
     /* ---------- 1. extension check ----------------------------------------- */
     match path.extension().and_then(|e| e.to_str()) {
         Some("pml" | "prm") => {}
@@ -88,7 +92,8 @@ fn process_file(path: &Path, debug_mode: bool) -> anyhow::Result<(PromelaScan, P
 
     /* ---------- 5. build: AST → Channel System ------------------------------ */
     let cs = Builder::create_channel_system(ast)
-        .context("failed to create channel system from AST".to_string())?;
+        .context("failed to create channel system from AST".to_string())?
+        .build();
     info!("Channel system built successfully.");
     let tsd = TransitionSystem::new(cs);
     let oracle = PmtlOracle::new(&[], &[]);
diff --git a/scan_scxml/Cargo.toml b/scan_scxml/Cargo.toml
index 66560d4..0932bf7 100644
--- a/scan_scxml/Cargo.toml
+++ b/scan_scxml/Cargo.toml
@@ -29,7 +29,7 @@ boa_ast = "0.21.1"
 boa_interner = "0.21.1"
 boa_parser = "0.21.1"
 log = { workspace = true }
-quick-xml = "0.40.0"
+quick-xml = "0.40.1"
 thiserror = { workspace = true }
 logos = "0.16.1"
 chumsky = "0.13.0"
diff --git a/scan_scxml/src/builder.rs b/scan_scxml/src/builder.rs
index 0997888..cfdc192 100644
--- a/scan_scxml/src/builder.rs
+++ b/scan_scxml/src/builder.rs
@@ -942,7 +942,7 @@ impl ModelBuilder {
                     self.cs.add_reset(pg_id, reset, clock).expect("add reset");
                     let next_loc = self
                         .cs
-                        .new_timed_location(pg_id, &[(clock, None, Some(*delay + 1))])
+                        .new_timed_location(pg_id, &[(clock, TimeRange::new(0..*delay + 1))])
                         .expect("PG exists");
                     self.cs
                         .add_transition(pg_id, loc, reset, next_loc, None)
@@ -955,7 +955,7 @@ impl ModelBuilder {
                             loc,
                             next_loc,
                             None,
-                            &[(clock, Some(*delay), None)],
+                            &[(clock, TimeRange::new(*delay..))],
                         )
                         .expect("autonomous timed transition");
                     loc = next_loc;
@@ -1420,7 +1420,8 @@ impl ModelBuilder {
     }
 
     fn build_model(mut self, parser: Parser) -> (TransitionSystem, PmtlOracle, ScxmlModel) {
-        let mut model = TransitionSystem::new(self.cs);
+        let cs = self.cs.build();
+        let mut model = TransitionSystem::new(cs);
         let port_vars = self
             .port_vars
             .into_iter()
@@ -1428,10 +1429,10 @@ impl ModelBuilder {
             .collect::<Vec<_>>();
         self.ports.sort_unstable_by_key(|(c, _)| *c);
         for (channel, init) in &self.ports {
-            model.add_port(*channel, init.clone());
+            model.add_port(*channel, init.clone()).expect("add port");
         }
         for pred_expr in self.predicates {
-            model.add_predicate(pred_expr);
+            model.add_predicate(pred_expr).expect("add predicate");
         }
         // Shrink model storage (just an optimization);
         model.shrink();
diff --git a/scan_scxml/src/lib.rs b/scan_scxml/src/lib.rs
index 8d674a6..a826b9a 100644
--- a/scan_scxml/src/lib.rs
+++ b/scan_scxml/src/lib.rs
@@ -1,4 +1,8 @@
-//! Parser and model builder for SCAN's CONVINCE-XML specification format.
+//! Parser and model builder for SCAN's SCXML specification format.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![forbid(unsafe_code)]
 
 mod builder;
 mod parser;
@@ -13,13 +17,11 @@ use scan_core::Scan;
 use scan_pmtl::PmtlOracle;
 pub use tracer::TracePrinter;
 
-pub type ScxmlScan = Scan<PmtlOracle>;
-
 pub fn load(
     path: &Path,
     properties: &[String],
     all_properties: bool,
-) -> anyhow::Result<(ScxmlScan, ScxmlModel)> {
+) -> anyhow::Result<(Scan<PmtlOracle>, ScxmlModel)> {
     let time = std::time::Instant::now();
     info!(target: "parser", "parse SCXML model");
     let parser = parser::Parser::parse(path)?;
diff --git a/scan_scxml/src/parser/property.rs b/scan_scxml/src/parser/property.rs
index 412391f..c79c794 100644
--- a/scan_scxml/src/parser/property.rs
+++ b/scan_scxml/src/parser/property.rs
@@ -334,20 +334,19 @@ fn parse_predicates(
                 parse_predicates(rhs, predicates, interner)?,
             ))))
         }
-        Pmtl::Historically(pmtl, l, u) => parse_predicates(*pmtl, predicates, interner)
-            .map(|f| Pmtl::Historically(Box::new(f), l, u)),
-        Pmtl::Once(pmtl, l, u) => {
-            parse_predicates(*pmtl, predicates, interner).map(|f| Pmtl::Once(Box::new(f), l, u))
+        Pmtl::Historically(pmtl, range) => parse_predicates(*pmtl, predicates, interner)
+            .map(|f| Pmtl::Historically(Box::new(f), range)),
+        Pmtl::Once(pmtl, range) => {
+            parse_predicates(*pmtl, predicates, interner).map(|f| Pmtl::Once(Box::new(f), range))
         }
-        Pmtl::Since(args, l, u) => {
+        Pmtl::Since(args, range) => {
             let (lhs, rhs) = *args;
             Ok(Pmtl::Since(
                 Box::new((
                     parse_predicates(lhs, predicates, interner)?,
                     parse_predicates(rhs, predicates, interner)?,
                 )),
-                l,
-                u,
+                range,
             ))
         }
     }
diff --git a/scan_scxml/src/parser/rye.rs b/scan_scxml/src/parser/rye.rs
index ba67915..ea9c00e 100644
--- a/scan_scxml/src/parser/rye.rs
+++ b/scan_scxml/src/parser/rye.rs
@@ -1,7 +1,9 @@
+use std::ops::Bound;
+
 use anyhow::{anyhow, bail};
 use chumsky::{IterParser, Parser, prelude::*, select};
 use logos::Logos;
-use scan_core::Time;
+use scan_core::TimeRange;
 use scan_pmtl::Pmtl;
 
 #[derive(Logos, Debug, PartialEq, Eq, Hash, Clone)]
@@ -75,9 +77,17 @@ fn parser<'src>() -> impl Parser<'src, &'src [Token], Pmtl<String>, extra::Err<S
     };
 
     let bounds = just(Token::BracketOpen)
-        .ignore_then(integer.or_not().map(|p| p.unwrap_or(Time::MIN)))
+        .ignore_then(
+            integer
+                .or_not()
+                .map(|p| p.map(Bound::Included).unwrap_or(Bound::Unbounded)),
+        )
         .then_ignore(just(Token::Colon))
-        .then(integer.or_not().map(|p| p.unwrap_or(Time::MAX)))
+        .then(
+            integer
+                .or_not()
+                .map(|p| p.map(Bound::Included).unwrap_or(Bound::Unbounded)),
+        )
         .then_ignore(just(Token::BracketClose));
 
     recursive(|p| {
@@ -101,8 +111,8 @@ fn parser<'src>() -> impl Parser<'src, &'src [Token], Pmtl<String>, extra::Err<S
             .repeated()
             .foldr(atom, |op, rhs| match op {
                 Token::Not => Pmtl::Not(Box::new(rhs)),
-                Token::Once => Pmtl::Once(Box::new(rhs), Time::MIN, Time::MAX),
-                Token::Historically => Pmtl::Historically(Box::new(rhs), Time::MIN, Time::MAX),
+                Token::Once => Pmtl::Once(Box::new(rhs), TimeRange::new(..)),
+                Token::Historically => Pmtl::Historically(Box::new(rhs), TimeRange::new(..)),
                 _ => unreachable!(),
             });
 
@@ -111,8 +121,8 @@ fn parser<'src>() -> impl Parser<'src, &'src [Token], Pmtl<String>, extra::Err<S
             .then(bounds.clone())
             .repeated()
             .foldr(unary, |(op, (l, u)), rhs| match op {
-                Token::Once => Pmtl::Once(Box::new(rhs), l, u),
-                Token::Historically => Pmtl::Historically(Box::new(rhs), l, u),
+                Token::Once => Pmtl::Once(Box::new(rhs), TimeRange::new((l, u))),
+                Token::Historically => Pmtl::Historically(Box::new(rhs), TimeRange::new((l, u))),
                 _ => unreachable!(),
             });
 
@@ -127,14 +137,14 @@ fn parser<'src>() -> impl Parser<'src, &'src [Token], Pmtl<String>, extra::Err<S
                 Token::And => Pmtl::And(vec![lhs, rhs]),
                 Token::Or => Pmtl::Or(vec![lhs, rhs]),
                 Token::Implies => Pmtl::Implies(Box::new((lhs, rhs))),
-                Token::Since => Pmtl::Since(Box::new((lhs, rhs)), Time::MIN, Time::MAX),
+                Token::Since => Pmtl::Since(Box::new((lhs, rhs)), TimeRange::new(..)),
                 _ => unreachable!(),
             },
         );
 
         binary.clone().foldl(
             just(Token::Since).then(bounds).then(binary).repeated(),
-            |lhs, ((_op, (l, u)), rhs)| Pmtl::Since(Box::new((lhs, rhs)), l, u),
+            |lhs, ((_op, (l, u)), rhs)| Pmtl::Since(Box::new((lhs, rhs)), TimeRange::new((l, u))),
         )
     })
     .then_ignore(end())
@@ -164,7 +174,10 @@ pub fn parse(input: &str) -> anyhow::Result<Pmtl<String>> {
 
 #[cfg(test)]
 mod test {
-    use super::*;
+    use scan_core::TimeRange;
+    use scan_pmtl::*;
+
+    use super::parse;
 
     #[test]
     fn not() {
@@ -185,8 +198,9 @@ mod test {
     #[test]
     fn bounded_once() {
         let once = parse("P[0:1] { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Once(_, 0, 1)));
-        if let Pmtl::Once(atom, 0, 1) = once {
+        assert!(matches!(once, Pmtl::Once(..)));
+        if let Pmtl::Once(atom, range) = once {
+            assert_eq!(range, TimeRange::new(0u32..=1));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -199,8 +213,9 @@ mod test {
     #[test]
     fn low_bounded_once() {
         let once = parse("P[1:] { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Once(_, 1, Time::MAX)));
-        if let Pmtl::Once(atom, 1, Time::MAX) = once {
+        assert!(matches!(once, Pmtl::Once(..)));
+        if let Pmtl::Once(atom, range) = once {
+            assert_eq!(range, TimeRange::new(1..));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -213,8 +228,9 @@ mod test {
     #[test]
     fn bounded_historically() {
         let once = parse("H[0:1] { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Historically(_, 0, 1)));
-        if let Pmtl::Historically(atom, 0, 1) = once {
+        assert!(matches!(once, Pmtl::Historically(..)));
+        if let Pmtl::Historically(atom, range) = once {
+            assert_eq!(range, TimeRange::new(0..=1));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -227,8 +243,9 @@ mod test {
     #[test]
     fn up_bounded_historically() {
         let once = parse("H[:1] { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Historically(_, Time::MIN, 1)));
-        if let Pmtl::Historically(atom, Time::MIN, 1) = once {
+        assert!(matches!(once, Pmtl::Historically(..)));
+        if let Pmtl::Historically(atom, range) = once {
+            assert_eq!(range, TimeRange::new(..=1));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -241,8 +258,9 @@ mod test {
     #[test]
     fn unbounded_once() {
         let once = parse("P { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Once(_, Time::MIN, Time::MAX)));
-        if let Pmtl::Once(atom, Time::MIN, Time::MAX) = once {
+        assert!(matches!(once, Pmtl::Once(..)));
+        if let Pmtl::Once(atom, range) = once {
+            assert_eq!(range, TimeRange::new(..));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -255,8 +273,9 @@ mod test {
     #[test]
     fn unbounded_historically() {
         let once = parse("H { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Historically(_, Time::MIN, Time::MAX)));
-        if let Pmtl::Historically(atom, Time::MIN, Time::MAX) = once {
+        assert!(matches!(once, Pmtl::Historically(..)));
+        if let Pmtl::Historically(atom, range) = once {
+            assert_eq!(range, TimeRange::new(..));
             assert!(matches!(*atom, Pmtl::Atom(_)));
             if let Pmtl::Atom(pred) = *atom {
                 assert_eq!(pred, "var > 10".to_string());
@@ -269,9 +288,13 @@ mod test {
     #[test]
     fn historically_once() {
         let historically = parse("H[0:1] P[2:3] { var > 10 }").expect("parse formula");
-        assert!(matches!(historically, Pmtl::Historically(_, 0, 1)));
-        if let Pmtl::Historically(once, 0, 1) = historically {
-            assert!(matches!(*once, Pmtl::Once(_, 2, 3)));
+        assert!(matches!(historically, Pmtl::Historically(..)));
+        if let Pmtl::Historically(once, range) = historically {
+            assert_eq!(range, TimeRange::new(0..=1));
+            assert!(matches!(*once, Pmtl::Once(..)));
+            if let Pmtl::Once(_, range) = *once {
+                assert_eq!(range, TimeRange::new(2..=3));
+            }
         } else {
             unreachable!();
         }
@@ -279,10 +302,14 @@ mod test {
 
     #[test]
     fn once_historically() {
-        let once = parse("P[2:3] H[0:1] { var > 10 }").expect("parse formula");
-        assert!(matches!(once, Pmtl::Once(_, 2, 3)));
-        if let Pmtl::Once(historically, 2, 3) = once {
-            assert!(matches!(*historically, Pmtl::Historically(_, 0, 1)));
+        let once = parse("P[2:3] H[:1] { var > 10 }").expect("parse formula");
+        assert!(matches!(once, Pmtl::Once(..)));
+        if let Pmtl::Once(historically, range) = once {
+            assert_eq!(range, TimeRange::new(2..=3));
+            assert!(matches!(*historically, Pmtl::Historically(..)));
+            if let Pmtl::Historically(_, range) = *historically {
+                assert_eq!(range, TimeRange::new(..=1));
+            }
         } else {
             unreachable!();
         }
@@ -292,8 +319,9 @@ mod test {
     fn since() {
         let since =
             parse("not { var > 10 } since[2:10] { other_var == 1 }").expect("parse formula");
-        assert!(matches!(since, Pmtl::Since(_, 2, 10)));
-        if let Pmtl::Since(args, _, _) = since {
+        assert!(matches!(since, Pmtl::Since(..)));
+        if let Pmtl::Since(args, range) = since {
+            assert_eq!(range, TimeRange::new(2..=10));
             let (lhs, rhs) = *args;
             assert!(matches!(lhs, Pmtl::Not(_)));
             assert!(matches!(rhs, Pmtl::Atom(_)));
diff --git a/scan_scxml/tests/basic.rs b/scan_scxml/tests/basic.rs
index 7ca5939..733ce9b 100644
--- a/scan_scxml/tests/basic.rs
+++ b/scan_scxml/tests/basic.rs
@@ -1,73 +1,71 @@
 use std::path::Path;
 
-use anyhow::anyhow;
-
 #[test]
-fn fsm() -> anyhow::Result<()> {
+fn fsm() {
     test(Path::new("./tests/assets/test_fsm/model.xml"))
 }
 
 #[test]
-fn datamodel() -> anyhow::Result<()> {
+fn datamodel() {
     test(Path::new("./tests/assets/test_datamodel/model.xml"))
 }
 
 #[test]
-fn enumdata() -> anyhow::Result<()> {
+fn enumdata() {
     test(Path::new("./tests/assets/test_enumdata/model.xml"))
 }
 
 #[test]
-fn send() -> anyhow::Result<()> {
+fn send() {
     test(Path::new("./tests/assets/test_send/model.xml"))
 }
 
 #[test]
-fn send_triangle() -> anyhow::Result<()> {
+fn send_triangle() {
     test(Path::new("./tests/assets/test_send_triangle/model.xml"))
 }
 
 #[test]
-fn send_onentry() -> anyhow::Result<()> {
+fn send_onentry() {
     test(Path::new("./tests/assets/test_send_onentry/model.xml"))
 }
 
 #[test]
-fn origin() -> anyhow::Result<()> {
+fn origin() {
     test(Path::new("./tests/assets/test_origin/model.xml"))
 }
 
 #[test]
-fn origin_location() -> anyhow::Result<()> {
+fn origin_location() {
     test(Path::new("./tests/assets/test_origin_location/model.xml"))
 }
 
 #[test]
-fn param() -> anyhow::Result<()> {
+fn param() {
     test(Path::new("./tests/assets/test_param/model.xml"))
 }
 
 #[test]
-fn param_triangle() -> anyhow::Result<()> {
+fn param_triangle() {
     test(Path::new("./tests/assets/test_param_triangle/model.xml"))
 }
 
 #[test]
-fn param_tennis() -> anyhow::Result<()> {
+fn param_tennis() {
     test(Path::new("./tests/assets/test_param_tennis/model.xml"))
 }
 
 #[test]
-fn conditional() -> anyhow::Result<()> {
+fn conditional() {
     test(Path::new("./tests/assets/test_if/model.xml"))
 }
 
 #[test]
-fn elif() -> anyhow::Result<()> {
+fn elif() {
     test(Path::new("./tests/assets/test_elif/model.xml"))
 }
 
-fn test(path: &Path) -> anyhow::Result<()> {
-    let (scan, ..) = scan_scxml::load(path, &[], true)?;
-    scan.adaptive(0.95, 0.01, 100).map_err(|err| anyhow!(err))
+fn test(path: &Path) {
+    let (scan, ..) = scan_scxml::load(path, &[], true).expect("load model");
+    let _ = scan.adaptive(0.95, 0.01).expect("run verification");
 }
diff --git a/src/lib.rs b/src/lib.rs
index 942db32..9943eb4 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -14,8 +14,13 @@
 //! - [x] [Promela](https://spinroot.com/spin/Man/Manual.html)
 //! - [x] [JANI](https://jani-spec.org/)
 //!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+//!
 //! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.
 
+#![warn(missing_docs)]
+#![forbid(unsafe_code)]
+
 mod progress;
 mod report;
 mod trace;
@@ -51,6 +56,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 +65,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 +74,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,
 }
 
@@ -165,6 +173,7 @@ pub struct Cli {
 }
 
 impl Cli {
+    /// Run SCAN with the parameters passed via the CLI.
     pub fn run(self) -> anyhow::Result<()> {
         let model = std::path::absolute(&self.model)?
             .file_name()
@@ -174,9 +183,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 +201,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 +247,7 @@ impl Cli {
         Ok(())
     }
 
+    #[cfg(feature = "jani")]
     fn run_jani(self, model: &str) -> anyhow::Result<()> {
         use scan_jani::*;
 
@@ -263,6 +280,7 @@ impl Cli {
         Ok(())
     }
 
+    #[cfg(feature = "promela")]
     fn run_promela(self, model: &str) -> anyhow::Result<()> {
         use scan_promela::*;
 
@@ -313,8 +331,8 @@ where
 {
     if !json {
         println!(
-            "Verifying {model} (-p {} -c {} -d {}) {:?}",
-            args.precision, args.confidence, args.duration, args.properties
+            "Verifying {model} (-p {} -c {}) {:?}",
+            args.precision, args.confidence, args.properties
         );
     }
     if let Some(bar) = progress {
diff --git a/src/main.rs b/src/main.rs
index 0815114..beca551 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,8 +1,14 @@
+//! The main binary crate for SCAN statistical model checker.
+//!
+//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
+
+#![warn(missing_docs)]
+#![forbid(unsafe_code)]
+
 use clap::Parser;
 use scan::Cli;
 
 fn main() -> anyhow::Result<()> {
-    human_panic::setup_panic!();
     let cli = Cli::parse();
     env_logger::Builder::new()
         .filter_level(cli.verbosity.log_level_filter())
diff --git a/src/report.rs b/src/report.rs
index 9ea3ebe..7d54131 100644
--- a/src/report.rs
+++ b/src/report.rs
@@ -1,13 +1,11 @@
-use scan_core::Time;
 use serde::Serialize;
 use std::fmt::Display;
 
-#[derive(Serialize)]
+#[derive(Debug, Clone, Serialize)]
 pub(crate) struct Report {
     pub(crate) model: String,
     pub(crate) precision: f64,
     pub(crate) confidence: f64,
-    pub(crate) duration: Time,
     pub(crate) rate: f64,
     pub(crate) runs: u32,
     pub(crate) successes: u32,
diff --git a/src/trace.rs b/src/trace.rs
index e9c7564..9e397fa 100644
--- a/src/trace.rs
+++ b/src/trace.rs
@@ -2,7 +2,7 @@ use std::path::PathBuf;
 
 use anyhow::anyhow;
 use clap::Parser;
-use scan_core::{Oracle, Scan, Time, Tracer};
+use scan_core::{Oracle, Scan, Tracer};
 
 const ALL_PROPS_ERR: &str =
     "the --all flag is incompatible with individually-specified properties.\n
@@ -24,9 +24,6 @@ pub(crate) struct TraceArgs {
     /// Number of traces to save.
     #[arg(long, default_value_t = 1)]
     pub(crate) traces: usize,
-    /// Max duration of execution (in model-time).
-    #[arg(short, long, default_value_t = 0)]
-    pub(crate) duration: Time,
     /// Run the model execution on a single thread.
     ///
     /// By default, SCAN uses multi-threading.
@@ -53,14 +50,14 @@ impl TraceArgs {
 
     pub(crate) fn trace<'a, Od, Tr>(&self, scan: &'a Scan<Od>, path: PathBuf, model: &Tr::ModelData)
     where
-        Od: Oracle + Sync + 'a,
+        Od: Oracle + Clone + Sync + 'a,
         Tr: Tracer,
         Tr::ModelData: Sync,
     {
         if self.single_thread {
-            scan.traces::<Tr>(self.traces, self.duration, path, model);
+            scan.traces::<Tr>(self.traces, path, model);
         } else {
-            scan.par_traces::<Tr>(self.traces, self.duration, path, model);
+            scan.par_traces::<Tr>(self.traces, path, model);
         }
     }
 }
diff --git a/src/verify.rs b/src/verify.rs
index b2a0371..44d43d5 100644
--- a/src/verify.rs
+++ b/src/verify.rs
@@ -1,6 +1,6 @@
 use anyhow::anyhow;
 use clap::Parser;
-use scan_core::{Oracle, Scan, Time};
+use scan_core::{Oracle, Scan};
 
 use super::report::Report;
 
@@ -48,10 +48,6 @@ pub(crate) struct VerifyArgs {
     /// It has to be a value between 0 and 1 (bounds excluded).
     #[arg(short, long, default_value_t = 0.01)]
     pub(crate) precision: f64,
-    /// Max duration of execution (in model-time),
-    /// to prevent infinite executions.
-    #[arg(short, long, default_value_t = 0)]
-    pub(crate) duration: Time,
     /// Run the verification on a single thread.
     ///
     /// By default, SCAN uses multi-threading.
@@ -82,29 +78,28 @@ impl VerifyArgs {
 
     pub(crate) fn verify<'a, O>(&self, model: String, scan: &'a Scan<O>) -> Report
     where
-        O: Oracle + Sync + 'a,
+        O: Oracle + Clone + Sync + 'a,
     {
-        if self.single_thread {
-            scan.adaptive(self.confidence, self.precision, self.duration)
+        let report = if self.single_thread {
+            scan.adaptive(self.confidence, self.precision)
         } else {
-            scan.par_adaptive(self.confidence, self.precision, self.duration)
+            scan.par_adaptive(self.confidence, self.precision)
         }
         .expect("verify");
-        let successes = scan.successes();
-        let failures = scan.failures();
+        let successes = report.successes;
+        let failures = report.failures;
         let runs = successes + failures;
         let rate = successes as f64 / runs as f64;
         let property_failures = self
             .properties
             .iter()
             .cloned()
-            .zip(scan.violations().into_iter().chain([0].into_iter().cycle()))
+            .zip(report.violations.into_iter().chain([0].into_iter().cycle()))
             .collect::<Vec<(String, u32)>>();
         Report {
             model,
             precision: self.precision,
             confidence: self.confidence,
-            duration: self.duration,
             rate,
             runs,
             successes,