Hello everyone:
I am now wirting a Spec to verfiy a DHT ( peer-to-peer distributed hash
table) protocol, the key algorithm is based on an enhanced version of
Kademlia.
As we now, for such peer to peer network, the logic distance of two nodes
is 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.