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

[Cesar Munoz <munoz@xxxxxxxxxx>]

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

Your original definition of print_state

  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