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

*From*: Siegfried Bublitz <sbublitz24@xxxxxxxxx>*Date*: Wed, 8 Dec 2021 08:04:28 -0800 (PST)*References*: <69109ba9-e46a-40cf-a92f-6f6ed45b0eefn@googlegroups.com> <ff85fc95-da14-b95e-4348-e179806da96d@lemmster.de>

Hi,

what about this?

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

\* 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

Siegfried

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

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/0bb8313a-7347-4c82-9c8c-47ef67175bfen%40googlegroups.com.

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

**Re: [tlaplus] XOR operator for DHT based protocol verification***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] Re: Video Tutorial (Request for Feedback)** - Next by Date:
**[tlaplus] Meaning of conjunction or disjunction of fairness** - Previous by thread:
**Re: [tlaplus] XOR operator for DHT based protocol verification** - Next by thread:
**[tlaplus] New PlusCal Tutorial** - Index(es):