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

*From*: "'Chris' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Fri, 10 Nov 2023 22:51:23 +0000 (UTC)*References*: <a9174435-acc5-43a7-9ec9-83fdbba308f4n@googlegroups.com> <47158731-0aad-474f-909a-32abf95295fa@gmail.com>

There is very hacky approach to try and explicitly normalise the state after each step.

I have a partial example of this where I was trying to normalise all the ballot numbers in a Paxos implementation, as well as removing un-receivable messages to make the state space finite for small models.

The paxos variant: https://github.com/Cjen1/consensus-tlaplus/blob/vector-paxos/VectorPaxos/VectorPaxos.tla

The normalisation step: https://github.com/Cjen1/consensus-tlaplus/blob/vector-paxos/VectorPaxos/Finite.tla

I can't quite remember if this approach ended up working in TLA, but there is also stateright implementation where I could directly change the symmetry function.

On Friday, November 10, 2023 at 10:42:00 PM GMT, Hillel Wayne <hwayne@xxxxxxxxx> wrote:

If the order doesn't matter, could you instead use a bag?
Then all three of your sequences would map to the same value `(1
:> 1 @@ 2 :> 1 @@ 3 :> 1)`. If you needed to
convert it back to a sequence, you could use FoldFunction
with `Append `to pick an arbitrary sequence
representation of the bag.

H

On 11/10/2023 12:46 PM, J.D. Meadows
wrote:

Let's say that I have a set of integers, and I totally need
them to be numbers and not model values so that they are
comparable and I can perform arithmetic. Eg.:

Vals == 1..5

Tuples = Vals \X Vals
\X Vals

with (t \in Tuples){

...

}

But then in my particular problem I know that
<<1,2,3>> is equivalent to <<3,1,2>> and
<<2,3,1>>. Is there some way of filtering Tuples so that I can
avoid exploring the two latter equivalent cases? Ideally the
solution should scale to long sequences, not just 3 elements.

It would be nice if I could define a set of symmetric values
in the model overview form.

Or if I could define an external generator coded in Java that
I could plug in into the spec. That way I could keep track of
already generated states in the Java code and only return
non-equivalent combinations.

Or maybe have TLA+ accept some external file that I could
generate with a programming language of my choice.

-- 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/a9174435-acc5-43a7-9ec9-83fdbba308f4n%40googlegroups.com.

--

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/47158731-0aad-474f-909a-32abf95295fa%40gmail.com.

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/47158731-0aad-474f-909a-32abf95295fa%40gmail.com.

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/978874540.1778592.1699656683192%40mail.yahoo.com.

**References**:

- Prev by Date:
**Re: [tlaplus] Strategies to avoid exploring symmetric combinations in non-model values?** - Next by Date:
**[tlaplus] Experience report: unicode-first spec writing** - Previous by thread:
**Re: [tlaplus] Strategies to avoid exploring symmetric combinations in non-model values?** - Next by thread:
**[tlaplus] Experience report: unicode-first spec writing** - Index(es):