Most interactive applications are informally specified state-machines with intertwined business-logic and state-management.
With the possibility of using virtual actor systems, it is highly desirable to be able to formally specify the states, messages and transitions associated with an application separate from the business logic so that we can better reason about an application's behaviour and correctness.
This project specifies one such DSL, and provides a parser/code-generator to transform the DSL into idiomatic Orleans code, allowing the user to formally specify state-transitions and custom business-logic separately. A few analysis tools to reason about the state-machine are also provided.
| Mono | .NET |
|---|---|
 |
 |