[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Thu, 2 Dec 2021 12:58:06 -0800*References*: <69109ba9-e46a-40cf-a92f-6f6ed45b0eefn@googlegroups.com>

On 12/2/21 2:12 AM, Earnshaw wrote:

Hello everyone:I am now wirting a Spec to verfiy a DHT ( peer-to-peer distributed hashtable) protocol, the key algorithm is based on an enhanced version ofKademlia.As we now, for such peer to peer network, the logic distance of two nodesis computed as the /exclusive or (XOR)<https://en.wikipedia.org/wiki/Exclusive_or>/ of the two node IDs,taking the result as an unsigned integer number<https://en.wikipedia.org/wiki/Integer>.d(a,b)=a⊕b but how can I build such ⊕ operator or function in TLA+? Of course, in my spec I can replace the logic distance computation with d(a,b)=|a-b | , but this is not a ideal solution.

https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla#L39-L51 -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ff85fc95-da14-b95e-4348-e179806da96d%40lemmster.de.

**Follow-Ups**:**Re: [tlaplus] XOR operator for DHT based protocol verification***From:*Siegfried Bublitz

**References**:**[tlaplus] XOR operator for DHT based protocol verification***From:*Earnshaw

- Prev by Date:
**[tlaplus] XOR operator for DHT based protocol verification** - Next by Date:
**[tlaplus] New PlusCal Tutorial** - Previous by thread:
**[tlaplus] XOR operator for DHT based protocol verification** - Next by thread:
**Re: [tlaplus] XOR operator for DHT based protocol verification** - Index(es):