Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
Kelerchian opened this issue Sep 11, 2023 · 3 comments
Open

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

Kelerchian opened this issue Sep 11, 2023 · 3 comments

Comments

@Kelerchian
Copy link
Contributor

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
Copy link
Member

rkuhn commented Sep 16, 2023

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
Copy link
Contributor Author

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
Copy link
Member

rkuhn commented Sep 22, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants