Using XState as a model checker

[ezhikov]

Will not be giving code, since it's in very early and unfinished state (pun intended) with lots of parts that need some polish.

Since I made myself more or less familiar with statecharts I started to wonder if there is a method to identify if my statechart is, indeed, correct. It's easy to overlook some details or make some assumptions that will fail in a long run. After some search I found that there is indeed some solutions, but most of them either produce C++/C#/Java code, or don't translate into code at all. There is also some methods that are not tied to some language, but they require almost double amount of setup to work (e.g. creating another statechart to verify the main one).

During my search I found a paper that describe statechart verification with state invariants and it clicked that we already have a library for that. Here is what my early experiments yielded.

As a test case I took file uploader UI component that we are making. In natural language it have these requirements:

• All files uploaded one by one to specific API route
• If app accepts more than one file, user can add multiple files at once
• There is a limit of files that can be uploaded per control
• Files can be limited by maximum size and format (by extension)
• User can delete file at any time

My first urge was to properly assemble component with mocked UI, but, in fact it was not needed and it would be way more than it is needed to check assumptions. We don't need actual context, and machine options to check if we have our model right, but we can substitute it with something simpler. For example, for model we don't need filenames, or, actually, any info about added files, apart from their state, so list of files was presented in simplest possible form: {state: 'loading' | 'error' | 'complete'}[]. Same simplifications were made for other parts, like machine options.

One thing that is worth to mention is that we still checking not the model universally, but model with some values set. It is important, because if we set maximum files amount 10 we will get huge amount of tests that will produce same result as if there would be maximum files amount set to 3, and in my case with 3 files and "user" adding 1, 2, 3 or 4 files it was already more than 800 tests.

During this experiment I found that my initial idea was wrong and I had to made some changes in guards. My model will also hold for any requirements changes and, in fact, can be detailed and turned in actual working code. Adding details and replacing state invariants with tests that check UI with puppeteer or cypress will give us working and fully tested component and it is awesome, but not always will be the case. There is many ways to present some logic in form of statechart and I found that sometimes parallel states work great for understanding logic, but not so great for actually implementing it. In this case our model can serve as an alternative representation with test cases as additional documentation. Say, we have parallel state A and B and we don't want to A.A be active at the same time as B.A. It can be modelled and verified, but in actual code it will probably be some case of nested states.

But there is still parts that don't work as I expect. First is "Maximum call stack exceeded" when generating test plans. I haven't figured it out how to properly set state as visited in different cases with filter. Another one is lack of some kind of UI to set model parameters (e.g. maximum files limit in my example). Another thing is that if I fill meta.description with requirements for state, in test output it will replace reached state with said description. It would also be nice if we could provide some description to events, apart from their names and types.

Don't know how to conclude it, so, I'd like to know what do you think about all this?

[davidkpiano]

This is giving me a lot of food for thought for improving @xstate/test, I'll have to think more about this!

[Andarist]

This is the OSS content I'm here for! Great train thought - I would love to see your experiments in code.

[ezhikov]

I'll try to publish some results on github this weekend, but no promises yet

[tomByrer]

"Maximum call stack exceeded"

There was a situation in one of my machines where I changed a (parallel) machine into a flag in context. I used guards to check against that flag. Maybe you can track the number of calls in context?

I haven't figured it out how to properly set state as visited in different cases with filter

I would first try to save a 'persisted state' as a snapshot or temp file, then use that to 'replay' the machine from that position.
Advanced trick if you know how that object works: hand-edit that file for new states or cases...

[ezhikov]

Was digging into theme of model checkers in general and found out that exceeding memory limits is one of yet unsolved problems which often require either changing model, or specific solution regarding specific model checker. While "maximum call stack exceeded", probably not a problem with memory, I have feeling that after solving this one, I'll get new problem. Will tinker with xstate/test on weekend and find what can be done. Probably, filtering states based on "target + event" would be easier from that side also.