How to create an array where each index has a random number?

Question

I can't figure out how to create an array variable, that has x indices, and for each index it has a random number from some given range. How can this be done in TLA+ or PlusCal?

Let's say I want an array with 10 indices. On each index, for example on x[1], I want it's value to be a random number between 1-10.

Answer 1

Update December 2022

The RandomElement operator in the TLA+ Standard Modules supports selecting a "random element" from a set and can be used to assign a random value to each index of the array with the following code:

--------------------------- MODULE ArrayRandomV2 ---------------------------
EXTENDS Integers, Sequences, TLC

(****
--algorithm ArrayRandomV2 {
   \* define a variables, inp as initial array of 10 with all values set to 0, set of the domain (1 - 10), and index for loop
   variables inp \in [1..10 -> 0..0], seed \in {1..10}, i = 1;
   { 
     while (i <= Len(inp)) {
       inp[i] := RandomElement(seed);
       i := i + 1;
     };
     assert \A n \in 1..Len(inp) : inp[n] >= 1 /\ inp[n] <= 10;
     print inp;  
   }
}
****)
=============================================================================

The output of running this in the TCL Model Checker would be something like:

<<5, 8, 10, 5, 10, 1, 3, 4, 10, 1>>

However, please keep in mind that TLA+/PlusCal specifications are intended to be mathematical proofs and "randomness" is not math. There may be use cases where it is helpful but when creating algorithm specifications it would probably not be practical since each run of the TLC Model Checker would produce different results and would therefore not be verifiable.

Some further reading regarding using randomness in TLA+:

• RandomElement fails with TLC bug
• TLC choose a new unique element everytime

---

Original Answer

TLA+/PlusCal is designed to test algorithm behaviors so, taking that into consideration if your algorithm needs to test an array of 10 where each index is a value in the domain of 1 to 10 you could define a variable that is a tuple of count 10 with a domain of 1..10:

inp \in [1..10 -> 1..10]

When running the TLC model checker on the above variable it would test every combination of values in the domain for the array (this will take a very long time).

Here's a full sample of the code (I've adjusted the array size and domain to be 3 with a domain of 1..3 since using a large array with a large domain size will take a long time to test and a lot of memory to store):

---------------------------- MODULE ArrayRandom ----------------------------
EXTENDS Integers, Sequences, TLC

(*
--algorithm ArrayRandom {
   \* define a variable, inp, as an array (a 3-tuple) whose domain is from 1 to 3
   variables inp \in [1..3 -> 1..3];    
   { 
     assert \A n \in 1..Len(inp) : inp[n] >= 1 /\ inp[n] <= 3;
     print inp;  
   }
}
*)
=============================================================================

Running the TLC model checker on the above code will print the following:

<<1, 1, 3>>
<<1, 2, 1>>
<<1, 1, 1>>
<<1, 1, 2>>
<<1, 2, 3>>
<<1, 3, 1>>
<<1, 2, 2>>
<<1, 3, 2>>
<<1, 3, 3>>
<<2, 1, 1>>
<<2, 1, 2>>
<<2, 1, 3>>
<<2, 2, 1>>
<<2, 3, 1>>
<<2, 2, 3>>
<<2, 3, 2>>
<<2, 2, 2>>
<<2, 3, 3>>
<<3, 1, 1>>
<<3, 1, 2>>
<<3, 1, 3>>
<<3, 2, 2>>
<<3, 2, 3>>
<<3, 2, 1>>
<<3, 3, 3>>
<<3, 3, 1>>
<<3, 3, 2>>