# [PVS-Help] Re: Problem with the RANDOM function

```
> As it is implemented right now, I don't see any way to fix an array of
> random values. Therefore, initial_random(i) will potentially have a
> different value every time you evaluate it.
>
> Cesar
>

Actually, I found a way to (locally) fix an array of random values.
The solution is not elegant, but it works. The reason an array of random
values is not fix in let-in expressions is that arrays are just functions in PVS.
Therefore, the evaluation of arrays is lazy. On the other hand, lists are
"objects" and they are evaluated in let-in expressions such as
let <x> = <list> in <expr> before the evaluation of expr.

Define:

List(n:nat): TYPE = {l:list[node_status] | length(l) = n}

initial_random_list(n:nat) : RECURSIVE List(n) =
if (n=0) then null
else
let s = IF BRANDOM THEN on ELSE off ENDIF in
cons(s,initial_random_list(n-1))
endif
MEASURE n

Notice that

test3 : bool =
let i = initial_random_list(10) in
nth(i,1) = nth(i,1)

always prints TRUE. Now, define initial_random_state_fix as follows:

list2network_state(l:List(10))(i:node_id):node_status =
nth(l,i)

initial_random_state_fix : network_state =
list2network_state(initial_random_list(10))

Notice that
test4 : bool =
let i = initial_random_state_fix in
i(1) = i(1)
always prints TRUE.

print_state(ns: network_state, i: node_id): void =
IF on?(ns(i)) THEN print("ON ")
ELSIF off?(ns(i)) THEN print("OFF ")
ELSE print("? ")
ENDIF

works for initial_random_state_fix:

test5 : void =
print_node_states(initial_random_state_fix) % Never prints "?"

<PVSio> test5;
ON OFF OFF ON ON ON ON OFF ON OFF

<PVSio> test5;
ON ON OFF OFF ON ON ON OFF OFF ON

<PVSio> test5;
OFF OFF ON ON OFF ON OFF ON ON OFF

<PVSio> test5;
ON OFF OFF OFF ON ON ON OFF ON OFF

<PVSio> test5;
OFF ON ON OFF ON OFF OFF ON OFF OFF

<PVSio> test5;
OFF OFF OFF ON OFF OFF OFF OFF ON ON

Of course, every invocation of test5 generates a new list of random
values. Locally, the values in the array are fix.

Cesar
--
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace         mailto:Cesar.A.Munoz@nasa.gov
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4

```