I am a tool creator (serious tools count of one) that created a tool out of genuine personal need, in reference to the note linked from " serious contexts of use".

In my case it is in context to the state machine portion of the blog.

The link to Leslie Lamport and TLA+ is informative and the initial point of my tool making was to end up with an executable specification of a state machine that could be translated to TLA+ to allow validation by formal methods.

For functional safety (IEC 61508 and subsidiary standards) this is the Holy Grail for a significant number of applications. Think things like Rail Signaling, Burner Management Systems, Aircraft Landing Gear Hydraulic Sequencing, complex machinery automation and interlocking, to name a very few examples. It can also extend to Cyber Security and transactional systems like banking etc.

In my tool I haven't quite got to automatic translation to TLA+, yet, and maybe I personally won't, because as discussed in the blog and some of it's links, the interface itself prompts a certain level of thinking that is highly beneficial. So I have done everything but an automatic translation to TLA+, but I can see no reason it is not possible, I already automatically translate the specification into controller code.

But the key point arising from the definition of state based behavior, which is what TLA+ is all about, is that implicit state is the enemy. And if all states and transitions are not defined explicitly, then the door is opened to implicit state.

The often-quoted example is the Apple Facetime bug where you could follow a specific, unintended, sequence to make a call and then listen to a callees microphone before they answered.

https://medium.com/@DavidKPiano/the-facetime-bug-and-the-dan...

Also interesting is this one where a bug involving implicit state was fixed by changing two characters, after som eeffort.

https://blog.scottlogic.com/2020/12/08/finite-state-machines...

For finite state machines the problem is the State Chart (and or UML) - neither forces an exhaustive and unambiguous examination of every transition for every state.

In order to do this, you need a State Table, and ideally a dereferencing of the inputs by grouping them into Transition Input Conditions from raw inputs.

The State Table looks like columns with all possible "From" states heading them and the "To" state underneath. Where more than one possible "To" state is possible, a new column is created with the same "From" state.

The logic is "scanned" or "polled" at regular intervals, it generally cannot be event driven, to ensure deterministic outcomes are easily known, because the precedence for a state that might solve two different transitions at the same time is established by left to right on the table as the table is scanned (could be right to left, but it needs to be defined and repeatable).

Try being totally deterministic in your specification with a chart or UML, you end up having to assign order of execution numbers to each state bubble as a minimum, and it is hard to make intuitively clear the exact behavior that will emerge in edge cases.

But, straight away any impossible state transitions are explicitly excluded and all possible transitions are easily read off the first two rows

The state columns are crossed with rows of transition conditions, which are logic conditions derived from raw inputs. Every square for a transition possibility for any state must have an entry, even if just an X to indicate not allowed or don't care.

Not only that, every possible transition has a unique square (with grid reference if you want) which you can attach a design or user comment to for explaining the reasoning for the selected transition, or for generating an alarm for that transition condition. So even a square with an X might get a comment to explain why that transition was elected not to be valid.

Outputs are driven as a feature of state, as a Moore machine is better intuitively, even though you likely end up with more states. Often the state explosion is vastly improved with hierarchal state machines, the first thing to do is split out modes and states, often giving great improvement.

You then have the basis for an exhaustive and unambiguous definition of a state machine with no implicit state. It can be an executable specification, the tool I have created allows single stepping thru the "scans" of the logic, and generates things like state trace logs etc for debugging while designing.

If you want to specify known state based behavior with no implicit state, this is by far the best available practice, only improved by a further examination by formal methods (TLA+ or similar) of the resulting specification. UML won't get you here, and no methodology of state charts I have seen or can imagine can get to the same place in a comprehendible way.

But, I find the process that the designer is forced to use to create the state machine/s in tabular form like this yields immense improvements over traditional specification methods, which usually focus almost exclusively on expected behavior only and are in the form of the "crappy narrative".

Because the target is industrial safety and control systems I put an OPC server in so the logic could be simulated and hook up to a HMI to test user interaction, if desired.

Final point is the tabular form then also leads to an extremely compact and succinct algorithm for solving that reduces the logic required to handful of bitwise logic operations. Given the maxim that errors are proportional to LOC, this means the chances of errors can be substantially reduced over any other state machine implementation I have seen, by orders of magnitude, something highly desirable for a functional safety implementation.

I have spent years on this and development of the tool, for my own use at this stage. But I am very confident there is no better practice (yet I still wait for the world to beat a path to my door), and it starts with the correct interface to describe the specification, and flows naturally from there. There are hints of similar approaches, some around for a long time, but nothing I have seen that condenses all the dimensions into one 2D table like this and allows it to be executable in it's own format.

It is a little involved to explain, often needing a couple of hours of hours of focused attention. But once people see it and get it, they usually don't want to work any other way.

But I have found a significant portion of my colleagues, who are experienced engineers, just aren't able to grasp the full extents of what it means, why and how to use it or that it can be used to describe fully arbitrary behaviors - first clue is if they do not believe that such a simple basis can describe all wanted behaviors and/or they ask why they have to use the table and why not a chart or UML. UML is just not going to get you there, this way will.

There is a lot more, but I would be surprised if many people have read this far.

But I take my chance to explain the surprising benefits of a particular UI/interface in solving a particular problem and how it flows on. If anyone is genuinely interested feel free to DM me, as I said I have a tool I made in PyQt to enable this workflow. It has been used on design of some large industrial safety systems, some projects with overall value in excess of $1B, but lends itself to any state based behavior.