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 scientifically derived test sequences for regression deployment. 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.
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.
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.
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 suitable for integration into SanDisk’s regression deployment workflows.
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 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) | Requirements gathering, TLA+ onboarding, architecture design, DOT parsing prototype, initial graph analysis algorithms, 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. |