Re: [work] Re: [PVS-Help] problem with the RANDOM function

[Cesar Munoz <munoz@xxxxxxxxxx>]

To complement Leonard's answer,consider the following declaration

A : real = RANDOM

then, go to PVSio and type (several times)

<PVSio> A=A;

==> 
FALSE

Then, try (several times)
<PVSio> let i = A in i=i;

==> 
TRUE

"let" works in this case as it evaluates RANDOM before evaluating i=i.
However, try this case (several times):

<PVSio>  let i = initial_random_state in 
     i(1)=i(1);
==> 
FALSE

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

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