feat(cli): add warnings for unsupported liveness features

The checker silently ignored liveness properties and fairness constraints, which could mislead users about verification coverage. Introducing explicit warnings informs users that only safety invariants are checked, improving transparency and debugging experience.

Author: danwt

specl/crates/specl-cli/src/main.rs

@@ -2581,6 +2581,10 @@ fn cmd_check(
     let module =
         parse(&source).map_err(|e| CliError::from_parse_error(e, source.clone(), &filename))?;
 
+    if !quiet {
+        warn_unsupported_features(&module);
+    }
+
     info!("type checking...");
     specl_types::check_module(&module)
         .map_err(|e| CliError::from_type_error(e, source.clone(), &filename))?;
@@ -3388,6 +3392,10 @@ fn cmd_check_symbolic(
     let module =
         parse(&source).map_err(|e| CliError::from_parse_error(e, source.clone(), &filename))?;
 
+    if !json {
+        warn_unsupported_features(&module);
+    }
+
     info!("type checking...");
     specl_types::check_module(&module)
         .map_err(|e| CliError::from_type_error(e, source.clone(), &filename))?;
@@ -3753,6 +3761,42 @@ fn filter_invariants(spec: &mut specl_ir::CompiledSpec, check_only: &[String]) -
     Ok(())
 }
 
+/// Warn about unsupported liveness features (property, fairness, temporal operators).
+/// These are parsed but silently ignored by the compiler/checker.
+fn warn_unsupported_features(module: &specl_syntax::Module) {
+    let mut has_properties = false;
+    let mut has_fairness = false;
+    let mut property_names = Vec::new();
+
+    for decl in &module.decls {
+        match decl {
+            specl_syntax::Decl::Property(d) => {
+                has_properties = true;
+                property_names.push(d.name.name.clone());
+            }
+            specl_syntax::Decl::Fairness(_) => {
+                has_fairness = true;
+            }
+            _ => {}
+        }
+    }
+
+    if has_properties {
+        eprintln!(
+            "Warning: specl does not yet support liveness properties. \
+             Only safety invariants are checked. The following property declarations \
+             will be ignored: {}",
+            property_names.join(", ")
+        );
+    }
+    if has_fairness {
+        eprintln!(
+            "Warning: specl does not yet support fairness constraints. \
+             Fairness declarations will be ignored."
+        );
+    }
+}
+
 fn parse_constants(constants: &[String], spec: &specl_ir::CompiledSpec) -> CliResult<Vec<Value>> {
     let mut values = vec![Value::none(); spec.consts.len()];
 

specl/crates/specl-cli/tests/regression_integration.rs

@@ -125,7 +125,10 @@ invariant Subset {
 "#;
     let outcome = check_spec(source, &[("MaxKey", 2)]).expect("should check");
     assert!(
-        matches!(outcome, CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }),
+        matches!(
+            outcome,
+            CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }
+        ),
         "expected OK, got: {outcome:?}"
     );
 }
@@ -231,7 +234,10 @@ invariant NotInConsistent {
 "#;
     let outcome = check_spec(source, &[("N", 2)]).expect("should check");
     assert!(
-        matches!(outcome, CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }),
+        matches!(
+            outcome,
+            CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }
+        ),
         "expected OK, got: {outcome:?}"
     );
 }
@@ -290,7 +296,10 @@ invariant KeysDomain { getKeys(d) == 0..N }
 "#;
     let outcome = check_spec(source, &[("N", 2)]).expect("should check");
     assert!(
-        matches!(outcome, CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }),
+        matches!(
+            outcome,
+            CheckOutcome::Ok { .. } | CheckOutcome::StateLimitReached { .. }
+        ),
         "expected OK, got: {outcome:?}"
     );
 }