Contribute to CommunityModules?

[lemmy]

Would you want to contribute your operators to https://github.com/tlaplus/CommunityModules to make them more broadly available?

[nano-o]

Hi, sorry I didn't notice your issue before! Sure, I'd like to contribute this to the community modules. How should we proceed?

[lemmy]

Here is what I think would work best in terms of merging your operators with the ones in CM:

DiGraph.tla can be merged with CM's Graphs.tla module. Likewise, SequenceUtils.tla and SequencesExt.tla could become one.
LexicographicOrder can, perhaps, also be merged into SequencesExt.tla?

OrderRelations.tla could be merged and aligned with Relations.tla assuming the declared constants become operator arguments.

Quorums.tla: No other module in CM declares constants and defines assumes yet. How well does it work to reuse modules with declared constants and assumes in practices?

Maps and Misc seem mostly redundant to what we already have in CM. Do you think CStructs.tla is of general use?

IANAL, but regarding the actual contribution, you should probably create an issue or even PR. This way, we have a public record of you contributing your operators into CM under the MIT license.

[nano-o]

Okay. I think that the Quorums module was meant to be instantiated (with INSTANCE) in other module. Anyway, there's not much in Quorums.tla, so maybe it's not very useful.
CStructs.tla is about Lamport's CStructs, which are use in the Generalized Paxos algorithm. So it's very specific. Probably, very few people will want to reuse this, but it might be an interesting example.

[lemmy]

CStructs.tla could be moved to or referenced from the Paxos spec in https://github.com/tlaplus/Examples?