[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



> 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

Hi Paolo,

The behavior you describe is due to the fact that your
initial_random_state function is not free of side-effects.
The call to the RANDOM function evaluates to a different value
each time. In print_state you call ns(i) two times and the
results will be different for the two calls.

Changing your print_state function to:

    LET nsi = ns(i) IN
     (IF on?(nsi) THEN print("ON ")
      ELSIF off?(nsi) THEN print("OFF ")
      ELSE print("? ")
      ENDIF)

will solve that problem. However, you have to be careful, since
you might have the same problem elsewhere in your code.

Hope this helps,

Leonard