[machine-check] Command name matching, can it be removed?

[Kelerchian]

One functionality of machine-check is checking whether a particular state of a role has a command.
This checks whether a role's particular state has a command corresponding to its SwarmProtocolType counterpart (which relates to checking whether the swarm protocol can get stuck in the middle, thus halting the swarm)

One part of this functionality checks the command's name.
Unlike the types the command emits, the command's name does not affect how the swarm state changes in any way.
Furthermore, the command name check adds to the process of writing the application's test code.

Is it a good idea to remove the command name matching (and maybe replace it with duplicate name-checking, which will be more valuable in rare cases when the application developer does not use TypeScript) or is it a bad idea and I have missed a context?

[rkuhn]

As far as I’m aware the command names are not required for proving the correctness of the theory, but writing the paper without them would be awkward. I know that this is not a strong argument. The strongest argument that I know is that there seems to be value in clearly distinguishing the intent (i.e. the command) from the result (i.e. the emitted events) because one is local and ephemeral and the other is global and persistent. Without a name it would be difficult to do this.

[Kelerchian]

I understand the importance, especially when the event name can not perfectly describe the intention at all times.
Considering the "audience" of the SwarmProtocolType consists only of the unit test (I am not sure though if it is not used for anything else than that).

Yet when used with machine-check, it binds the various roles/machines implementation with constraints that could only be adjusted manually (e.g. misnomer needs to be retyped instead of inferred).

What I think is ideal is to remove this constraint until SwarmProtocolType has more audience and helpful influence toward the various roles/machines. Then, applying this constraint will not only be a justifiable action but also a good constraint.

[rkuhn]

Ah, I see (and you raise a good point): the intention of machine-check is not only to verify conformance, but also to certify correspondence to an external workflow design. The audience should include non-programmers, to be exact. For this purpose, I have a TODO on my stack to write a function that transforms a SwarmProtocolType to a PlantUml text (for example). In the output, the command names are used in discussions about the workflow, they are basically the text on the buttons that can be pressed in a given state.