MidGARD is a Rust-based command-line tool suite that accepts TLA+ formal specifications, leverages the TLC Model Checker, and performs directed-graph analysis to produce structured, reproducible test sequences for regression testing. The requirements below capture what the system must do, and are organized around the major functional areas of the pipeline.
The system must accept a TLA+ specification as input and invoke the TLC model checker to verify correctness. If the specification passes, the system must generate a Graphviz DOT directed graph of state predicates (nodes) and actions (edges). If the state space is too large for direct DOT generation, the system must support TLC’s VIEW and ALIAS options to abstract the model and reduce the state space to a manageable size.
Implementation will use Rust to invoke TLC as an external process, capture model-checking output, and manage DOT file generation through a command-line workflow.
The system must parse and clean the generated DOT file, including removal of self-referencing edges caused by TLA+’s stuttering invariance. Additional cleanup steps (e.g., removing unreachable nodes, collapsing equivalent states) should be configurable. The cleaned graph must be stored in a format amenable to efficient algorithmic traversal.
Implementation will use Rust graph-processing logic, likely supported by the petgraph crate, to parse, clean, and store the DOT graph in an efficient in-memory directed graph structure.
Given a cleaned digraph, the system must algorithmically generate a set of test sequences (routes through the graph). Generation must support at least two modes: (a) full-coverage mode, which produces a minimal set of routes that traverse all nodes and edges, and (b) n-test mode, which produces exactly n routes that are as mutually distinct as possible. Generation must be seeded (randomly or by a user-provided value) for reproducibility. A “set of seeds” mechanism should allow users to produce families of fully distinct route sets.
Implementation will use graph traversal and coverage algorithms to generate candidate paths, compare sequence distinctness, and produce reproducible outputs based on user-provided configuration and seed values.
The system must reorder the generated test sequences according to a user-specified criterion (e.g., random shuffle, coverage priority, edge diversity) so that any prefix of the ordered list still constitutes a reasonable test suite. The final output must be a structured, machine-readable list of test sequences, such as CSV or JSON, suitable for integration into SanDisk’s regression deployment workflows. A time-permitting extension may explore AI-assisted translation of generated sequences into more readable action steps for test engineers.
Implementation will serialize generated sequences into structured output formats such as CSV or JSON, depending on the format best suited for SanDisk’s testing workflow.
The core system must be implemented in Rust, leveraging Cargo and relevant crates for graph analysis (e.g., petgraph). The TLC model checker (Java-based, requiring OpenJDK ≥ 11.0.6) will be invoked as an external process.
All outputs must be fully reproducible given the same specification, configuration, and seed. Deterministic behavior is essential for regression validation.
The project must deliver a detailed reference manual for SanDisk product teams, a well-commented codebase, and a complete private GitHub repository. Documentation should be sufficient for a test engineer unfamiliar with the tool to run it independently.
The architecture should be modular enough to accommodate new graph analysis algorithms, additional criteria for test generation, and future integration with SanDisk’s internal tooling.
The command-line interface should be clear enough for SanDisk engineers to run the tool, configure generation options, and interpret output files without needing to modify the source code.
The project spans two semesters with a team of four students, guided by a project mentor and a client from SanDisk. The development process is structured as follows:
| Phase | Activities |
|---|---|
| Spring (Jan–May) | Completed requirements gathering, TLA+ onboarding, architecture design, initial DOT parsing exploration, graph analysis planning, and documentation framework. |
| Summer | Project paused. The team will reconvene in Fall to begin full implementation. |
| Fall (Aug–Dec) | Full pipeline implementation, test generation engine, ordering/output module, end-to-end testing with SanDisk-provided specifications, final documentation and delivery. |