[PVS-Help] problem with the RANDOM function

["Paolo Masci" <paolo.masci@xxxxxxxxxxxx>]

Hi,

I have a problem while using the RANDOM function.

In my PVS theory, I need to generate a
random state vector, with each element
initialised with "on" or "off".

When I try to animate the specification
with PVSio, I get a weird behaviour,
since sometimes elements seem to be
uninitialised.

Attached there's a simple theory that generates
the described behaviour, and the
output of PVSio. The function print_state
should never print the question mark.

I'm missing what's wrong.

Thanks,

Paolo

-----------------

test: THEORY
 BEGIN
  node_id: TYPE = below(10)
  node_status: TYPE = {on, off}
  network_state: TYPE = [node_id -> node_status]

  initial_random_state: network_state =
    (LAMBDA (i: node_id): IF RANDOM < 0.5 THEN on ELSE off ENDIF)

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

  print_node_states(ns: network_state): bool =
    FORALL (i: node_id): print_state(ns, i)

 END test

------------------

<PVSio> print_node_states(initial_random_state);
ON ON ON ON OFF ON ON ON ON ON
==>
TRUE

<PVSio> print_node_states(initial_random_state);
ON ON ON ? ON ON ? ON ? ON
==>
TRUE

<PVSio> print_node_states(initial_random_state);
ON ON ON OFF OFF ? OFF OFF ? OFF
==>
TRUE