A tool to convert (a subset of the whole spec of) an UML state machine/statechart into:
- a Promela model for spin checking.
- a TLA model
The state machine is described in a plantuml file (again, a subset of what plantuml offers) with some additions.
Finite state machines (FSM) should be fully supported. Hierarchical state machines (HSM) are WIP, and having only a Promela model.
Depends on boost (spirit, program_options, filesystem). Requires C++20 or later.
vUML. I could not get my hands on it.- An exhaustive list of FSL
- SysML
- qhsmtst/qtools