Re: [tlaplus] XOR operator for DHT based protocol verification

EXTENDS Integers, Sequences

\* The Hamming Distance between two vectors of equal length is the number
\* of components at which they differ.

RECURSIVE HamDist(_,_) \* define as prefix operator
HamDist(a,b) == IF Len(a) # Len (b) THEN -1 \* or some undefined value
ELSE IF a = <<>> THEN 0 \* this implies b = <<>>
ELSE IF Head(a) = Head(b) THEN HamDist(Tail(a),Tail(b))
ELSE 1 + HamDist(Tail(a),Tail(b))

a (+) b == HamDist(a,b) \* define as infix operator

Markus Alexander Kuppe schrieb am Donnerstag, 2. Dezember 2021 um 21:58:17 UTC+1:

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

https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla#L39-L51