Generating Random Numbers/probability distribution

[Ulrich Kowohl]

Hi everybody,

in my project there is a need for using prism generated random numbers
in the model.
Is there any chance to generate some?

Otherwise i have the Workaround:

test : [1..100] init 1;
[] true -> (test'=1);
[] true -> (test'=2);
...
[] true -> (test'=100);

for generating a random Value for the variable "test" in the model.
The Question for that is, how random the transitions are. Is the
probability for all of the transitions a uniform distribution?

greetings,

Ulrich

[Vojtech Forejt]

Dear Ulrich,

if you use DTMCs, then the distribution is uniform, as you correctly say. But note that PRISM outputs a warning, because overlapping commands in DTMC generally signify an error in the model design. Also in MDPs the semantics of overlapping commands is different (there each command represents a nondeterministic choice).

Probably the simplest "neat" workaround for your problem is to define multiple initial states, one for each number "test" (see http://www.prismmodelchecker.org/manual/ThePRISMLanguage/MultipleInitialStates), and then use the "avg" filter described at http://www.prismmodelchecker.org/manual/PropertySpecification/Filters

Kind regards,

Vojta

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To post to this group, send email to prismmod...@googlegroups.com.
> To unsubscribe from this group, send email to prismmodelchec...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/prismmodelchecker?hl=en.
>

[Dave Parker]

> if you use DTMCs, then the distribution is uniform, as you correctly
> say. But note that PRISM outputs a warning, because overlapping
> commands in DTMC generally signify an error in the model design. Also
> in MDPs the semantics of overlapping commands is different (there
> each command represents a nondeterministic choice).

and for this reason, the preferred PRISM code would be:

test : [1..100] init 1;
[] true -> 1/100:(test'=1)
+ 1/100:(test'=2)
+ 1/100:(test'=3)
...
+ 1/100:(test'=100);

Admittedly, this is pretty unpleasant - adding a nicer language
construct for this to PRISM is long overdue. In the meantime, a second
possible workaround is to use the (beta release) of PRISM's preprocessor
tool, which can help you script models like the above:

http://www.prismmodelchecker.org/prismpp/

Regards,

Dave.

[Ulrich Kowohl]

hi :)

i am not sure about it. This solutions might not work on my project. I
use the Prism - Generator for generating Markov Chains. These Markov
Chains are used outside the Generator by another tool. Sometimes i
need some variables from the model. Sometimes i have to define these
variables (setting on a definite value) and sometimes i need a random
value for the variable.

Is there another solution?

best wishes,

Ulrich :)

[Vojtech Forejt]

Dear Ulrich,

I am afraid that from the information you have provided it's hard to devise a solution that will help you. It actually still seems to me that the PRISM preprocessor might be what you are looking for. If not, could you please post some concrete examples together with a description of the analysis you want to perform on them?

Best,

Vojta