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

[tlaplus] Strategies to avoid exploring symmetric combinations in non-model values?

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.