如何创建每个索引都有一个随机数的数组？

Question

我不知道如何创建一个数组变量，该变量有x个索引，对于每个索引，它都有一个来自给定范围的随机数。如何在TLA+或PlusCal中做到这一点？

假设我想要一个包含10个索引的数组。在每个索引上，例如在x1上，我希望它的值是介于1-10之间的随机数。

Answer 1

TLA+/PlusCal是用来测试算法行为的，考虑到这一点，如果算法需要测试一个10的数组，其中每个索引都是1到10域中的值，那么您可以定义一个变量，它是一个计数10的元组，其域为1..10。

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

当对上述变量运行TLC模型检查器时，它将测试数组域中的每个值组合(这将花费很长的时间)。

下面是代码的完整示例(我已经将数组大小和域调整为具有1..3域的3，因为使用大域大小的大数组将需要很长时间来测试，存储大量内存)：

---------------------------- 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;  
   }
}
*)
=============================================================================

在上述代码上运行TLC模型检查器将打印以下内容：

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