Envisioned Solution

We are building a system to be able to test a SSD through TLA+ file code in randomly generated ways. The system will be able to take a TLA+ file that is loaded with multiple tests and randomly pick tests. The system will loop through and test multiple different instructions. Through a modified pluspy, the system will take the TLA+ into Python, which can then be turned into mvme-cli commands that will be given to an SD. We will then have some Python code that will log if an error occurred and have a log of the actions that took place to make that error occur.

Planned System

img