Well this is timely :) I’m in the middle of writing a library, based on rust-fsm crate, that adds nice support for Mealy automata, with extensions like<p>- transition handlers<p>- guards<p>- clocks<p>- composition of automata into a system.<p>The idea is to allow write tooling that will export the automata into UPPAAL and allow for model checking. This way you don’t need to make too much additional effort to ensure your model and implementation match/are up to date, you can run the checker during CI tests to ensure you don’t have code that deadlocks/ some states are always reachable etc.<p>I plan to post a link here to HN once finished.