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

*From*: "J.D. Meadows" <tr1pl3.d3v@xxxxxxxxx>*Date*: Fri, 10 Nov 2023 10:46:56 -0800 (PST)

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.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Macros don't compose with the parallel assignment operator** - Next by Date:
**Re: [tlaplus] Strategies to avoid exploring symmetric combinations in non-model values?** - Previous by thread:
**Re: [tlaplus] TLC: distinct states decreasing?** - Next by thread:
**Re: [tlaplus] Strategies to avoid exploring symmetric combinations in non-model values?** - Index(es):