A tool to convert (a subset of the whole spec of) a 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.
Depends on boost (spirit, program_options, filesystem). Requires C++20 or later.
- Syntax
- Examples:
vUML. I could not get my hands on it.- An exhausting list of FSL
- SysML
- qhsmtst/qtools