Xstate: Question: tooling for gradual statechart specification

[PEZO19]

This project is really cool, however I think there is room for going one more abstraction level up.

Do you plan to create tools which help the user to develop (gradually specify) the state machines (/statecharts) themselves?
I am thinking about a solution where you can define some high level constraints (states, transitions, invariants) of your system, and with the exhaustive search on these existing high level constraints the user would be prompted to make further decisions about lower level constraints (states, transitions, invariants).
At the end you would be able to generate a statechart which fulfills the "requirements" (with high and low level states, transitions, invariants).
In my understanding this tool would really helpful to develop the orthogonal parts - which I think the hardest parts are to make them work together and not to forget about a single case (from the set of all cases in the cartesian product).

State machines are an old topic, I think there must be some information about that.
Do you have any idea / material on that?

[paul-f-maxson]

I use Sketch.systems to define the high level constraints, then pull the output of that into the xstate visualizer to refine the model. This isn't a foolproof workflow but it helps a lot with bootstrapping and allows a certain level of gradual development.

[davidkpiano]

Do you plan to create tools which help the user to develop (gradually specify) the state machines (/statecharts) themselves?

Yes. Working on that as we speak (literally). It will be a visual + code platform for editing, visualizing, simulating, testing, analyzing, and sharing statecharts, whether they're written in XState or some other SCXML-compatible DSL.

I am thinking about a solution where you can define some high level constraints...

This can already be done, albeit in code. What I love about statecharts in general is that you can have a higher-level abstraction, such as:

const taskMachine = Machine({
  id: 'task',
  initial: 'pending',
  states: {
    pending: {
      on: { DONE: 'finished' }
    },
    finished: { type: 'final' }
  }
});

And without changing the overall higher-level shape of the machine, you can refine states:

    pending: {
      initial: 'firstTask',
      states: {
        firstTask: {...},
        secondTask: {...},
        thirdTask: {...}
      },
      on: { DONE: 'finished' }
    },

Or you can even invoke other services, which itself is a higher-level abstraction:

    pending: {
      invoke: {
        src: 'doAllTheTasks',
        onDone: 'finished'
      }
    },

And then you can refine services and encapsulate their complexity:

const taskMachine = Machine({
  /* ... */
}, {
  services: {
    doAllTheTasks: (ctx) => {
      // Implementation details here!
      // This can be as simple as a Promise,
      // or a callback,
      // or even a completely separate statechart.
    }
  }
});

But no matter the complexity, the statechart still maintains its comprehensibility at a higher-level without losing clarity:

(pseudocode)
The task machine starts by invoking a task.
When that task is done, it is "finished".

The task does A, B, C...

As far as fulfilling "requirements" (e.g., behaviors, invariants, etc.) there's a lot to be explored in this area. Lots of inspiration in Sismic (statecharts for Python): https://sismic.readthedocs.io/en/master/contract.html

For example, if requirements are specified in natural language, e.g. in a "given-when-then" way:

A turnstile should start in the locked state. Given being locked, when a coin is inserted, it should be in the unlocked state. Given being unlocked, when pushed, it should go back to the locked state. Etc...

Each one of these GWT statements can be turned into nodes and edges:

locked --(coin)--> unlocked
unlocked --(push)--> locked

And these can gradually be turned into a complete directed graph; e.g., a state machine or statechart. I agree that it would be useful to have a tool that turns these "requirements" automatically into a fully connected statechart.

[PEZO19]

Working on that as we speak (literally). It will be a visual + code platform for editing, visualizing, simulating, testing, analyzing, and sharing statecharts...

I was wondering about the some for years now, I am so glad you are pushing this project, thanks! The reason I did not start implementing my ideas is that I am not up to date with the current research and I am quite sure someone has already found it out; now I have some time to look around.

As far as fulfilling "requirements" (e.g., behaviors, invariants, etc.) there's a lot to be explored in this area.

I have checked the sismic link, thanks! As far I have seen its DbC implementation is based on runtime checks.
My main interest is to create a tool which helps analyzing & developing the states/transitions/invariants "compile" time. I have some ideas which could be used by this (or any other similar) project, and if I can't find anything better/similar I'll implement it soon in prolog.

If anyone has any idea on that topic I would be glad to hear about it, to me it seems like a problem of safe async distributed programming.

Did you hear about P# ? At first glance it might worth to look at their approach.

The other thing I am wondering about is creating statecharts in Idris language, because its type system and overall capabilities might be used to reason about half-baked statecharts as well.

[davidkpiano]

...to me it seems like a problem of safe async distributed programming.

This is why I'm also emphasizing the Actor model in XState's design and implementation.

I've heard about the related project P (https://github.com/p-org/P) which looks like a great DSL that's based on statecharts. I'll look into P# as well.

I'm also not sure how expressive Idris' types are to handle all statechart semantics.

[PEZO19]

@davidkpiano Are you familiar with existing model checking tools & techniques?

[davidkpiano]

I am, yes. There is existing research on model-checking statecharts:

• http://users.ece.cmu.edu/~krogh/papers/ZhK06.pdf
• https://www.researchgate.net/publication/282131297_A_Framework_for_Verification_of_UML_Statechart_Diagrams
• http://archive.inf.mit.bme.hu/ftsrg_en/Publications/ddecs02.pdf

And interestingly, statecharts can themselves be used to verify other programs: https://www.amazon.com/Modeling-Verification-Using-Statecharts-Execution-based/dp/0750679492