fix SPECIFICATION directive extracting only first init conjunct (#18)

* fix SPECIFICATION directive extracting only first init conjunct (#17)

* simplify collect_init and use direct PartialEq in test

* bump version to 0.3.4 and update changelog

Author: fabracht

CHANGELOG.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## [0.3.4] - 2026-03-08
+
+### Fixed
+
+- `SPECIFICATION` cfg directive extracting only the first init conjunct, producing 0 initial states for multi-variable specs
+
 ## [0.3.3] - 2026-02-25
 
 ### Added

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "tla-checker"
-version = "0.3.3"
+version = "0.3.4"
 edition = "2024"
 description = "A TLA+ model checker written in Rust"
 license = "MIT OR Apache-2.0"
@@ -33,7 +33,6 @@ strip = true
 panic = "abort"
 
 [profile.bench]
-panic = "unwind"
 strip = false
 
 [profile.profiling]

src/config.rs

@@ -615,18 +615,23 @@ fn find_box_action(expr: &Expr) -> Option<Expr> {
     }
 }
 
-fn leftmost_conjunct(expr: &Expr) -> &Expr {
+fn collect_init(expr: &Expr) -> Option<Expr> {
     match expr {
-        Expr::And(l, _) => leftmost_conjunct(l),
-        other => other,
+        Expr::BoxAction(_, _) => None,
+        Expr::And(l, r) => match (collect_init(l), collect_init(r)) {
+            (Some(a), Some(b)) => Some(Expr::And(Box::new(a), Box::new(b))),
+            (a, None) => a,
+            (None, b) => b,
+        },
+        other => Some(other.clone()),
     }
 }
 
 fn resolve_specification(spec_name: &Arc<str>, spec: &mut Spec) -> Result<(), String> {
     match spec.definitions.get(spec_name.as_ref()) {
         Some((params, expr)) if params.is_empty() => {
             if let Some(next_expr) = find_box_action(expr) {
-                spec.init = Some(leftmost_conjunct(expr).clone());
+                spec.init = Some(collect_init(expr).unwrap_or(Expr::Lit(Value::Bool(true))));
                 spec.next = Some(next_expr);
                 return Ok(());
             }
@@ -1001,6 +1006,65 @@ mod tests {
         );
     }
 
+    #[test]
+    fn apply_config_specification_inlined_multi_var() {
+        let mut spec = Spec {
+            vars: vec![Arc::from("x"), Arc::from("y")],
+            init: None,
+            next: None,
+            invariants: vec![],
+            invariant_names: vec![],
+            definitions: std::collections::BTreeMap::new(),
+            instances: vec![],
+            extends: vec![],
+            fairness: vec![],
+            assumes: vec![],
+            liveness_properties: vec![],
+            constants: vec![],
+        };
+
+        let init_part_1 = Expr::In(
+            Box::new(Expr::Var(Arc::from("x"))),
+            Box::new(Expr::SetEnum(vec![Expr::Lit(Value::Int(1))])),
+        );
+        let init_part_2 = Expr::In(
+            Box::new(Expr::Var(Arc::from("y"))),
+            Box::new(Expr::SetEnum(vec![Expr::Lit(Value::Bool(true))])),
+        );
+        let next_expr = Expr::Var(Arc::from("SomeNext"));
+        let spec_body = Expr::And(
+            Box::new(Expr::And(
+                Box::new(init_part_1.clone()),
+                Box::new(init_part_2.clone()),
+            )),
+            Box::new(Expr::BoxAction(
+                Box::new(next_expr.clone()),
+                Arc::from("vars"),
+            )),
+        );
+        spec.definitions
+            .insert(Arc::from("Spec"), (vec![], spec_body));
+
+        let cfg = parse_cfg("SPECIFICATION Spec").unwrap();
+        let mut domains = Env::new();
+        let mut checker_config = CheckerConfig::default();
+
+        apply_config(
+            &cfg,
+            &mut spec,
+            &mut domains,
+            &mut checker_config,
+            &[],
+            &[],
+            false,
+        )
+        .unwrap();
+
+        let expected_init = Expr::And(Box::new(init_part_1), Box::new(init_part_2));
+        assert_eq!(spec.init.unwrap(), expected_init);
+        assert_eq!(spec.next.unwrap(), next_expr);
+    }
+
     #[test]
     fn apply_config_specification_missing_box_action_errors() {
         let mut spec = Spec {

test_cases/should_pass/specification_directive_multi_var.cfg

@@ -0,0 +1,2 @@
+SPECIFICATION Spec
+INVARIANT TypeOK

test_cases/should_pass/specification_directive_multi_var.tla

@@ -0,0 +1,43 @@
+---- MODULE specification_directive_multi_var ----
+LOCAL INSTANCE Integers
+
+VARIABLES number, toggle
+
+vars == <<number, toggle>>
+
+Numbers == {22, 23}
+NumberMax == 23
+NumberMin == 22
+
+Init ==
+  /\ number \in Numbers
+  /\ toggle \in BOOLEAN
+
+NumberIncrease ==
+  /\ number < NumberMax
+  /\ number' = number + 1
+  /\ UNCHANGED toggle
+
+NumberDecrease ==
+  /\ number > NumberMin
+  /\ number' = number - 1
+  /\ UNCHANGED toggle
+
+Toggle ==
+  /\ toggle' = ~toggle
+  /\ UNCHANGED number
+
+Next ==
+  \/ NumberIncrease
+  \/ NumberDecrease
+  \/ Toggle
+
+Spec ==
+  /\ Init
+  /\ [][Next]_vars
+
+TypeOK ==
+  /\ number \in Numbers
+  /\ toggle \in BOOLEAN
+
+====

tests/oracle.rs

@@ -705,6 +705,41 @@ fn test_should_pass_specification_directive() {
     );
 }
 
+#[test]
+fn test_should_pass_specification_directive_multi_var() {
+    let path = Path::new("test_cases/should_pass/specification_directive_multi_var.tla");
+    let cfg_path = Path::new("test_cases/should_pass/specification_directive_multi_var.cfg");
+    let input = fs::read_to_string(path).expect("failed to read spec file");
+    let cfg_input = fs::read_to_string(cfg_path).expect("failed to read cfg file");
+    let mut spec = parse(&input).expect("failed to parse spec");
+    let tlc_cfg = parse_cfg(&cfg_input).expect("failed to parse cfg");
+
+    let mut domains = Env::new();
+    let mut config = CheckerConfig::default();
+    config.spec_path = Some(path.to_path_buf());
+
+    apply_config(
+        &tlc_cfg,
+        &mut spec,
+        &mut domains,
+        &mut config,
+        &[],
+        &[],
+        false,
+    )
+    .expect("failed to apply config");
+
+    let result = check(&spec, &domains, &config);
+    assert!(
+        matches!(result, CheckResult::Ok(_)),
+        "specification_directive_multi_var.tla with SPECIFICATION directive should pass, got: {result:?}",
+    );
+    if let CheckResult::Ok(stats) = &result {
+        assert_eq!(stats.states_explored, 4);
+        assert_eq!(stats.transitions, 8);
+    }
+}
+
 #[test]
 fn test_cfg_cli_constant_overrides_cfg() {
     let path = Path::new("test_cases/official/TwoPhase.tla");