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
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.