Implement Humans-in-the-Loop, NuSMV Integration, and Clojure Tooling

[3shn]

Implementation Plan - Humans-in-the-Loop, NuSMV & Clojure Integration

This plan outlines the steps to "implement humans-in-the-loop", integrate NuSMV formal verification, and introduce Clojure tooling into the MEMS pipeline.

User Review Required

Important

NuSMV Installation: The plan assumes NuSMV can be installed via apt-get or downloaded as a binary in the CI environment.
Clojure Runtime: To run Clojure code in OpenEMS (OSGi), we need the org.clojure/clojure generic OSGi bundle (or wrap it). I propose adding it as a bundle dependency.

Note

Human-in-the-Loop: Formalized as a Pull Request Review phase.
Clojure Strategy: We will use a deps.edn based approach for development ease (VSCode/Calva), but hook into Gradle for the build process to ensure "minimal interference".

Proposed Changes

1. System Design & Documentation (Humans-in-the-Loop)

[MODIFY] mems/JOURNAL.md

• Update Pipeline Stages diagram to explicitly show "Human Verification".
• Add "Human-in-the-Loop Protocol" section.
• Add NuSMV and Clojure to the tooling list.

2. NuSMV Integration

[NEW] mems/tools/verify-nusmv.js

• Script to convert XState JSON to SMV format and run NuSMV.

[MODIFY] mems/tools/package.json

• Add "verify:nusmv": "node verify-nusmv.js".

3. Clojure Integration

We will create a specific Clojure sub-project within mems/ that can be built into an OSGi bundle or library.

[NEW] mems/clojure/deps.edn

• Dependencies: org.clojure/clojure, org.clojure/tools.logging (for SLF4J), clj-osgi.
• Aliases:
  • :test: lambdaisland/kaocha for testing.
  • :lint: clj-kondo/clj-kondo for linting.
  • :build: tools.build configuration (if needed) or simple AOT.

[NEW] mems/clojure/src/mems/core.clj

• Example namespace with (:gen-class) to demonstrate Java interop.
• Integration with standard Java concurrency keys.

[NEW] mems/clojure/test/mems/core_test.clj

• Example clojure.test suite.

[NEW] mems/clojure/.clj-kondo/config.edn

• Configuration for linting.

[NEW] mems/clojure/.vscode/settings.json

• VSCode settings to enable Jack-in/Calva support (e.g., "calva.connect.nReplPortFile" setup).

4. Build System (Gradle Updates)

[MODIFY] build.gradle

• Tasks:
  • memsVerify: Add dependency on verify:nusmv.
  • tasks.register('clojureBuild'): A task to invoke clojure -M:build or compile the Clojure code to classes/jar.
  • tasks.register('clojureTest'): A task to invoke clojure -M:test (Kaocha).
  • tasks.register('clojureLint'): A task to invoke clj-kondo.

5. CI Workflow

[MODIFY] .github/workflows/mems-pipeline.yml

• Install NuSMV step.
• Install Clojure step: actions/setup-clojure.
• Run Clojure Tests: Execute clojure -M:test (via Gradle or direct).
• Run NuSMV Verification.

Verification Plan

Automated

1. Clojure: Run clj -M:test via Gradle. Verify tests pass. Check clj-kondo output.
2. NuSMV: Run npm run verify:nusmv. Check for pass/fail.
3. Pipeline: Trigger GitHub workflow and check all steps (Java build, Clojure test, NuSMV verify).

Manual

1. IDE Support: Open mems/clojure in VSCode with Calva, try "Jack-in". Verify REPL works.
2. Human Review: Create a PR and simulate the "Human-in-the-Loop" approval.

[google-labs-jules]

Jules is on it. When finished, you will see another comment and be able to review a PR.

[google-labs-jules]

Ready for a review! A PR has been created.